equal
deleted
inserted
replaced
6595 fix e :: real |
6595 fix e :: real |
6596 assume "e > 0" |
6596 assume "e > 0" |
6597 then have "\<exists>N::nat. inverse (real (N + 1)) < e" |
6597 then have "\<exists>N::nat. inverse (real (N + 1)) < e" |
6598 using real_arch_inv[of e] |
6598 using real_arch_inv[of e] |
6599 apply (auto simp add: Suc_pred') |
6599 apply (auto simp add: Suc_pred') |
6600 apply (rule_tac x="n - 1" in exI) |
6600 apply (metis Suc_pred' real_of_nat_Suc) |
6601 apply auto |
|
6602 done |
6601 done |
6603 then obtain N :: nat where "inverse (real (N + 1)) < e" |
6602 then obtain N :: nat where "inverse (real (N + 1)) < e" |
6604 by auto |
6603 by auto |
6605 then have "\<forall>n\<ge>N. inverse (real n + 1) < e" |
6604 then have "\<forall>n\<ge>N. inverse (real n + 1) < e" |
6606 apply auto |
6605 apply auto |