Metamath Proof Explorer

Theorem pythagtriplem18

Description: Lemma for pythagtrip . Wrap the previous M and N up in quantifiers. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion pythagtriplem18 
|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> E. n e. NN E. m e. NN ( A = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ B = ( 2 x. ( m x. n ) ) /\ C = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 )
2 1 pythagtriplem13 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) e. NN )
3 eqid 
 |-  ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 )
4 3 pythagtriplem11 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) e. NN )
5 3 1 pythagtriplem15 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> A = ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) - ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) )
6 3 1 pythagtriplem16 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> B = ( 2 x. ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) ) )
7 3 1 pythagtriplem17 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> C = ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) + ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) )
8 oveq1 
 |-  ( n = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) -> ( n ^ 2 ) = ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) )
9 8 oveq2d 
 |-  ( n = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) -> ( ( m ^ 2 ) - ( n ^ 2 ) ) = ( ( m ^ 2 ) - ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) )
10 9 eqeq2d 
 |-  ( n = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) -> ( A = ( ( m ^ 2 ) - ( n ^ 2 ) ) <-> A = ( ( m ^ 2 ) - ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) ) )
11 oveq2 
 |-  ( n = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) -> ( m x. n ) = ( m x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) )
12 11 oveq2d 
 |-  ( n = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) -> ( 2 x. ( m x. n ) ) = ( 2 x. ( m x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) ) )
13 12 eqeq2d 
 |-  ( n = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) -> ( B = ( 2 x. ( m x. n ) ) <-> B = ( 2 x. ( m x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) ) ) )
14 8 oveq2d 
 |-  ( n = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) -> ( ( m ^ 2 ) + ( n ^ 2 ) ) = ( ( m ^ 2 ) + ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) )
15 14 eqeq2d 
 |-  ( n = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) -> ( C = ( ( m ^ 2 ) + ( n ^ 2 ) ) <-> C = ( ( m ^ 2 ) + ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) ) )
16 10 13 15 3anbi123d 
 |-  ( n = ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) -> ( ( A = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ B = ( 2 x. ( m x. n ) ) /\ C = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) <-> ( A = ( ( m ^ 2 ) - ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) /\ B = ( 2 x. ( m x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) ) /\ C = ( ( m ^ 2 ) + ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) ) ) )
17 oveq1 
 |-  ( m = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) -> ( m ^ 2 ) = ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) )
18 17 oveq1d 
 |-  ( m = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) -> ( ( m ^ 2 ) - ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) = ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) - ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) )
19 18 eqeq2d 
 |-  ( m = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) -> ( A = ( ( m ^ 2 ) - ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) <-> A = ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) - ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) ) )
20 oveq1 
 |-  ( m = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) -> ( m x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) = ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) )
21 20 oveq2d 
 |-  ( m = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) -> ( 2 x. ( m x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) ) = ( 2 x. ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) ) )
22 21 eqeq2d 
 |-  ( m = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) -> ( B = ( 2 x. ( m x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) ) <-> B = ( 2 x. ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) ) ) )
23 17 oveq1d 
 |-  ( m = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) -> ( ( m ^ 2 ) + ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) = ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) + ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) )
24 23 eqeq2d 
 |-  ( m = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) -> ( C = ( ( m ^ 2 ) + ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) <-> C = ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) + ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) ) )
25 19 22 24 3anbi123d 
 |-  ( m = ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) -> ( ( A = ( ( m ^ 2 ) - ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) /\ B = ( 2 x. ( m x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) ) /\ C = ( ( m ^ 2 ) + ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) ) <-> ( A = ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) - ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) /\ B = ( 2 x. ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) ) /\ C = ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) + ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) ) ) )
26 16 25 rspc2ev 
 |-  ( ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) e. NN /\ ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) e. NN /\ ( A = ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) - ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) /\ B = ( 2 x. ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) x. ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ) ) /\ C = ( ( ( ( ( sqrt ` ( C + B ) ) + ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) + ( ( ( ( sqrt ` ( C + B ) ) - ( sqrt ` ( C - B ) ) ) / 2 ) ^ 2 ) ) ) ) -> E. n e. NN E. m e. NN ( A = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ B = ( 2 x. ( m x. n ) ) /\ C = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) )
27 2 4 5 6 7 26 syl113anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> E. n e. NN E. m e. NN ( A = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ B = ( 2 x. ( m x. n ) ) /\ C = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) )