Step Hyp Ref
Expression 1 nnz 10911 . . . . . . 7
2 nnz 10911 . . . . . . 7
3 1 , 2 anim12i 566 . . . . . 6
4 nnne0 10593 . . . . . . . . 9
5 4 neneqd 2659 . . . . . . . 8
6 5 intnanrd 917 . . . . . . 7
7 6 adantr 465 . . . . . 6
8 gcdn0cl 14152 . . . . . 6
9 3 , 7 , 8 syl2anc 661 . . . . 5
10 9 3adant3 1016 . . . 4
11 10 3ad2ant1 1017 . . 3
12 gcddvds 14153 . . . . . . . . . . 11
13 1 , 2 , 12 syl2an 477 . . . . . . . . . 10
14 13 3adant3 1016 . . . . . . . . 9
15 14 simpld 459 . . . . . . . 8
16 10 nnzd 10993 . . . . . . . . 9
17 10 nnne0d 10605 . . . . . . . . 9
18 1 3ad2ant1 1017 . . . . . . . . 9
19 dvdsval2 13989 . . . . . . . . 9
20 16 , 17 , 18 , 19 syl3anc 1228 . . . . . . . 8
21 15 , 20 mpbid 210 . . . . . . 7
22 nnre 10568 . . . . . . . . 9
23 22 3ad2ant1 1017 . . . . . . . 8
24 10 nnred 10576 . . . . . . . 8
25 nngt0 10590 . . . . . . . . 9
26 25 3ad2ant1 1017 . . . . . . . 8
27 10 nngt0d 10604 . . . . . . . 8
28 23 , 24 , 26 , 27 divgt0d 10506 . . . . . . 7
29 elnnz 10899 . . . . . . 7
30 21 , 28 , 29 sylanbrc 664 . . . . . 6
31 30 3ad2ant1 1017 . . . . 5
32 14 simprd 463 . . . . . . . 8
33 2 3ad2ant2 1018 . . . . . . . . 9
34 dvdsval2 13989 . . . . . . . . 9
35 16 , 17 , 33 , 34 syl3anc 1228 . . . . . . . 8
36 32 , 35 mpbid 210 . . . . . . 7
37 nnre 10568 . . . . . . . . 9
38 37 3ad2ant2 1018 . . . . . . . 8
39 nngt0 10590 . . . . . . . . 9
40 39 3ad2ant2 1018 . . . . . . . 8
41 38 , 24 , 40 , 27 divgt0d 10506 . . . . . . 7
42 elnnz 10899 . . . . . . 7
43 36 , 41 , 42 sylanbrc 664 . . . . . 6
44 43 3ad2ant1 1017 . . . . 5
45 dvdssq 14198 . . . . . . . . . . . . . . 15
46 16 , 18 , 45 syl2anc 661 . . . . . . . . . . . . . 14
47 dvdssq 14198 . . . . . . . . . . . . . . 15
48 16 , 33 , 47 syl2anc 661 . . . . . . . . . . . . . 14
49 46 , 48 anbi12d 710 . . . . . . . . . . . . 13
50 14 , 49 mpbid 210 . . . . . . . . . . . 12
51 10 nnsqcld 12330 . . . . . . . . . . . . . 14
52 51 nnzd 10993 . . . . . . . . . . . . 13
53 nnsqcl 12237 . . . . . . . . . . . . . . 15
54 53 3ad2ant1 1017 . . . . . . . . . . . . . 14
55 54 nnzd 10993 . . . . . . . . . . . . 13
56 nnsqcl 12237 . . . . . . . . . . . . . . 15
57 56 3ad2ant2 1018 . . . . . . . . . . . . . 14
58 57 nnzd 10993 . . . . . . . . . . . . 13
59 dvds2add 14015 . . . . . . . . . . . . 13
60 52 , 55 , 58 , 59 syl3anc 1228 . . . . . . . . . . . 12
61 50 , 60 mpd 15 . . . . . . . . . . 11
62 61 adantr 465 . . . . . . . . . 10
63 simpr 461 . . . . . . . . . 10
64 62 , 63 breqtrd 4476 . . . . . . . . 9
65 nnz 10911 . . . . . . . . . . . 12
66 65 3ad2ant3 1019 . . . . . . . . . . 11
67 dvdssq 14198 . . . . . . . . . . 11
68 16 , 66 , 67 syl2anc 661 . . . . . . . . . 10
69 68 adantr 465 . . . . . . . . 9
70 64 , 69 mpbird 232 . . . . . . . 8
71 dvdsval2 13989 . . . . . . . . . 10
72 16 , 17 , 66 , 71 syl3anc 1228 . . . . . . . . 9
73 72 adantr 465 . . . . . . . 8
74 70 , 73 mpbid 210 . . . . . . 7
75 nnre 10568 . . . . . . . . . 10
76 75 3ad2ant3 1019 . . . . . . . . 9
77 nngt0 10590 . . . . . . . . . 10
78 77 3ad2ant3 1019 . . . . . . . . 9
79 76 , 24 , 78 , 27 divgt0d 10506 . . . . . . . 8
80 79 adantr 465 . . . . . . 7
81 elnnz 10899 . . . . . . 7
82 74 , 80 , 81 sylanbrc 664 . . . . . 6
83 82 3adant3 1016 . . . . 5
84 nncn 10569 . . . . . . . . . . 11
85 84 3ad2ant1 1017 . . . . . . . . . 10
86 10 nncnd 10577 . . . . . . . . . 10
87 85 , 86 , 17 sqdivd 12323 . . . . . . . . 9
88 nncn 10569 . . . . . . . . . . 11
89 88 3ad2ant2 1018 . . . . . . . . . 10
90 89 , 86 , 17 sqdivd 12323 . . . . . . . . 9
91 87 , 90 oveq12d 6314 . . . . . . . 8
92 91 3ad2ant1 1017 . . . . . . 7
93 54 nncnd 10577 . . . . . . . . 9
94 57 nncnd 10577 . . . . . . . . 9
95 51 nncnd 10577 . . . . . . . . 9
96 51 nnne0d 10605 . . . . . . . . 9
97 93 , 94 , 95 , 96 divdird 10383 . . . . . . . 8
98 97 3ad2ant1 1017 . . . . . . 7
99 92 , 98 eqtr4d 2501 . . . . . 6
100 nncn 10569 . . . . . . . . . 10
101 100 3ad2ant3 1019 . . . . . . . . 9
102 101 , 86 , 17 sqdivd 12323 . . . . . . . 8
103 102 3ad2ant1 1017 . . . . . . 7
104 oveq1 6303 . . . . . . . 8
105 104 3ad2ant2 1018 . . . . . . 7
106 103 , 105 eqtr4d 2501 . . . . . 6
107 99 , 106 eqtr4d 2501 . . . . 5
108 gcddiv 14187 . . . . . . . 8
109 18 , 33 , 10 , 14 , 108 syl31anc 1231 . . . . . . 7
110 86 , 17 dividd 10343 . . . . . . 7
111 109 , 110 eqtr3d 2500 . . . . . 6
112 111 3ad2ant1 1017 . . . . 5
113 simp3 998 . . . . 5
114 pythagtriplem18 14356 . . . . 5
115 31 , 44 , 83 , 107 , 112 , 113 , 114 syl312anc 1249 . . . 4
116 85 , 86 , 17 divcan2d 10347 . . . . . . . . . 10
117 116 eqcomd 2465 . . . . . . . . 9
118 89 , 86 , 17 divcan2d 10347 . . . . . . . . . 10
119 118 eqcomd 2465 . . . . . . . . 9
120 101 , 86 , 17 divcan2d 10347 . . . . . . . . . 10
121 120 eqcomd 2465 . . . . . . . . 9
122 117 , 119 ,
121 3jca 1176 . . . . . . . 8
123 122 3ad2ant1 1017 . . . . . . 7
124 oveq2 6304 . . . . . . . . . 10
125 124 eqeq2d 2471 . . . . . . . . 9
126 125 3ad2ant1 1017 . . . . . . . 8
127 oveq2 6304 . . . . . . . . . 10
128 127 eqeq2d 2471 . . . . . . . . 9
129 128 3ad2ant2 1018 . . . . . . . 8
130 oveq2 6304 . . . . . . . . . 10
131 130 eqeq2d 2471 . . . . . . . . 9
132 131 3ad2ant3 1019 . . . . . . . 8
133 126 , 129 ,
132 3anbi123d 1299 . . . . . . 7
134 123 , 133 syl5ibcom 220 . . . . . 6
135 134 reximdv 2931 . . . . 5
136 135 reximdv 2931 . . . 4
137 115 , 136 mpd 15 . . 3
138 oveq1 6303 . . . . . . 7
139 138 eqeq2d 2471 . . . . . 6
140 oveq1 6303 . . . . . . 7
141 140 eqeq2d 2471 . . . . . 6
142 oveq1 6303 . . . . . . 7
143 142 eqeq2d 2471 . . . . . 6
144 139 , 141 ,
143 3anbi123d 1299 . . . . 5
145 144 2rexbidv 2975 . . . 4
146 145 rspcev 3210 . . 3
147 11 , 137 , 146 syl2anc 661 . 2
148 rexcom 3019 . . 3
149 rexcom 3019 . . . 4
150 149 rexbii 2959 . . 3
151 148 , 150 bitri 249 . 2
152 147 , 151 sylib 196 1
