Metamath Proof Explorer

Theorem 2sqreulem2

Description: Lemma 2 for 2sqreu etc. (Contributed by AV, 25-Jun-2023)

Ref Expression
Assertion 2sqreulem2 
|- ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( A ^ 2 ) + ( C ^ 2 ) ) -> B = C ) )

Proof

Step Hyp Ref Expression
1 nn0cn 
 |-  ( A e. NN0 -> A e. CC )
2 1 sqcld 
 |-  ( A e. NN0 -> ( A ^ 2 ) e. CC )
3 2 3ad2ant1 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) -> ( A ^ 2 ) e. CC )
4 nn0cn 
 |-  ( B e. NN0 -> B e. CC )
5 4 sqcld 
 |-  ( B e. NN0 -> ( B ^ 2 ) e. CC )
6 5 3ad2ant2 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) -> ( B ^ 2 ) e. CC )
7 nn0cn 
 |-  ( C e. NN0 -> C e. CC )
8 7 sqcld 
 |-  ( C e. NN0 -> ( C ^ 2 ) e. CC )
9 8 3ad2ant3 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) -> ( C ^ 2 ) e. CC )
10 3 6 9 addcand 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( A ^ 2 ) + ( C ^ 2 ) ) <-> ( B ^ 2 ) = ( C ^ 2 ) ) )
11 nn0sq11 
 |-  ( ( B e. NN0 /\ C e. NN0 ) -> ( ( B ^ 2 ) = ( C ^ 2 ) <-> B = C ) )
12 11 biimpd 
 |-  ( ( B e. NN0 /\ C e. NN0 ) -> ( ( B ^ 2 ) = ( C ^ 2 ) -> B = C ) )
13 12 3adant1 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) -> ( ( B ^ 2 ) = ( C ^ 2 ) -> B = C ) )
14 10 13 sylbid 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( A ^ 2 ) + ( C ^ 2 ) ) -> B = C ) )