Metamath Proof Explorer

Theorem pythagtriplem15

Description: Lemma for pythagtrip . Show the relationship between M , N , and A . (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 pythagtriplem15 
|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> A = ( ( 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 simp3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. NN )
7 simp1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. NN )
8 6 7 nnaddcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + A ) e. NN )
9 8 nncnd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C + A ) e. CC )
10 9 3ad2ant1 
 |-  ( ( ( 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 )
11 nnz 
 |-  ( C e. NN -> C e. ZZ )
12 11 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. ZZ )
13 nnz 
 |-  ( A e. NN -> A e. ZZ )
14 13 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. ZZ )
15 12 14 zsubcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C - A ) e. ZZ )
16 15 zcnd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C - A ) e. CC )
17 16 3ad2ant1 
 |-  ( ( ( 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 )
18 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
19 divsubdir 
 |-  ( ( ( C + A ) e. CC /\ ( C - A ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( C + A ) - ( C - A ) ) / 2 ) = ( ( ( C + A ) / 2 ) - ( ( C - A ) / 2 ) ) )
20 18 19 mp3an3 
 |-  ( ( ( C + A ) e. CC /\ ( C - A ) e. CC ) -> ( ( ( C + A ) - ( C - A ) ) / 2 ) = ( ( ( C + A ) / 2 ) - ( ( C - A ) / 2 ) ) )
21 10 17 20 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 ) ) )
22 5 21 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 ) )
23 nncn 
 |-  ( C e. NN -> C e. CC )
24 23 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. CC )
25 24 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 )
26 nncn 
 |-  ( A e. NN -> A e. CC )
27 26 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. CC )
28 27 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 )
29 25 28 28 pnncand 
 |-  ( ( ( 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 ) ) = ( A + A ) )
30 28 2timesd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( 2 x. A ) = ( A + A ) )
31 29 30 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. A ) )
32 31 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. A ) / 2 ) )
33 2cn 
 |-  2 e. CC
34 2ne0 
 |-  2 =/= 0
35 divcan3 
 |-  ( ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. A ) / 2 ) = A )
36 33 34 35 mp3an23 
 |-  ( A e. CC -> ( ( 2 x. A ) / 2 ) = A )
37 28 36 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( 2 x. A ) / 2 ) = A )
38 22 32 37 3eqtrrd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> A = ( ( M ^ 2 ) - ( N ^ 2 ) ) )