equal
deleted
inserted
replaced
571 ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n |
571 ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n |
572 @= hypreal_of_real pi" |
572 @= hypreal_of_real pi" |
573 apply (frule STAR_sin_Infinitesimal_divide |
573 apply (frule STAR_sin_Infinitesimal_divide |
574 [OF Infinitesimal_pi_divide_HNatInfinite |
574 [OF Infinitesimal_pi_divide_HNatInfinite |
575 pi_divide_HNatInfinite_not_zero]) |
575 pi_divide_HNatInfinite_not_zero]) |
576 apply (auto simp add: hypreal_inverse_distrib) |
576 apply (auto simp add: inverse_mult_distrib) |
577 apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"]) |
577 apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"]) |
578 apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac) |
578 apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac) |
579 done |
579 done |
580 |
580 |
581 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2: |
581 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2: |