To be more specific, the theorems ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) ( sqr ` ( A / B ) ) = ( ( sqr ` A ) / ( sqr ` B ) )
only hold for a subset of the complex numbers. If B is real then it's true, but the exact region where this holds is complicated because of the position of the branch cuts. What can be said is that ( ( sqr ` A ) / ( sqr ` B ) ) is *a* square root of ( A / B ), meaning that it is either equal to ( sqr ` ( A / B ) ) or -u ( sqr ` ( A / B ) ), but that's a difficult algebraic condition to work with. Instead I recommend keeping it squared until you are ready to introduce the branch cut sqr and its negative, via the theorem A = B^2 <-> B = (sqr`A) \/ B = -u (sqr`A) . This is how quad is proved: the key step is (((((2 ยท ๐ด) ยท ๐) โ -๐ต)โ2) = (๐ทโ2) โ ((((2 ยท ๐ด) ยท ๐) โ -๐ต) = ๐ท โจ (((2 ยท ๐ด) ยท ๐) โ -๐ต) = -๐ท)) where D is (any) square root of the discriminant. On Sun, Jun 30, 2019 at 7:59 AM Mario Carneiro <[email protected]> wrote: > The square root does not distribute over division in general. You should > try not to introduce the square root until you have the desired expression > already under the square root. > > By the way, it looks like you are proving theorem quad. Depending on your > goals you could either use that theorem or use it as a template for your > theorem. > > On Sat, Jun 29, 2019 at 7:22 PM Norman Megill <[email protected]> wrote: > >> I, too, am puzzled by this. My initial though was that maybe it could be >> done via complex exponentiation, which relates to the sqr function for all >> complex numbers via ~ cxpsqr. However, ~ divcxp accepts only nonnegative >> real arguments for the ratio terms (although the exponent can be complex). >> Does anyone know what the issues are that require this limitation? >> >> Norm >> >> On Wednesday, June 26, 2019 at 1:55:03 PM UTC-4, Filip Cernatescu wrote: >>> >>> I have started from (( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0 >>> and I have followed the classical math proof and >>> I have arrived at: >>> >>> ( ( X + ( B / ( 2 x. A ) ) ) = ( sqr ` ( ( ( B ^ 2 ) - ( 4 x. ( A x. C ) >>> ) ) / ( ( 2 x. A ) ^ 2 ) ) ) \/ ( X + ( B / ( 2 x. A ) ) ) = -u ( sqr ` ( ( >>> ( B ^ 2 ) - ( 4 x. >>> >>> ( A x. C ) ) ) / ( ( 2 x. A ) ^ 2 ) ) ) ) >>> >>> The problem is the distribution of square root over division(requires >>> real not complex): >>> >>> sqrdiv ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> >>> ( sqr ` ( A / B ) ) = ( ( sqr ` A ) / ( sqr ` B ) ) ) >>> >>> >>> Thank you very much!!! >>> >>> Filip >>> >>> >>> >>> >>> >>> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/e19a3604-756e-458d-9df9-5290b3f73eae%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/e19a3604-756e-458d-9df9-5290b3f73eae%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStc5PNquPey-6FTH9gN3aw7QaUCtiK0e-CJ4xAZkMv6-g%40mail.gmail.com.
