Metamath Proof Explorer

Theorem eqsqrtor

Description: Solve an equation containing a square. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion eqsqrtor 
|- ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) = B <-> ( A = ( sqrt ` B ) \/ A = -u ( sqrt ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 sqrtth 
 |-  ( B e. CC -> ( ( sqrt ` B ) ^ 2 ) = B )
2 1 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sqrt ` B ) ^ 2 ) = B )
3 2 eqeq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) = ( ( sqrt ` B ) ^ 2 ) <-> ( A ^ 2 ) = B ) )
4 sqrtcl 
 |-  ( B e. CC -> ( sqrt ` B ) e. CC )
5 sqeqor 
 |-  ( ( A e. CC /\ ( sqrt ` B ) e. CC ) -> ( ( A ^ 2 ) = ( ( sqrt ` B ) ^ 2 ) <-> ( A = ( sqrt ` B ) \/ A = -u ( sqrt ` B ) ) ) )
6 4 5 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) = ( ( sqrt ` B ) ^ 2 ) <-> ( A = ( sqrt ` B ) \/ A = -u ( sqrt ` B ) ) ) )
7 3 6 bitr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) = B <-> ( A = ( sqrt ` B ) \/ A = -u ( sqrt ` B ) ) ) )