Step | Hyp | Ref
| Expression |
1 | | 4sq.1 |
. . . 4
|
2 | | 4sq.2 |
. . . 4
|
3 | | 4sq.3 |
. . . 4
|
4 | | 4sq.4 |
. . . 4
|
5 | | 4sqlem11.5 |
. . . 4
|
6 | | 4sqlem11.6 |
. . . 4
|
7 | 1, 2, 3, 4, 5, 6 | 4sqlem11 15659 |
. . 3
|
8 | | n0 3931 |
. . 3
|
9 | 7, 8 | sylib 208 |
. 2
|
10 | | vex 3203 |
. . . . . . 7
|
11 | | eqeq1 2626 |
. . . . . . . 8
|
12 | 11 | rexbidv 3052 |
. . . . . . 7
|
13 | 10, 12, 5 | elab2 3354 |
. . . . . 6
|
14 | | abid 2610 |
. . . . . . . . 9
|
15 | 5 | rexeqi 3143 |
. . . . . . . . 9
|
16 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
17 | 16 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
18 | 17 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
19 | 18 | cbvrexv 3172 |
. . . . . . . . . . 11
|
20 | | eqeq1 2626 |
. . . . . . . . . . . 12
|
21 | 20 | rexbidv 3052 |
. . . . . . . . . . 11
|
22 | 19, 21 | syl5bb 272 |
. . . . . . . . . 10
|
23 | 22 | rexab 3369 |
. . . . . . . . 9
|
24 | 14, 15, 23 | 3bitri 286 |
. . . . . . . 8
|
25 | 6 | rnmpt 5371 |
. . . . . . . . 9
|
26 | 25 | eleq2i 2693 |
. . . . . . . 8
|
27 | | rexcom4 3225 |
. . . . . . . . 9
|
28 | | r19.41v 3089 |
. . . . . . . . . 10
|
29 | 28 | exbii 1774 |
. . . . . . . . 9
|
30 | 27, 29 | bitri 264 |
. . . . . . . 8
|
31 | 24, 26, 30 | 3bitr4i 292 |
. . . . . . 7
|
32 | | ovex 6678 |
. . . . . . . . 9
|
33 | | oveq2 6658 |
. . . . . . . . . 10
|
34 | 33 | eqeq2d 2632 |
. . . . . . . . 9
|
35 | 32, 34 | ceqsexv 3242 |
. . . . . . . 8
|
36 | 35 | rexbii 3041 |
. . . . . . 7
|
37 | 31, 36 | bitri 264 |
. . . . . 6
|
38 | 13, 37 | anbi12i 733 |
. . . . 5
|
39 | | elin 3796 |
. . . . 5
|
40 | | reeanv 3107 |
. . . . 5
|
41 | 38, 39, 40 | 3bitr4i 292 |
. . . 4
|
42 | | eqtr2 2642 |
. . . . . 6
|
43 | 4 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . 19
|
44 | | prmnn 15388 |
. . . . . . . . . . . . . . . . . . 19
|
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
46 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . . 18
|
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
48 | 47 | nn0red 11352 |
. . . . . . . . . . . . . . . 16
|
49 | 45 | nnrpd 11870 |
. . . . . . . . . . . . . . . 16
|
50 | 47 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . 16
|
51 | 45 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
|
52 | 51 | ltm1d 10956 |
. . . . . . . . . . . . . . . 16
|
53 | | modid 12695 |
. . . . . . . . . . . . . . . 16
|
54 | 48, 49, 50, 52, 53 | syl22anc 1327 |
. . . . . . . . . . . . . . 15
|
55 | 54 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
56 | | simp2r 1088 |
. . . . . . . . . . . . . . . . . . . . 21
|
57 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . 21
|
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
59 | | zsqcl2 12941 |
. . . . . . . . . . . . . . . . . . . 20
|
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
61 | 60 | nn0red 11352 |
. . . . . . . . . . . . . . . . . 18
|
62 | | modlt 12679 |
. . . . . . . . . . . . . . . . . 18
|
63 | 61, 49, 62 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
64 | | zsqcl 12934 |
. . . . . . . . . . . . . . . . . . . . 21
|
65 | 58, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
66 | 65, 45 | zmodcld 12691 |
. . . . . . . . . . . . . . . . . . 19
|
67 | 66 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . 18
|
68 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . 19
|
69 | 43, 68 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
70 | | zltlem1 11430 |
. . . . . . . . . . . . . . . . . 18
|
71 | 67, 69, 70 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
72 | 63, 71 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
73 | 72, 54 | breqtrrd 4681 |
. . . . . . . . . . . . . . 15
|
74 | | modsubdir 12739 |
. . . . . . . . . . . . . . . 16
|
75 | 48, 61, 49, 74 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
76 | 73, 75 | mpbid 222 |
. . . . . . . . . . . . . 14
|
77 | | simp3 1063 |
. . . . . . . . . . . . . 14
|
78 | 55, 76, 77 | 3eqtr4rd 2667 |
. . . . . . . . . . . . 13
|
79 | | simp2l 1087 |
. . . . . . . . . . . . . . . 16
|
80 | | elfzelz 12342 |
. . . . . . . . . . . . . . . 16
|
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . 15
|
82 | | zsqcl 12934 |
. . . . . . . . . . . . . . 15
|
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . 14
|
84 | 47 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
|
85 | 84, 65 | zsubcld 11487 |
. . . . . . . . . . . . . 14
|
86 | | moddvds 14991 |
. . . . . . . . . . . . . 14
|
87 | 45, 83, 85, 86 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
88 | 78, 87 | mpbid 222 |
. . . . . . . . . . . 12
|
89 | | zsqcl2 12941 |
. . . . . . . . . . . . . . . 16
|
90 | 81, 89 | syl 17 |
. . . . . . . . . . . . . . 15
|
91 | 90 | nn0cnd 11353 |
. . . . . . . . . . . . . 14
|
92 | 47 | nn0cnd 11353 |
. . . . . . . . . . . . . 14
|
93 | 60 | nn0cnd 11353 |
. . . . . . . . . . . . . 14
|
94 | 91, 92, 93 | subsub3d 10422 |
. . . . . . . . . . . . 13
|
95 | 90, 60 | nn0addcld 11355 |
. . . . . . . . . . . . . . 15
|
96 | 95 | nn0cnd 11353 |
. . . . . . . . . . . . . 14
|
97 | 45 | nncnd 11036 |
. . . . . . . . . . . . . 14
|
98 | | 1cnd 10056 |
. . . . . . . . . . . . . 14
|
99 | 96, 97, 98 | subsub3d 10422 |
. . . . . . . . . . . . 13
|
100 | 94, 99 | eqtrd 2656 |
. . . . . . . . . . . 12
|
101 | 88, 100 | breqtrd 4679 |
. . . . . . . . . . 11
|
102 | | nn0p1nn 11332 |
. . . . . . . . . . . . . 14
|
103 | 95, 102 | syl 17 |
. . . . . . . . . . . . 13
|
104 | 103 | nnzd 11481 |
. . . . . . . . . . . 12
|
105 | | dvdssubr 15027 |
. . . . . . . . . . . 12
|
106 | 69, 104, 105 | syl2anc 693 |
. . . . . . . . . . 11
|
107 | 101, 106 | mpbird 247 |
. . . . . . . . . 10
|
108 | 45 | nnne0d 11065 |
. . . . . . . . . . 11
|
109 | | dvdsval2 14986 |
. . . . . . . . . . 11
|
110 | 69, 108, 104, 109 | syl3anc 1326 |
. . . . . . . . . 10
|
111 | 107, 110 | mpbid 222 |
. . . . . . . . 9
|
112 | | nnrp 11842 |
. . . . . . . . . . . . . 14
|
113 | | nnrp 11842 |
. . . . . . . . . . . . . 14
|
114 | | rpdivcl 11856 |
. . . . . . . . . . . . . 14
|
115 | 112, 113,
114 | syl2an 494 |
. . . . . . . . . . . . 13
|
116 | 103, 45, 115 | syl2anc 693 |
. . . . . . . . . . . 12
|
117 | 116 | rpgt0d 11875 |
. . . . . . . . . . 11
|
118 | | elnnz 11387 |
. . . . . . . . . . 11
|
119 | 111, 117,
118 | sylanbrc 698 |
. . . . . . . . . 10
|
120 | 119 | nnge1d 11063 |
. . . . . . . . 9
|
121 | 95 | nn0red 11352 |
. . . . . . . . . . . 12
|
122 | | 2nn 11185 |
. . . . . . . . . . . . . . . 16
|
123 | 2 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
|
124 | | nnmulcl 11043 |
. . . . . . . . . . . . . . . 16
|
125 | 122, 123,
124 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
126 | 125 | nnred 11035 |
. . . . . . . . . . . . . 14
|
127 | 126 | resqcld 13035 |
. . . . . . . . . . . . 13
|
128 | | nnmulcl 11043 |
. . . . . . . . . . . . . . 15
|
129 | 122, 125,
128 | sylancr 695 |
. . . . . . . . . . . . . 14
|
130 | 129 | nnred 11035 |
. . . . . . . . . . . . 13
|
131 | 127, 130 | readdcld 10069 |
. . . . . . . . . . . 12
|
132 | | 1red 10055 |
. . . . . . . . . . . 12
|
133 | 123 | nnsqcld 13029 |
. . . . . . . . . . . . . . . 16
|
134 | | nnmulcl 11043 |
. . . . . . . . . . . . . . . 16
|
135 | 122, 133,
134 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
136 | 135 | nnred 11035 |
. . . . . . . . . . . . . 14
|
137 | 90 | nn0red 11352 |
. . . . . . . . . . . . . . . 16
|
138 | 133 | nnred 11035 |
. . . . . . . . . . . . . . . 16
|
139 | 81 | zred 11482 |
. . . . . . . . . . . . . . . . 17
|
140 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . . 18
|
141 | 79, 140 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
142 | 123 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
|
143 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . 18
|
144 | 79, 143 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
145 | | le2sq2 12939 |
. . . . . . . . . . . . . . . . 17
|
146 | 139, 141,
142, 144, 145 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
|
147 | 58 | zred 11482 |
. . . . . . . . . . . . . . . . 17
|
148 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . . 18
|
149 | 56, 148 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
150 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . 18
|
151 | 56, 150 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
152 | | le2sq2 12939 |
. . . . . . . . . . . . . . . . 17
|
153 | 147, 149,
142, 151, 152 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
|
154 | 137, 61, 138, 138, 146, 153 | le2addd 10646 |
. . . . . . . . . . . . . . 15
|
155 | 133 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
|
156 | 155 | 2timesd 11275 |
. . . . . . . . . . . . . . 15
|
157 | 154, 156 | breqtrrd 4681 |
. . . . . . . . . . . . . 14
|
158 | | 2lt4 11198 |
. . . . . . . . . . . . . . . 16
|
159 | | 2re 11090 |
. . . . . . . . . . . . . . . . . 18
|
160 | 159 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
161 | | 4re 11097 |
. . . . . . . . . . . . . . . . . 18
|
162 | 161 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
163 | 133 | nngt0d 11064 |
. . . . . . . . . . . . . . . . 17
|
164 | | ltmul1 10873 |
. . . . . . . . . . . . . . . . 17
|
165 | 160, 162,
138, 163, 164 | syl112anc 1330 |
. . . . . . . . . . . . . . . 16
|
166 | 158, 165 | mpbii 223 |
. . . . . . . . . . . . . . 15
|
167 | | 2cn 11091 |
. . . . . . . . . . . . . . . . 17
|
168 | 123 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
|
169 | | sqmul 12926 |
. . . . . . . . . . . . . . . . 17
|
170 | 167, 168,
169 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
171 | | sq2 12960 |
. . . . . . . . . . . . . . . . 17
|
172 | 171 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
|
173 | 170, 172 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
174 | 166, 173 | breqtrrd 4681 |
. . . . . . . . . . . . . 14
|
175 | 121, 136,
127, 157, 174 | lelttrd 10195 |
. . . . . . . . . . . . 13
|
176 | 129 | nnrpd 11870 |
. . . . . . . . . . . . . 14
|
177 | 127, 176 | ltaddrpd 11905 |
. . . . . . . . . . . . 13
|
178 | 121, 127,
131, 175, 177 | lttrd 10198 |
. . . . . . . . . . . 12
|
179 | 121, 131,
132, 178 | ltadd1dd 10638 |
. . . . . . . . . . 11
|
180 | 3 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
181 | 180 | oveq1d 6665 |
. . . . . . . . . . . 12
|
182 | 97 | sqvald 13005 |
. . . . . . . . . . . 12
|
183 | 125 | nncnd 11036 |
. . . . . . . . . . . . 13
|
184 | | binom21 12980 |
. . . . . . . . . . . . 13
|
185 | 183, 184 | syl 17 |
. . . . . . . . . . . 12
|
186 | 181, 182,
185 | 3eqtr3d 2664 |
. . . . . . . . . . 11
|
187 | 179, 186 | breqtrrd 4681 |
. . . . . . . . . 10
|
188 | 103 | nnred 11035 |
. . . . . . . . . . 11
|
189 | 45 | nngt0d 11064 |
. . . . . . . . . . 11
|
190 | | ltdivmul 10898 |
. . . . . . . . . . 11
|
191 | 188, 51, 51, 189, 190 | syl112anc 1330 |
. . . . . . . . . 10
|
192 | 187, 191 | mpbird 247 |
. . . . . . . . 9
|
193 | | 1z 11407 |
. . . . . . . . . 10
|
194 | | elfzm11 12411 |
. . . . . . . . . 10
|
195 | 193, 69, 194 | sylancr 695 |
. . . . . . . . 9
|
196 | 111, 120,
192, 195 | mpbir3and 1245 |
. . . . . . . 8
|
197 | | gzreim 15643 |
. . . . . . . . 9
|
198 | 81, 58, 197 | syl2anc 693 |
. . . . . . . 8
|
199 | | gzcn 15636 |
. . . . . . . . . . . . 13
|
200 | 198, 199 | syl 17 |
. . . . . . . . . . . 12
|
201 | 200 | absvalsq2d 14182 |
. . . . . . . . . . 11
|
202 | 139, 147 | crred 13971 |
. . . . . . . . . . . . 13
|
203 | 202 | oveq1d 6665 |
. . . . . . . . . . . 12
|
204 | 139, 147 | crimd 13972 |
. . . . . . . . . . . . 13
|
205 | 204 | oveq1d 6665 |
. . . . . . . . . . . 12
|
206 | 203, 205 | oveq12d 6668 |
. . . . . . . . . . 11
|
207 | 201, 206 | eqtrd 2656 |
. . . . . . . . . 10
|
208 | 207 | oveq1d 6665 |
. . . . . . . . 9
|
209 | 103 | nncnd 11036 |
. . . . . . . . . 10
|
210 | 209, 97, 108 | divcan1d 10802 |
. . . . . . . . 9
|
211 | 208, 210 | eqtr4d 2659 |
. . . . . . . 8
|
212 | | oveq1 6657 |
. . . . . . . . . 10
|
213 | 212 | eqeq2d 2632 |
. . . . . . . . 9
|
214 | | fveq2 6191 |
. . . . . . . . . . . 12
|
215 | 214 | oveq1d 6665 |
. . . . . . . . . . 11
|
216 | 215 | oveq1d 6665 |
. . . . . . . . . 10
|
217 | 216 | eqeq1d 2624 |
. . . . . . . . 9
|
218 | 213, 217 | rspc2ev 3324 |
. . . . . . . 8
|
219 | 196, 198,
211, 218 | syl3anc 1326 |
. . . . . . 7
|
220 | 219 | 3expia 1267 |
. . . . . 6
|
221 | 42, 220 | syl5 34 |
. . . . 5
|
222 | 221 | rexlimdvva 3038 |
. . . 4
|
223 | 41, 222 | syl5bi 232 |
. . 3
|
224 | 223 | exlimdv 1861 |
. 2
|
225 | 9, 224 | mpd 15 |
1
|