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/03fb27c0-444b-43ca-a35c-c02f9984db4d%40googlegroups.com.
