Metamath Proof Explorer

Theorem pythagtrip

Description: Parameterize the Pythagorean triples. If A , B , and C are naturals, then they obey the Pythagorean triple formula iff they are parameterized by three naturals. This proof follows the Isabelle proof at http://afp.sourceforge.net/entries/Fermat3_4.shtml . This is Metamath 100 proof #23. (Contributed by Scott Fenton, 19-Apr-2014)

Ref Expression
Assertion pythagtrip 
|- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) <-> E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 divgcdodd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) )
2 1 3adant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) )
3 2 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) )
4 pythagtriplem19 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
5 4 3expia 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( -. 2 || ( A / ( A gcd B ) ) -> E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
6 simp12 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( A gcd B ) ) ) -> B e. NN )
7 simp11 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( A gcd B ) ) ) -> A e. NN )
8 simp13 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( A gcd B ) ) ) -> C e. NN )
9 nnsqcl 
 |-  ( A e. NN -> ( A ^ 2 ) e. NN )
10 9 nncnd 
 |-  ( A e. NN -> ( A ^ 2 ) e. CC )
11 10 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A ^ 2 ) e. CC )
12 nnsqcl 
 |-  ( B e. NN -> ( B ^ 2 ) e. NN )
13 12 nncnd 
 |-  ( B e. NN -> ( B ^ 2 ) e. CC )
14 13 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) e. CC )
15 11 14 addcomd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( B ^ 2 ) + ( A ^ 2 ) ) )
16 15 eqeq1d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) <-> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) ) )
17 16 biimpa 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) )
18 17 3adant3 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( A gcd B ) ) ) -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) )
19 nnz 
 |-  ( A e. NN -> A e. ZZ )
20 19 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. ZZ )
21 nnz 
 |-  ( B e. NN -> B e. ZZ )
22 21 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. ZZ )
23 22 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> B e. ZZ )
24 gcdcom 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) = ( B gcd A ) )
25 20 23 24 syl2an2r 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( A gcd B ) = ( B gcd A ) )
26 25 oveq2d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( B / ( A gcd B ) ) = ( B / ( B gcd A ) ) )
27 26 breq2d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( 2 || ( B / ( A gcd B ) ) <-> 2 || ( B / ( B gcd A ) ) ) )
28 27 notbid 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( -. 2 || ( B / ( A gcd B ) ) <-> -. 2 || ( B / ( B gcd A ) ) ) )
29 28 biimp3a 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( A gcd B ) ) ) -> -. 2 || ( B / ( B gcd A ) ) )
30 pythagtriplem19 
 |-  ( ( ( B e. NN /\ A e. NN /\ C e. NN ) /\ ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( B gcd A ) ) ) -> E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
31 6 7 8 18 29 30 syl311anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( A gcd B ) ) ) -> E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
32 31 3expia 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( -. 2 || ( B / ( A gcd B ) ) -> E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
33 5 32 orim12d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) -> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) ) )
34 3 33 mpd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
35 ovex 
 |-  ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) e. _V
36 ovex 
 |-  ( k x. ( 2 x. ( m x. n ) ) ) e. _V
37 preq12bg 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) e. _V /\ ( k x. ( 2 x. ( m x. n ) ) ) e. _V ) ) -> ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } <-> ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) ) )
38 35 36 37 mpanr12 
 |-  ( ( A e. NN /\ B e. NN ) -> ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } <-> ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) ) )
39 38 anbi1d 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
40 39 rexbidv 
 |-  ( ( A e. NN /\ B e. NN ) -> ( E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> E. k e. NN ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
41 40 2rexbidv 
 |-  ( ( A e. NN /\ B e. NN ) -> ( E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> E. n e. NN E. m e. NN E. k e. NN ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
42 andir 
 |-  ( ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
43 df-3an 
 |-  ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
44 df-3an 
 |-  ( ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
45 43 44 orbi12i 
 |-  ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
46 3ancoma 
 |-  ( ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
47 46 orbi2i 
 |-  ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
48 42 45 47 3bitr2i 
 |-  ( ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
49 48 rexbii 
 |-  ( E. k e. NN ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> E. k e. NN ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
50 49 2rexbii 
 |-  ( E. n e. NN E. m e. NN E. k e. NN ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> E. n e. NN E. m e. NN E. k e. NN ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
51 r19.43 
 |-  ( E. k e. NN ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
52 51 2rexbii 
 |-  ( E. n e. NN E. m e. NN E. k e. NN ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> E. n e. NN E. m e. NN ( E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
53 r19.43 
 |-  ( E. m e. NN ( E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
54 53 rexbii 
 |-  ( E. n e. NN E. m e. NN ( E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> E. n e. NN ( E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
55 r19.43 
 |-  ( E. n e. NN ( E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
56 54 55 bitri 
 |-  ( E. n e. NN E. m e. NN ( E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
57 52 56 bitri 
 |-  ( E. n e. NN E. m e. NN E. k e. NN ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
58 50 57 bitri 
 |-  ( E. n e. NN E. m e. NN E. k e. NN ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
59 41 58 bitrdi 
 |-  ( ( A e. NN /\ B e. NN ) -> ( E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) ) )
60 59 3adant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) ) )
61 60 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) ) )
62 34 61 mpbird 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
63 62 ex 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) -> E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
64 pythagtriplem2 
 |-  ( ( A e. NN /\ B e. NN ) -> ( E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) )
65 64 3adant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) )
66 63 65 impbid 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) <-> E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )