diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-27 21:30:53 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-27 21:30:53 +0200 |
| commit | 0a255f51809e8d29a7239bfbd9fe57a8b2b41705 (patch) | |
| tree | 9f9b9515dc1bdddf17ab8746a7a061d23d6b15ca /theories/Reals/Rpower.v | |
| parent | cc12397b32785b06ed892e8ad420cfe253842141 (diff) | |
| parent | f5c81ac1bcae7c40d5e89229647c06c97b5ddc85 (diff) | |
Merge PR#414: Some more theory on powerRZ.
Diffstat (limited to 'theories/Reals/Rpower.v')
| -rw-r--r-- | theories/Reals/Rpower.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index b8040bb4f..0e0246cbf 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -473,6 +473,20 @@ Proof. apply exp_Ropp. Qed. +Lemma powerRZ_Rpower x z : (0 < x)%R -> powerRZ x z = Rpower x (IZR z). +Proof. + intros Hx. + assert (x <> 0)%R + by now intros Habs; rewrite Habs in Hx; apply (Rlt_irrefl 0). + destruct (intP z). + - now rewrite Rpower_O. + - rewrite <- pow_powerRZ, <- Rpower_pow by assumption. + now rewrite INR_IZR_INZ. + - rewrite opp_IZR, Rpower_Ropp. + rewrite powerRZ_neg, powerRZ_inv by assumption. + now rewrite <- pow_powerRZ, <- INR_IZR_INZ, Rpower_pow. +Qed. + Theorem Rle_Rpower : forall e n m:R, 1 < e -> 0 <= n -> n <= m -> e ^R n <= e ^R m. Proof. |