Metamath Proof Explorer

Theorem pythagtriplem19

Description: Lemma for pythagtrip . Introduce k and remove the relative primality requirement. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 gcdnncl 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. NN )
2 1 3adant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) e. NN )
3 2 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( A gcd B ) e. NN )
4 nnz 
 |-  ( A e. NN -> A e. ZZ )
5 nnz 
 |-  ( B e. NN -> B e. ZZ )
6 gcddvds 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
7 4 5 6 syl2an 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
8 7 3adant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
9 8 simpld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) || A )
10 2 nnzd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) e. ZZ )
11 2 nnne0d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) =/= 0 )
12 4 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. ZZ )
13 dvdsval2 
 |-  ( ( ( A gcd B ) e. ZZ /\ ( A gcd B ) =/= 0 /\ A e. ZZ ) -> ( ( A gcd B ) || A <-> ( A / ( A gcd B ) ) e. ZZ ) )
14 10 11 12 13 syl3anc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || A <-> ( A / ( A gcd B ) ) e. ZZ ) )
15 9 14 mpbid 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A / ( A gcd B ) ) e. ZZ )
16 nnre 
 |-  ( A e. NN -> A e. RR )
17 16 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. RR )
18 2 nnred 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) e. RR )
19 nngt0 
 |-  ( A e. NN -> 0 < A )
20 19 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < A )
21 2 nngt0d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < ( A gcd B ) )
22 17 18 20 21 divgt0d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < ( A / ( A gcd B ) ) )
23 elnnz 
 |-  ( ( A / ( A gcd B ) ) e. NN <-> ( ( A / ( A gcd B ) ) e. ZZ /\ 0 < ( A / ( A gcd B ) ) ) )
24 15 22 23 sylanbrc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A / ( A gcd B ) ) e. NN )
25 24 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( A / ( A gcd B ) ) e. NN )
26 8 simprd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) || B )
27 5 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. ZZ )
28 dvdsval2 
 |-  ( ( ( A gcd B ) e. ZZ /\ ( A gcd B ) =/= 0 /\ B e. ZZ ) -> ( ( A gcd B ) || B <-> ( B / ( A gcd B ) ) e. ZZ ) )
29 10 11 27 28 syl3anc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || B <-> ( B / ( A gcd B ) ) e. ZZ ) )
30 26 29 mpbid 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B / ( A gcd B ) ) e. ZZ )
31 nnre 
 |-  ( B e. NN -> B e. RR )
32 31 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. RR )
33 nngt0 
 |-  ( B e. NN -> 0 < B )
34 33 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < B )
35 32 18 34 21 divgt0d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < ( B / ( A gcd B ) ) )
36 elnnz 
 |-  ( ( B / ( A gcd B ) ) e. NN <-> ( ( B / ( A gcd B ) ) e. ZZ /\ 0 < ( B / ( A gcd B ) ) ) )
37 30 35 36 sylanbrc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B / ( A gcd B ) ) e. NN )
38 37 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( B / ( A gcd B ) ) e. NN )
39 dvdssq 
 |-  ( ( ( A gcd B ) e. ZZ /\ A e. ZZ ) -> ( ( A gcd B ) || A <-> ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) ) )
40 10 12 39 syl2anc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || A <-> ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) ) )
41 dvdssq 
 |-  ( ( ( A gcd B ) e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || B <-> ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) )
42 10 27 41 syl2anc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || B <-> ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) )
43 40 42 anbi12d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A gcd B ) || A /\ ( A gcd B ) || B ) <-> ( ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) /\ ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) ) )
44 8 43 mpbid 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) /\ ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) )
45 2 nnsqcld 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) ^ 2 ) e. NN )
46 45 nnzd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) ^ 2 ) e. ZZ )
47 nnsqcl 
 |-  ( A e. NN -> ( A ^ 2 ) e. NN )
48 47 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A ^ 2 ) e. NN )
49 48 nnzd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A ^ 2 ) e. ZZ )
50 nnsqcl 
 |-  ( B e. NN -> ( B ^ 2 ) e. NN )
51 50 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) e. NN )
52 51 nnzd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) e. ZZ )
53 dvds2add 
 |-  ( ( ( ( A gcd B ) ^ 2 ) e. ZZ /\ ( A ^ 2 ) e. ZZ /\ ( B ^ 2 ) e. ZZ ) -> ( ( ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) /\ ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) -> ( ( A gcd B ) ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
54 46 49 52 53 syl3anc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) /\ ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) -> ( ( A gcd B ) ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
55 44 54 mpd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) )
56 55 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( A gcd B ) ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) )
57 simpr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
58 56 57 breqtrd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( A gcd B ) ^ 2 ) || ( C ^ 2 ) )
59 nnz 
 |-  ( C e. NN -> C e. ZZ )
60 59 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. ZZ )
61 dvdssq 
 |-  ( ( ( A gcd B ) e. ZZ /\ C e. ZZ ) -> ( ( A gcd B ) || C <-> ( ( A gcd B ) ^ 2 ) || ( C ^ 2 ) ) )
62 10 60 61 syl2anc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || C <-> ( ( A gcd B ) ^ 2 ) || ( C ^ 2 ) ) )
63 62 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( A gcd B ) || C <-> ( ( A gcd B ) ^ 2 ) || ( C ^ 2 ) ) )
64 58 63 mpbird 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( A gcd B ) || C )
65 dvdsval2 
 |-  ( ( ( A gcd B ) e. ZZ /\ ( A gcd B ) =/= 0 /\ C e. ZZ ) -> ( ( A gcd B ) || C <-> ( C / ( A gcd B ) ) e. ZZ ) )
66 10 11 60 65 syl3anc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || C <-> ( C / ( A gcd B ) ) e. ZZ ) )
67 66 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( A gcd B ) || C <-> ( C / ( A gcd B ) ) e. ZZ ) )
68 64 67 mpbid 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( C / ( A gcd B ) ) e. ZZ )
69 nnre 
 |-  ( C e. NN -> C e. RR )
70 69 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. RR )
71 nngt0 
 |-  ( C e. NN -> 0 < C )
72 71 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < C )
73 70 18 72 21 divgt0d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < ( C / ( A gcd B ) ) )
74 73 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> 0 < ( C / ( A gcd B ) ) )
75 elnnz 
 |-  ( ( C / ( A gcd B ) ) e. NN <-> ( ( C / ( A gcd B ) ) e. ZZ /\ 0 < ( C / ( A gcd B ) ) ) )
76 68 74 75 sylanbrc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( C / ( A gcd B ) ) e. NN )
77 76 3adant3 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( C / ( A gcd B ) ) e. NN )
78 48 nncnd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A ^ 2 ) e. CC )
79 51 nncnd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) e. CC )
80 45 nncnd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) ^ 2 ) e. CC )
81 45 nnne0d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) ^ 2 ) =/= 0 )
82 78 79 80 81 divdird 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A gcd B ) ^ 2 ) ) = ( ( ( A ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) + ( ( B ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) ) )
83 82 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A gcd B ) ^ 2 ) ) = ( ( ( A ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) + ( ( B ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) ) )
84 nncn 
 |-  ( C e. NN -> C e. CC )
85 84 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. CC )
86 2 nncnd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) e. CC )
87 85 86 11 sqdivd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( C / ( A gcd B ) ) ^ 2 ) = ( ( C ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) )
88 87 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( C / ( A gcd B ) ) ^ 2 ) = ( ( C ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) )
89 oveq1 
 |-  ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A gcd B ) ^ 2 ) ) = ( ( C ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) )
90 89 3ad2ant2 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A gcd B ) ^ 2 ) ) = ( ( C ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) )
91 88 90 eqtr4d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( C / ( A gcd B ) ) ^ 2 ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A gcd B ) ^ 2 ) ) )
92 nncn 
 |-  ( A e. NN -> A e. CC )
93 92 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. CC )
94 93 86 11 sqdivd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A / ( A gcd B ) ) ^ 2 ) = ( ( A ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) )
95 nncn 
 |-  ( B e. NN -> B e. CC )
