Step | Hyp | Ref
| Expression |
1 | | lgsquad2.1 |
. . . 4
|
2 | | 2nn 11185 |
. . . . 5
|
3 | 2 | a1i 11 |
. . . 4
|
4 | | lgsquad2.3 |
. . . 4
|
5 | 1 | nnzd 11481 |
. . . . . 6
|
6 | | 2z 11409 |
. . . . . 6
|
7 | | gcdcom 15235 |
. . . . . 6
|
8 | 5, 6, 7 | sylancl 694 |
. . . . 5
|
9 | | lgsquad2.2 |
. . . . . 6
|
10 | | 2prm 15405 |
. . . . . . 7
|
11 | | coprm 15423 |
. . . . . . 7
|
12 | 10, 5, 11 | sylancr 695 |
. . . . . 6
|
13 | 9, 12 | mpbid 222 |
. . . . 5
|
14 | 8, 13 | eqtrd 2656 |
. . . 4
|
15 | | rpmulgcd 15275 |
. . . 4
|
16 | 1, 3, 4, 14, 15 | syl31anc 1329 |
. . 3
|
17 | | lgsquad2.5 |
. . 3
|
18 | 16, 17 | eqtrd 2656 |
. 2
|
19 | | oveq1 6657 |
. . . . . . . 8
|
20 | | oveq2 6658 |
. . . . . . . 8
|
21 | 19, 20 | oveq12d 6668 |
. . . . . . 7
|
22 | | oveq1 6657 |
. . . . . . . . . . . 12
|
23 | | 1m1e0 11089 |
. . . . . . . . . . . 12
|
24 | 22, 23 | syl6eq 2672 |
. . . . . . . . . . 11
|
25 | 24 | oveq1d 6665 |
. . . . . . . . . 10
|
26 | | 2cn 11091 |
. . . . . . . . . . 11
|
27 | | 2ne0 11113 |
. . . . . . . . . . 11
|
28 | 26, 27 | div0i 10759 |
. . . . . . . . . 10
|
29 | 25, 28 | syl6eq 2672 |
. . . . . . . . 9
|
30 | 29 | oveq1d 6665 |
. . . . . . . 8
|
31 | 30 | oveq2d 6666 |
. . . . . . 7
|
32 | 21, 31 | eqeq12d 2637 |
. . . . . 6
|
33 | 32 | imbi2d 330 |
. . . . 5
|
34 | 33 | imbi2d 330 |
. . . 4
|
35 | | oveq1 6657 |
. . . . . . 7
|
36 | 35 | eqeq1d 2624 |
. . . . . 6
|
37 | | oveq1 6657 |
. . . . . . . 8
|
38 | | oveq2 6658 |
. . . . . . . 8
|
39 | 37, 38 | oveq12d 6668 |
. . . . . . 7
|
40 | | oveq1 6657 |
. . . . . . . . . 10
|
41 | 40 | oveq1d 6665 |
. . . . . . . . 9
|
42 | 41 | oveq1d 6665 |
. . . . . . . 8
|
43 | 42 | oveq2d 6666 |
. . . . . . 7
|
44 | 39, 43 | eqeq12d 2637 |
. . . . . 6
|
45 | 36, 44 | imbi12d 334 |
. . . . 5
|
46 | 45 | imbi2d 330 |
. . . 4
|
47 | | oveq1 6657 |
. . . . . . 7
|
48 | 47 | eqeq1d 2624 |
. . . . . 6
|
49 | | oveq1 6657 |
. . . . . . . 8
|
50 | | oveq2 6658 |
. . . . . . . 8
|
51 | 49, 50 | oveq12d 6668 |
. . . . . . 7
|
52 | | oveq1 6657 |
. . . . . . . . . 10
|
53 | 52 | oveq1d 6665 |
. . . . . . . . 9
|
54 | 53 | oveq1d 6665 |
. . . . . . . 8
|
55 | 54 | oveq2d 6666 |
. . . . . . 7
|
56 | 51, 55 | eqeq12d 2637 |
. . . . . 6
|
57 | 48, 56 | imbi12d 334 |
. . . . 5
|
58 | 57 | imbi2d 330 |
. . . 4
|
59 | | oveq1 6657 |
. . . . . . 7
|
60 | 59 | eqeq1d 2624 |
. . . . . 6
|
61 | | oveq1 6657 |
. . . . . . . 8
|
62 | | oveq2 6658 |
. . . . . . . 8
|
63 | 61, 62 | oveq12d 6668 |
. . . . . . 7
|
64 | | oveq1 6657 |
. . . . . . . . . 10
|
65 | 64 | oveq1d 6665 |
. . . . . . . . 9
|
66 | 65 | oveq1d 6665 |
. . . . . . . 8
|
67 | 66 | oveq2d 6666 |
. . . . . . 7
|
68 | 63, 67 | eqeq12d 2637 |
. . . . . 6
|
69 | 60, 68 | imbi12d 334 |
. . . . 5
|
70 | 69 | imbi2d 330 |
. . . 4
|
71 | | oveq1 6657 |
. . . . . . 7
|
72 | 71 | eqeq1d 2624 |
. . . . . 6
|
73 | | oveq1 6657 |
. . . . . . . 8
|
74 | | oveq2 6658 |
. . . . . . . 8
|
75 | 73, 74 | oveq12d 6668 |
. . . . . . 7
|
76 | | oveq1 6657 |
. . . . . . . . . 10
|
77 | 76 | oveq1d 6665 |
. . . . . . . . 9
|
78 | 77 | oveq1d 6665 |
. . . . . . . 8
|
79 | 78 | oveq2d 6666 |
. . . . . . 7
|
80 | 75, 79 | eqeq12d 2637 |
. . . . . 6
|
81 | 72, 80 | imbi12d 334 |
. . . . 5
|
82 | 81 | imbi2d 330 |
. . . 4
|
83 | | 1t1e1 11175 |
. . . . . . 7
|
84 | | neg1cn 11124 |
. . . . . . . 8
|
85 | | exp0 12864 |
. . . . . . . 8
|
86 | 84, 85 | ax-mp 5 |
. . . . . . 7
|
87 | 83, 86 | eqtr4i 2647 |
. . . . . 6
|
88 | | sq1 12958 |
. . . . . . . . 9
|
89 | 88 | oveq1i 6660 |
. . . . . . . 8
|
90 | | 1z 11407 |
. . . . . . . . . 10
|
91 | | ax-1ne0 10005 |
. . . . . . . . . 10
|
92 | 90, 91 | pm3.2i 471 |
. . . . . . . . 9
|
93 | 4 | nnzd 11481 |
. . . . . . . . 9
|
94 | | 1gcd 15254 |
. . . . . . . . . 10
|
95 | 93, 94 | syl 17 |
. . . . . . . . 9
|
96 | | lgssq 25062 |
. . . . . . . . 9
|
97 | 92, 93, 95, 96 | mp3an2i 1429 |
. . . . . . . 8
|
98 | 89, 97 | syl5eqr 2670 |
. . . . . . 7
|
99 | 88 | oveq2i 6661 |
. . . . . . . 8
|
100 | | 1nn 11031 |
. . . . . . . . . 10
|
101 | 100 | a1i 11 |
. . . . . . . . 9
|
102 | | gcd1 15249 |
. . . . . . . . . 10
|
103 | 93, 102 | syl 17 |
. . . . . . . . 9
|
104 | | lgssq2 25063 |
. . . . . . . . 9
|
105 | 93, 101, 103, 104 | syl3anc 1326 |
. . . . . . . 8
|
106 | 99, 105 | syl5eqr 2670 |
. . . . . . 7
|
107 | 98, 106 | oveq12d 6668 |
. . . . . 6
|
108 | | nnm1nn0 11334 |
. . . . . . . . . . 11
|
109 | 4, 108 | syl 17 |
. . . . . . . . . 10
|
110 | 109 | nn0cnd 11353 |
. . . . . . . . 9
|
111 | 110 | halfcld 11277 |
. . . . . . . 8
|
112 | 111 | mul02d 10234 |
. . . . . . 7
|
113 | 112 | oveq2d 6666 |
. . . . . 6
|
114 | 87, 107, 113 | 3eqtr4a 2682 |
. . . . 5
|
115 | 114 | a1d 25 |
. . . 4
|
116 | | simprl 794 |
. . . . . . . . 9
|
117 | | prmz 15389 |
. . . . . . . . . . . 12
|
118 | 117 | ad2antrl 764 |
. . . . . . . . . . 11
|
119 | 6 | a1i 11 |
. . . . . . . . . . 11
|
120 | 4 | adantr 481 |
. . . . . . . . . . . . 13
|
121 | 120 | nnzd 11481 |
. . . . . . . . . . . 12
|
122 | | zmulcl 11426 |
. . . . . . . . . . . 12
|
123 | 6, 121, 122 | sylancr 695 |
. . . . . . . . . . 11
|
124 | | simprr 796 |
. . . . . . . . . . 11
|
125 | | dvdsmul1 15003 |
. . . . . . . . . . . 12
|
126 | 6, 121, 125 | sylancr 695 |
. . . . . . . . . . 11
|
127 | | rpdvds 15374 |
. . . . . . . . . . 11
|
128 | 118, 119,
123, 124, 126, 127 | syl32anc 1334 |
. . . . . . . . . 10
|
129 | | prmrp 15424 |
. . . . . . . . . . 11
|
130 | 116, 10, 129 | sylancl 694 |
. . . . . . . . . 10
|
131 | 128, 130 | mpbid 222 |
. . . . . . . . 9
|
132 | | eldifsn 4317 |
. . . . . . . . 9
|
133 | 116, 131,
132 | sylanbrc 698 |
. . . . . . . 8
|
134 | | prmnn 15388 |
. . . . . . . . . . 11
|
135 | 134 | ad2antrl 764 |
. . . . . . . . . 10
|
136 | 2 | a1i 11 |
. . . . . . . . . 10
|
137 | | rpmulgcd 15275 |
. . . . . . . . . 10
|
138 | 135, 136,
120, 128, 137 | syl31anc 1329 |
. . . . . . . . 9
|
139 | 138, 124 | eqtr3d 2658 |
. . . . . . . 8
|
140 | 133, 139 | jca 554 |
. . . . . . 7
|
141 | | lgsquad2lem2.f |
. . . . . . 7
|
142 | 140, 141 | syldan 487 |
. . . . . 6
|
143 | 142 | exp32 631 |
. . . . 5
|
144 | 143 | com12 32 |
. . . 4
|
145 | | jcab 907 |
. . . . 5
|
146 | | simplrl 800 |
. . . . . . . . . . . 12
|
147 | | eluz2nn 11726 |
. . . . . . . . . . . 12
|
148 | 146, 147 | syl 17 |
. . . . . . . . . . 11
|
149 | | simplrr 801 |
. . . . . . . . . . . 12
|
150 | | eluz2nn 11726 |
. . . . . . . . . . . 12
|
151 | 149, 150 | syl 17 |
. . . . . . . . . . 11
|
152 | 148, 151 | nnmulcld 11068 |
. . . . . . . . . 10
|
153 | | n2dvds1 15104 |
. . . . . . . . . . . 12
|
154 | 93 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
155 | 6, 154, 125 | sylancr 695 |
. . . . . . . . . . . . . 14
|
156 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . . 18
|
157 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . . 18
|
158 | 156, 157 | anim12i 590 |
. . . . . . . . . . . . . . . . 17
|
159 | 158 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
|
160 | | zmulcl 11426 |
. . . . . . . . . . . . . . . 16
|
161 | 159, 160 | syl 17 |
. . . . . . . . . . . . . . 15
|
162 | 6, 154, 122 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
163 | | dvdsgcd 15261 |
. . . . . . . . . . . . . . 15
|
164 | 6, 161, 162, 163 | mp3an2i 1429 |
. . . . . . . . . . . . . 14
|
165 | 155, 164 | mpan2d 710 |
. . . . . . . . . . . . 13
|
166 | | simpr 477 |
. . . . . . . . . . . . . 14
|
167 | 166 | breq2d 4665 |
. . . . . . . . . . . . 13
|
168 | 165, 167 | sylibd 229 |
. . . . . . . . . . . 12
|
169 | 153, 168 | mtoi 190 |
. . . . . . . . . . 11
|
170 | 169 | adantrr 753 |
. . . . . . . . . 10
|
171 | 4 | ad2antrr 762 |
. . . . . . . . . 10
|
172 | | lgsquad2.4 |
. . . . . . . . . . 11
|
173 | 172 | ad2antrr 762 |
. . . . . . . . . 10
|
174 | | dvdsmul2 15004 |
. . . . . . . . . . . . 13
|
175 | 6, 154, 174 | sylancr 695 |
. . . . . . . . . . . 12
|
176 | | rpdvds 15374 |
. . . . . . . . . . . 12
|
177 | 161, 154,
162, 166, 175, 176 | syl32anc 1334 |
. . . . . . . . . . 11
|
178 | 177 | adantrr 753 |
. . . . . . . . . 10
|
179 | | eqidd 2623 |
. . . . . . . . . 10
|
180 | 159 | simpld 475 |
. . . . . . . . . . . . . 14
|
181 | | gcdcom 15235 |
. . . . . . . . . . . . . 14
|
182 | 180, 162,
181 | syl2anc 693 |
. . . . . . . . . . . . 13
|
183 | | gcdcom 15235 |
. . . . . . . . . . . . . . . 16
|
184 | 162, 161,
183 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
185 | 184, 166 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
186 | | dvdsmul1 15003 |
. . . . . . . . . . . . . . 15
|
187 | 159, 186 | syl 17 |
. . . . . . . . . . . . . 14
|
188 | | rpdvds 15374 |
. . . . . . . . . . . . . 14
|
189 | 162, 180,
161, 185, 187, 188 | syl32anc 1334 |
. . . . . . . . . . . . 13
|
190 | 182, 189 | eqtrd 2656 |
. . . . . . . . . . . 12
|
191 | 190 | adantrr 753 |
. . . . . . . . . . 11
|
192 | | simprrl 804 |
. . . . . . . . . . 11
|
193 | 191, 192 | mpd 15 |
. . . . . . . . . 10
|
194 | 159 | simprd 479 |
. . . . . . . . . . . . . 14
|
195 | | gcdcom 15235 |
. . . . . . . . . . . . . 14
|
196 | 194, 162,
195 | syl2anc 693 |
. . . . . . . . . . . . 13
|
197 | | dvdsmul2 15004 |
. . . . . . . . . . . . . . 15
|
198 | 159, 197 | syl 17 |
. . . . . . . . . . . . . 14
|
199 | | rpdvds 15374 |
. . . . . . . . . . . . . 14
|
200 | 162, 194,
161, 185, 198, 199 | syl32anc 1334 |
. . . . . . . . . . . . 13
|
201 | 196, 200 | eqtrd 2656 |
. . . . . . . . . . . 12
|
202 | 201 | adantrr 753 |
. . . . . . . . . . 11
|
203 | | simprrr 805 |
. . . . . . . . . . 11
|
204 | 202, 203 | mpd 15 |
. . . . . . . . . 10
|
205 | 152, 170,
171, 173, 178, 148, 151, 179, 193, 204 | lgsquad2lem1 25109 |
. . . . . . . . 9
|
206 | 205 | exp32 631 |
. . . . . . . 8
|
207 | 206 | com23 86 |
. . . . . . 7
|
208 | 207 | expcom 451 |
. . . . . 6
|
209 | 208 | a2d 29 |
. . . . 5
|
210 | 145, 209 | syl5bir 233 |
. . . 4
|
211 | 34, 46, 58, 70, 82, 115, 144, 210 | prmind 15399 |
. . 3
|
212 | 1, 211 | mpcom 38 |
. 2
|
213 | 18, 212 | mpd 15 |
1
|