proposition: Theorem exp_ln_powerRZ : forall u v : Z, (0 < u)%Z -> (exp (ln u * v) = powerRZ u v)%R.
proof: Proof. intros u v H1. cut (forall e f : nat, (0 < e)%Z -> exp (ln e * f) = powerRZ e f). intros H2. case (Zle_or_lt 0 v); intros H3. replace u with (Z_of_nat (Z.abs_nat u)); [ idtac | apply inj_abs; auto with zarith ]. replace v with (Z_of_nat (Z.abs_nat v)); [ idtac | apply inj_abs; auto ]. apply H2. rewrite inj_abs; auto with zarith. replace v with (- Z.abs_nat v)%Z. rewrite <- Rinv_powerRZ; auto with zarith real. replace u with (Z_of_nat (Z.abs_nat u)); [ idtac | apply inj_abs; auto with zarith ]. rewrite Ropp_Ropp_IZR; rewrite Ropp_mult_distr_r_reverse; rewrite exp_Ropp. rewrite H2; auto with real. rewrite inj_abs; auto with zarith. apply Rgt_not_eq, IZR_lt; auto with real. rewrite <- Zabs_absolu; rewrite <- Zabs_Zopp. rewrite Z.abs_eq; auto with zarith. intros e f H2. induction f as [| f Hrecf]. simpl in |- *; ring_simplify (ln e * 0)%R; apply exp_0. replace (ln e * S f)%R with (ln e * f + ln e)%R. rewrite exp_plus; rewrite Hrecf; rewrite exp_ln; auto with real zarith. 2: now apply IZR_lt. replace (Z_of_nat (S f)) with (f + 1)%Z. rewrite powerRZ_add; try apply IZR_neq; simpl; auto with real zarith. rewrite inj_S; auto with zarith. replace (IZR (S f)) with (f + 1)%R; [ ring | idtac ]. apply trans_eq with (IZR (f + 1)). rewrite plus_IZR; simpl in |- *; auto with real. apply trans_eq with (IZR (Z.succ f)); auto with zarith real. rewrite <- inj_S; auto with zarith real. Qed.
imports: Reals ZArith List PeanoNat Psatz