Proving quadratic equation formula without delta with complex coefficients and with complex X

[Filip Cernatescu]

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

 

[Norman Megill]

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

[Mario Carneiro]

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.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e19a3604-756e-458d-9df9-5290b3f73eae%40googlegroups.com.

[Mario Carneiro]

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.