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/CAFXXJSsWShob-U3rqm3LbopFOiLym1b2Zdo6fQ2a4roqW2giUw%40mail.gmail.com.