96 95 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. CC )
97 96 86 11 sqdivd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( B / ( A gcd B ) ) ^ 2 ) = ( ( B ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) )
98 94 97 oveq12d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A / ( A gcd B ) ) ^ 2 ) + ( ( B / ( A gcd B ) ) ^ 2 ) ) = ( ( ( A ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) + ( ( B ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) ) )
99 98 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( ( A / ( A gcd B ) ) ^ 2 ) + ( ( B / ( A gcd B ) ) ^ 2 ) ) = ( ( ( A ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) + ( ( B ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) ) )
100 83 91 99 3eqtr4rd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( ( A / ( A gcd B ) ) ^ 2 ) + ( ( B / ( A gcd B ) ) ^ 2 ) ) = ( ( C / ( A gcd B ) ) ^ 2 ) )
101 gcddiv 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( A gcd B ) e. NN ) /\ ( ( A gcd B ) || A /\ ( A gcd B ) || B ) ) -> ( ( A gcd B ) / ( A gcd B ) ) = ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) )
102 12 27 2 8 101 syl31anc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) / ( A gcd B ) ) = ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) )
103 86 11 dividd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) / ( A gcd B ) ) = 1 )
104 102 103 eqtr3d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 )
105 104 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 )
106 simp3 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> -. 2 || ( A / ( A gcd B ) ) )
107 pythagtriplem18 
 |-  ( ( ( ( A / ( A gcd B ) ) e. NN /\ ( B / ( A gcd B ) ) e. NN /\ ( C / ( A gcd B ) ) e. NN ) /\ ( ( ( A / ( A gcd B ) ) ^ 2 ) + ( ( B / ( A gcd B ) ) ^ 2 ) ) = ( ( C / ( A gcd B ) ) ^ 2 ) /\ ( ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 /\ -. 2 || ( A / ( A gcd B ) ) ) ) -> E. n e. NN E. m e. NN ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) )
108 25 38 77 100 105 106 107 syl312anc 
 |-  ( ( ( 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 ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) )
109 93 86 11 divcan2d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) = A )
110 109 eqcomd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A = ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) )
111 96 86 11 divcan2d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) = B )
112 111 eqcomd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B = ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) )
113 85 86 11 divcan2d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) = C )
114 113 eqcomd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C = ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) )
115 110 112 114 3jca 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A = ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) /\ B = ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) /\ C = ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) ) )
116 115 3ad2ant1 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( A = ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) /\ B = ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) /\ C = ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) ) )
117 oveq2 
 |-  ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) -> ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) )
118 117 eqeq2d 
 |-  ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) -> ( A = ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) <-> A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) )
119 118 3ad2ant1 
 |-  ( ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> ( A = ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) <-> A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) )
120 oveq2 
 |-  ( ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) -> ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) )
121 120 eqeq2d 
 |-  ( ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) -> ( B = ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) <-> B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) ) )
122 121 3ad2ant2 
 |-  ( ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> ( B = ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) <-> B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) ) )
123 oveq2 
 |-  ( ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) -> ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) )
124 123 eqeq2d 
 |-  ( ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) -> ( C = ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) <-> C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
125 124 3ad2ant3 
 |-  ( ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> ( C = ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) <-> C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
126 119 122 125 3anbi123d 
 |-  ( ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> ( ( A = ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) /\ B = ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) /\ C = ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) ) <-> ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
127 116 126 syl5ibcom 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
128 127 reximdv 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( E. m e. NN ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> E. m e. NN ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
129 128 reximdv 
 |-  ( ( ( 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 ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> E. n e. NN E. m e. NN ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
130 108 129 mpd 
 |-  ( ( ( 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 ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
131 oveq1 
 |-  ( k = ( A gcd B ) -> ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) )
132 131 eqeq2d 
 |-  ( k = ( A gcd B ) -> ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) <-> A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) )
133 oveq1 
 |-  ( k = ( A gcd B ) -> ( k x. ( 2 x. ( m x. n ) ) ) = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) )
134 133 eqeq2d 
 |-  ( k = ( A gcd B ) -> ( B = ( k x. ( 2 x. ( m x. n ) ) ) <-> B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) ) )
135 oveq1 
 |-  ( k = ( A gcd B ) -> ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) )
136 135 eqeq2d 
 |-  ( k = ( A gcd B ) -> ( C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) <-> C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
137 132 134 136 3anbi123d 
 |-  ( k = ( A gcd B ) -> ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
138 137 2rexbidv 
 |-  ( k = ( A gcd B ) -> ( E. n e. NN E. m 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 ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
139 138 rspcev 
 |-  ( ( ( A gcd B ) e. NN /\ E. n e. NN E. m e. NN ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) -> E. k e. NN E. n e. NN E. m e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
140 3 130 139 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> E. k e. NN E. n e. NN E. m e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
141 rexcom 
 |-  ( E. k e. NN E. n e. NN E. m 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. k e. NN E. m e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
142 rexcom 
 |-  ( E. k e. NN E. m 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. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
143 142 rexbii 
 |-  ( E. n e. NN E. k e. NN E. m 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. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
144 141 143 bitri 
 |-  ( E. k e. NN E. n e. NN E. m 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. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
145 140 144 sylib 
 |-  ( ( ( 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 ) ) ) ) )