equal
deleted
inserted
replaced
4641 apply (insert LIM_cos_div_sin) |
4641 apply (insert LIM_cos_div_sin) |
4642 apply (simp only: LIM_eq) |
4642 apply (simp only: LIM_eq) |
4643 apply (drule_tac x = "inverse y" in spec) |
4643 apply (drule_tac x = "inverse y" in spec) |
4644 apply safe |
4644 apply safe |
4645 apply force |
4645 apply force |
4646 apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero]) |
4646 apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] field_lbound_gt_zero]) |
4647 apply safe |
4647 apply safe |
4648 apply (rule_tac x = "(pi/2) - e" in exI) |
4648 apply (rule_tac x = "(pi/2) - e" in exI) |
4649 apply (simp (no_asm_simp)) |
4649 apply (simp (no_asm_simp)) |
4650 apply (drule_tac x = "(pi/2) - e" in spec) |
4650 apply (drule_tac x = "(pi/2) - e" in spec) |
4651 apply (auto simp add: tan_def sin_diff cos_diff) |
4651 apply (auto simp add: tan_def sin_diff cos_diff) |