Metamath Proof Explorer

Theorem pythagtriplem17

Description: Lemma for pythagtrip . Show the relationship between M , N , and C . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses pythagtriplem15.1 
|- M = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 )
pythagtriplem15.2 
|- N = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 )
Assertion pythagtriplem17 
|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> C = ( ( M ^ 2 ) + ( N ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 pythagtriplem15.1 
 |-  M = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 )
2 pythagtriplem15.2 
 |-  N = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 )
3 1 pythagtriplem12 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( M ^ 2 ) = ( ( C + A ) / 2 ) )
4 2 pythagtriplem14 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( N ^ 2 ) = ( ( C - A ) / 2 ) )
5 3 4 oveq12d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( M ^ 2 ) + ( N ^ 2 ) ) = ( ( ( C + A ) / 2 ) + ( ( C - A ) / 2 ) ) )
6 nncn 
 |-  ( C e. NN -> C e. CC )
7 6 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. CC )
8 7 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> C e. CC )
9 nncn 
 |-  ( A e. NN -> A e. CC )
10 9 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. CC )
11 10 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> A e. CC )
12 8 11 addcld 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( C + A ) e. CC )
13 8 11 subcld 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( C - A ) e. CC )
14 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
15 divdir 
 |-  ( ( ( C + A ) e. CC /\ ( C - A ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( C + A ) + ( C - A ) ) / 2 ) = ( ( ( C + A ) / 2 ) + ( ( C - A ) / 2 ) ) )
16 14 15 mp3an3 
 |-  ( ( ( C + A ) e. CC /\ ( C - A ) e. CC ) -> ( ( ( C + A ) + ( C - A ) ) / 2 ) = ( ( ( C + A ) / 2 ) + ( ( C - A ) / 2 ) ) )
17 12 13 16 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( C + A ) + ( C - A ) ) / 2 ) = ( ( ( C + A ) / 2 ) + ( ( C - A ) / 2 ) ) )
18 5 17 eqtr4d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( M ^ 2 ) + ( N ^ 2 ) ) = ( ( ( C + A ) + ( C - A ) ) / 2 ) )
19 8 11 8 ppncand 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( C + A ) + ( C - A ) ) = ( C + C ) )
20 8 2timesd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( 2 x. C ) = ( C + C ) )
21 19 20 eqtr4d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( C + A ) + ( C - A ) ) = ( 2 x. C ) )
22 21 oveq1d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( C + A ) + ( C - A ) ) / 2 ) = ( ( 2 x. C ) / 2 ) )
23 2cn 
 |-  2 e. CC
24 2ne0 
 |-  2 =/= 0
25 divcan3 
 |-  ( ( C e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. C ) / 2 ) = C )
26 23 24 25 mp3an23 
 |-  ( C e. CC -> ( ( 2 x. C ) / 2 ) = C )
27 8 26 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( 2 x. C ) / 2 ) = C )
28 18 22 27 3eqtrrd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> C = ( ( M ^ 2 ) + ( N ^ 2 ) ) )