proposition: Lemma Pow_x_infinity : forall x:R, Rabs x > 1 -> forall b:R, exists N : nat, (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) >= b).
proof: Proof. intros; elim (archimed (b * / (Rabs x - 1))); intros; clear H1; cut (exists N : nat, INR N >= b * / (Rabs x - 1)). - intro; elim H1; clear H1; intros; exists x0; intros; apply (Rge_trans (Rabs (x ^ n)) (Rabs (x ^ x0)) b). { apply Rle_ge; apply Power_monotonic; assumption. } rewrite <- RPow_abs; assert (Rabs x = 1 + (Rabs x - 1)) by ring. rewrite H3; apply (Rge_trans ((1 + (Rabs x - 1)) ^ x0) (1 + INR x0 * (Rabs x - 1)) b). + apply Rle_ge; apply poly; fold (Rabs x - 1 > 0); apply Rgt_minus; assumption. + apply (Rge_trans (1 + INR x0 * (Rabs x - 1)) (INR x0 * (Rabs x - 1)) b). { apply Rle_ge; apply Rlt_le; rewrite (Rplus_comm 1 (INR x0 * (Rabs x - 1))); pattern (INR x0 * (Rabs x - 1)) at 1; rewrite <- (let (H1, H2) := Rplus_ne (INR x0 * (Rabs x - 1)) in H1); apply Rplus_lt_compat_l; apply Rlt_0_1. } cut (b = b * / (Rabs x - 1) * (Rabs x - 1)). * intros; rewrite H4; apply Rmult_ge_compat_r. { apply Rge_minus; unfold Rge; left; assumption. } assumption. * rewrite Rmult_assoc; rewrite Rinv_l. { ring. } apply Rlt_dichotomy_converse; right; apply Rgt_minus; assumption. - assert ((0 <= up (b * / (Rabs x - 1)))%Z \/ (up (b * / (Rabs x - 1)) <= 0)%Z) by apply Z.le_ge_cases. elim H1; intro. + elim (IZN (up (b * / (Rabs x - 1))) H2); intros; exists x0; apply (Rge_trans (INR x0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))). * rewrite INR_IZR_INZ; apply IZR_ge. normZ. slia H3 H5. * unfold Rge; left; assumption. + exists 0%nat; apply (Rge_trans (INR 0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))). * rewrite INR_IZR_INZ; apply IZR_ge; simpl. normZ. slia H2 H3. * unfold Rge; left; assumption. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac