Metamath Proof Explorer

Theorem pythagtriplem2

Description: Lemma for pythagtrip . Prove the full version of one direction of the theorem. (Contributed by Scott Fenton, 28-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) e. _V
2 ovex 
 |-  ( k x. ( 2 x. ( m x. n ) ) ) e. _V
3 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 ) ) ) ) ) ) )
4 1 2 3 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 ) ) ) ) ) ) )
5 4 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 ) ) ) ) ) )
6 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 ) ) ) ) ) )
7 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 ) ) ) ) )
8 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 ) ) ) ) )
9 7 8 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 ) ) ) ) ) )
10 6 9 bitr4i 
 |-  ( ( ( ( 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 ) ) ) ) ) )
11 5 10 bitrdi 
 |-  ( ( 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 ) ) ) /\ 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 ) ) ) ) ) ) )
12 11 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 ) ) ) /\ 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 ) ) ) ) ) ) )
13 12 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 ) ) ) /\ 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 ) ) ) ) ) ) )
14 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 ) ) ) ) \/ ( 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 ) ) ) ) \/ E. k e. NN ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
15 14 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 ) ) ) ) \/ ( 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. k e. NN ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
16 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 ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ 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 ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
17 16 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 ( 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. m e. NN E. k e. NN ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
18 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 ( 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 ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
19 15 17 18 3bitri 
 |-  ( 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 ) ) ) ) \/ ( 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 ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
20 13 19 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 ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) ) )
21 pythagtriplem1 
 |-  ( 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 ) ) ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
22 21 a1i 
 |-  ( ( A e. NN /\ B e. NN ) -> ( 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 ) ) ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) )
23 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 ) ) ) ) )
24 23 rexbii 
 |-  ( E. k e. NN ( 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 ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
25 24 2rexbii 
 |-  ( E. n e. NN E. m e. NN E. k e. NN ( 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 ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
26 pythagtriplem1 
 |-  ( 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 ) ) ) ) -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) )
27 25 26 sylbi 
 |-  ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) )
28 nncn 
 |-  ( A e. NN -> A e. CC )
29 28 sqcld 
 |-  ( A e. NN -> ( A ^ 2 ) e. CC )
30 nncn 
 |-  ( B e. NN -> B e. CC )
31 30 sqcld 
 |-  ( B e. NN -> ( B ^ 2 ) e. CC )
32 addcom 
 |-  ( ( ( A ^ 2 ) e. CC /\ ( B ^ 2 ) e. CC ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( B ^ 2 ) + ( A ^ 2 ) ) )
33 29 31 32 syl2an 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( B ^ 2 ) + ( A ^ 2 ) ) )
34 33 eqeq1d 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) <-> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) ) )
35 27 34 syl5ibr 
 |-  ( ( A e. NN /\ B e. NN ) -> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) )
36 22 35 jaod 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( 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 ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) )
37 20 36 sylbid 
 |-  ( ( 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 ) ) )