equal
deleted
inserted
replaced
695 have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith |
695 have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith |
696 thus ?thesis by (simp add: ring_simps power2_eq_square) |
696 thus ?thesis by (simp add: ring_simps power2_eq_square) |
697 qed |
697 qed |
698 |
698 |
699 lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y - x) < d \<longrightarrow> abs(y * y - x * x) < e)" |
699 lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y - x) < d \<longrightarrow> abs(y * y - x * x) < e)" |
700 using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_def, rule_format, of e x] apply (auto simp add: power2_eq_square) |
700 using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_eq, rule_format, of e x] apply (auto simp add: power2_eq_square) |
701 apply (rule_tac x="s" in exI) |
701 apply (rule_tac x="s" in exI) |
702 apply auto |
702 apply auto |
703 apply (erule_tac x=y in allE) |
703 apply (erule_tac x=y in allE) |
704 apply auto |
704 apply auto |
705 done |
705 done |