equal
deleted
inserted
replaced
1287 next |
1287 next |
1288 assume "0 \<le> x" and "x \<noteq> 0" |
1288 assume "0 \<le> x" and "x \<noteq> 0" |
1289 hence x0: "0 < x" by simp |
1289 hence x0: "0 < x" by simp |
1290 assume x1: "x < 1" |
1290 assume x1: "x < 1" |
1291 from x0 x1 have "1 < inverse x" |
1291 from x0 x1 have "1 < inverse x" |
1292 by (rule real_inverse_gt_one) |
1292 by (rule one_less_inverse) |
1293 hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0" |
1293 hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0" |
1294 by (rule LIMSEQ_inverse_realpow_zero) |
1294 by (rule LIMSEQ_inverse_realpow_zero) |
1295 thus ?thesis by (simp add: power_inverse) |
1295 thus ?thesis by (simp add: power_inverse) |
1296 qed |
1296 qed |
1297 |
1297 |