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.
