equal
deleted
inserted
replaced
126 apply (rule add_less_cancel_left [of "-r", THEN iffD1]) |
126 apply (rule add_less_cancel_left [of "-r", THEN iffD1]) |
127 apply (auto intro: mult_pos_pos |
127 apply (auto intro: mult_pos_pos |
128 simp add: add_assoc [symmetric] neg_less_0_iff_less) |
128 simp add: add_assoc [symmetric] neg_less_0_iff_less) |
129 done |
129 done |
130 |
130 |
|
131 lemma real_of_nat_inverse_le_iff: |
|
132 "(inverse (real(Suc n)) \<le> r) = (1 \<le> r * real(Suc n))" |
|
133 by (simp add: inverse_eq_divide pos_divide_le_eq) |
|
134 |
131 lemma real_mult_add_one_minus_ge_zero: |
135 lemma real_mult_add_one_minus_ge_zero: |
132 "0 < r ==> 0 <= r*(1 + -inverse(real (Suc n)))" |
136 "0 < r ==> 0 <= r*(1 + -inverse(real (Suc n)))" |
133 by (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff real_0_le_add_iff) |
137 by (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff real_0_le_add_iff) |
134 |
138 |
135 lemma lemma_nth_realpow_isLub_le: |
139 lemma lemma_nth_realpow_isLub_le: |