Metamath Proof Explorer

Theorem 2sqreulem3

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

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

Proof

Step Hyp Ref Expression
1 eqeq2 
 |-  ( P = ( ( A ^ 2 ) + ( B ^ 2 ) ) -> ( ( ( A ^ 2 ) + ( C ^ 2 ) ) = P <-> ( ( A ^ 2 ) + ( C ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
2 1 eqcoms 
 |-  ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = P -> ( ( ( A ^ 2 ) + ( C ^ 2 ) ) = P <-> ( ( A ^ 2 ) + ( C ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
3 2 adantl 
 |-  ( ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = P ) -> ( ( ( A ^ 2 ) + ( C ^ 2 ) ) = P <-> ( ( A ^ 2 ) + ( C ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
4 eqcom 
 |-  ( ( ( A ^ 2 ) + ( C ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) <-> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( A ^ 2 ) + ( C ^ 2 ) ) )
5 2sqreulem2 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( A ^ 2 ) + ( C ^ 2 ) ) -> B = C ) )
6 4 5 biimtrid 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) -> ( ( ( A ^ 2 ) + ( C ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) -> B = C ) )
7 6 adantr 
 |-  ( ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = P ) -> ( ( ( A ^ 2 ) + ( C ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) -> B = C ) )
8 3 7 sylbid 
 |-  ( ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = P ) -> ( ( ( A ^ 2 ) + ( C ^ 2 ) ) = P -> B = C ) )
9 8 adantld 
 |-  ( ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = P ) -> ( ( ps /\ ( ( A ^ 2 ) + ( C ^ 2 ) ) = P ) -> B = C ) )
10 9 ex 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = P -> ( ( ps /\ ( ( A ^ 2 ) + ( C ^ 2 ) ) = P ) -> B = C ) ) )
11 10 adantld 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) -> ( ( ph /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = P ) -> ( ( ps /\ ( ( A ^ 2 ) + ( C ^ 2 ) ) = P ) -> B = C ) ) )
12 11 impd 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ C e. NN0 ) -> ( ( ( ph /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = P ) /\ ( ps /\ ( ( A ^ 2 ) + ( C ^ 2 ) ) = P ) ) -> B = C ) )
13 12 3expb 
 |-  ( ( A e. NN0 /\ ( B e. NN0 /\ C e. NN0 ) ) -> ( ( ( ph /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = P ) /\ ( ps /\ ( ( A ^ 2 ) + ( C ^ 2 ) ) = P ) ) -> B = C ) )