Proof of Theorem 2sqmod
Step | Hyp | Ref
| Expression |
1 | | 2sqmod.6 |
. . . . . 6
|
2 | 1 | adantr 481 |
. . . . 5
|
3 | | 2sqmod.4 |
. . . . . . . 8
|
4 | 3 | nn0red 11352 |
. . . . . . 7
|
5 | 4 | adantr 481 |
. . . . . 6
|
6 | | 2sqmod.3 |
. . . . . . . 8
|
7 | 6 | nn0red 11352 |
. . . . . . 7
|
8 | 7 | adantr 481 |
. . . . . 6
|
9 | 3 | nn0ge0d 11354 |
. . . . . . 7
|
10 | 9 | adantr 481 |
. . . . . 6
|
11 | 6 | nn0ge0d 11354 |
. . . . . . 7
|
12 | 11 | adantr 481 |
. . . . . 6
|
13 | 3 | nn0cnd 11353 |
. . . . . . . . 9
|
14 | 13 | sqcld 13006 |
. . . . . . . 8
|
15 | 14 | adantr 481 |
. . . . . . 7
|
16 | 6 | nn0cnd 11353 |
. . . . . . . . 9
|
17 | 16 | sqcld 13006 |
. . . . . . . 8
|
18 | 17 | adantr 481 |
. . . . . . 7
|
19 | | 2sqmod.2 |
. . . . . . . . . . . . 13
|
20 | 19 | nn0cnd 11353 |
. . . . . . . . . . . 12
|
21 | 20 | sqcld 13006 |
. . . . . . . . . . 11
|
22 | | 2sqmod.5 |
. . . . . . . . . . . . 13
|
23 | 22 | nn0cnd 11353 |
. . . . . . . . . . . 12
|
24 | 23 | sqcld 13006 |
. . . . . . . . . . 11
|
25 | | 2sqmod.8 |
. . . . . . . . . . . 12
|
26 | | 2sqmod.9 |
. . . . . . . . . . . 12
|
27 | 25, 26 | eqtr4d 2659 |
. . . . . . . . . . 11
|
28 | 21, 17, 14, 24, 27 | subaddeqd 10446 |
. . . . . . . . . 10
|
29 | 28 | adantr 481 |
. . . . . . . . 9
|
30 | 19 | nn0zd 11480 |
. . . . . . . . . . . . . . . 16
|
31 | 3 | nn0zd 11480 |
. . . . . . . . . . . . . . . 16
|
32 | | dvdsmul1 15003 |
. . . . . . . . . . . . . . . 16
|
33 | 30, 31, 32 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
34 | 33 | adantr 481 |
. . . . . . . . . . . . . 14
|
35 | 20, 13 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
36 | 35 | adantr 481 |
. . . . . . . . . . . . . . 15
|
37 | 16, 23 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
38 | 37 | adantr 481 |
. . . . . . . . . . . . . . 15
|
39 | 19 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . 20
|
40 | 39, 4 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . 19
|
41 | 22 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . 20
|
42 | 7, 41 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . 19
|
43 | 40, 42 | resubcld 10458 |
. . . . . . . . . . . . . . . . . 18
|
44 | 43 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
46 | 43 | sqge0d 13036 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
47 | | 2sqmod.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
48 | 6 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
49 | 47, 30, 48, 25 | 2sqn0 29646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
50 | | elnnne0 11306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
51 | 19, 49, 50 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
52 | 22 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
53 | 24, 14 | addcomd 10238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
54 | 53, 26 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
55 | 47, 52, 31, 54 | 2sqn0 29646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
56 | | elnnne0 11306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
57 | 22, 55, 56 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
58 | 51, 57 | nnmulcld 11068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
59 | 47, 31, 52, 26 | 2sqn0 29646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
60 | | elnnne0 11306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
61 | 3, 59, 60 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
62 | 17, 21 | addcomd 10238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
63 | 62, 25 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
64 | 47, 48, 30, 63 | 2sqn0 29646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
65 | | elnnne0 11306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
66 | 6, 64, 65 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
67 | 61, 66 | nnmulcld 11068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
68 | 58, 67 | nnaddcld 11067 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
69 | 68 | nnsqcld 13029 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
70 | 69 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
71 | 43 | resqcld 13035 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
72 | 70, 71 | addge02d 10616 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
73 | 46, 72 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 22
|
74 | 25, 26 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
75 | | bhmafibid1 29644 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
76 | 39, 7, 4, 41, 75 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
77 | 74, 76 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
78 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
79 | 47, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
80 | 79 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
81 | 80 | sqvald 13005 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
82 | 13, 16 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
83 | 82 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
84 | 83 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
85 | 84 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
86 | 77, 81, 85 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . . . . . . 22
|
87 | 73, 86 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . . . 21
|
88 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | 30, 52 | zmulcld 11488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
90 | 31, 48 | zmulcld 11488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
91 | 89, 90 | zaddcld 11486 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
92 | | dvdssqim 15273 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
93 | 79, 91, 92 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
94 | | zsqcl 12934 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
95 | 79, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
96 | | dvdsle 15032 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
97 | 95, 69, 96 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
98 | 93, 97 | syld 47 |
. . . . . . . . . . . . . . . . . . . . 21
|
99 | 98 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
|
100 | 95 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
101 | 70, 100 | letri3d 10179 |
. . . . . . . . . . . . . . . . . . . . 21
|
102 | 101 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
103 | 88, 99, 102 | mpbir2and 957 |
. . . . . . . . . . . . . . . . . . 19
|
104 | 86 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
105 | 103, 104 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . 18
|
106 | 70 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
107 | 71 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
108 | 106, 106,
107 | subadd2d 10411 |
. . . . . . . . . . . . . . . . . . 19
|
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
110 | 105, 109 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
|
111 | 106 | subidd 10380 |
. . . . . . . . . . . . . . . . . 18
|
112 | 111 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
113 | 110, 112 | eqtr3d 2658 |
. . . . . . . . . . . . . . . 16
|
114 | 45, 113 | sqeq0d 13007 |
. . . . . . . . . . . . . . 15
|
115 | 36, 38, 114 | subeq0d 10400 |
. . . . . . . . . . . . . 14
|
116 | 34, 115 | breqtrd 4679 |
. . . . . . . . . . . . 13
|
117 | 47, 30, 48, 25 | 2sqcoprm 29647 |
. . . . . . . . . . . . . 14
|
118 | 117 | adantr 481 |
. . . . . . . . . . . . 13
|
119 | | coprmdvds 15366 |
. . . . . . . . . . . . . . 15
|
120 | 30, 48, 52, 119 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
121 | 120 | adantr 481 |
. . . . . . . . . . . . 13
|
122 | 116, 118,
121 | mp2and 715 |
. . . . . . . . . . . 12
|
123 | | dvdsle 15032 |
. . . . . . . . . . . . . 14
|
124 | 30, 57, 123 | syl2anc 693 |
. . . . . . . . . . . . 13
|
125 | 124 | adantr 481 |
. . . . . . . . . . . 12
|
126 | 122, 125 | mpd 15 |
. . . . . . . . . . 11
|
127 | 51 | nnrpd 11870 |
. . . . . . . . . . . . . 14
|
128 | 127 | rprege0d 11879 |
. . . . . . . . . . . . 13
|
129 | 22 | nn0ge0d 11354 |
. . . . . . . . . . . . 13
|
130 | | le2sq 12938 |
. . . . . . . . . . . . 13
|
131 | 128, 41, 129, 130 | syl12anc 1324 |
. . . . . . . . . . . 12
|
132 | 131 | adantr 481 |
. . . . . . . . . . 11
|
133 | 126, 132 | mpbid 222 |
. . . . . . . . . 10
|
134 | 51 | nnsqcld 13029 |
. . . . . . . . . . . . 13
|
135 | 134 | nnred 11035 |
. . . . . . . . . . . 12
|
136 | | zsqcl 12934 |
. . . . . . . . . . . . . 14
|
137 | 52, 136 | syl 17 |
. . . . . . . . . . . . 13
|
138 | 137 | zred 11482 |
. . . . . . . . . . . 12
|
139 | 135, 138 | suble0d 10618 |
. . . . . . . . . . 11
|
140 | 139 | adantr 481 |
. . . . . . . . . 10
|
141 | 133, 140 | mpbird 247 |
. . . . . . . . 9
|
142 | 29, 141 | eqbrtrrd 4677 |
. . . . . . . 8
|
143 | | dvdsmul1 15003 |
. . . . . . . . . . . . . . 15
|
144 | 48, 52, 143 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
145 | 144 | adantr 481 |
. . . . . . . . . . . . 13
|
146 | 145, 115 | breqtrrd 4681 |
. . . . . . . . . . . 12
|
147 | | gcdcom 15235 |
. . . . . . . . . . . . . . 15
|
148 | 30, 48, 147 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
149 | 148, 117 | eqtr3d 2658 |
. . . . . . . . . . . . 13
|
150 | 149 | adantr 481 |
. . . . . . . . . . . 12
|
151 | | coprmdvds 15366 |
. . . . . . . . . . . . . 14
|
152 | 48, 30, 31, 151 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
153 | 152 | adantr 481 |
. . . . . . . . . . . 12
|
154 | 146, 150,
153 | mp2and 715 |
. . . . . . . . . . 11
|
155 | | dvdsle 15032 |
. . . . . . . . . . . . 13
|
156 | 48, 61, 155 | syl2anc 693 |
. . . . . . . . . . . 12
|
157 | 156 | adantr 481 |
. . . . . . . . . . 11
|
158 | 154, 157 | mpd 15 |
. . . . . . . . . 10
|
159 | 7, 4, 11, 9 | le2sqd 13044 |
. . . . . . . . . . 11
|
160 | 159 | adantr 481 |
. . . . . . . . . 10
|
161 | 158, 160 | mpbid 222 |
. . . . . . . . 9
|
162 | 4 | resqcld 13035 |
. . . . . . . . . . 11
|
163 | | zsqcl 12934 |
. . . . . . . . . . . . 13
|
164 | 48, 163 | syl 17 |
. . . . . . . . . . . 12
|
165 | 164 | zred 11482 |
. . . . . . . . . . 11
|
166 | 162, 165 | subge0d 10617 |
. . . . . . . . . 10
|
167 | 166 | adantr 481 |
. . . . . . . . 9
|
168 | 161, 167 | mpbird 247 |
. . . . . . . 8
|
169 | 135, 138 | resubcld 10458 |
. . . . . . . . . . 11
|
170 | 28, 169 | eqeltrrd 2702 |
. . . . . . . . . 10
|
171 | | 0red 10041 |
. . . . . . . . . 10
|
172 | 170, 171 | letri3d 10179 |
. . . . . . . . 9
|
173 | 172 | adantr 481 |
. . . . . . . 8
|
174 | 142, 168,
173 | mpbir2and 957 |
. . . . . . 7
|
175 | 15, 18, 174 | subeq0d 10400 |
. . . . . 6
|
176 | 5, 8, 10, 12, 175 | sq11d 13045 |
. . . . 5
|
177 | 2, 176 | breqtrrd 4681 |
. . . 4
|
178 | | 2sqmod.7 |
. . . . . 6
|
179 | 178 | adantr 481 |
. . . . 5
|
180 | 39 | adantr 481 |
. . . . . 6
|
181 | 41 | adantr 481 |
. . . . . 6
|
182 | 19 | nn0ge0d 11354 |
. . . . . . 7
|
183 | 182 | adantr 481 |
. . . . . 6
|
184 | 129 | adantr 481 |
. . . . . 6
|
185 | 21 | adantr 481 |
. . . . . . 7
|
186 | 24 | adantr 481 |
. . . . . . 7
|
187 | 168, 29 | breqtrrd 4681 |
. . . . . . . 8
|
188 | 169, 171 | letri3d 10179 |
. . . . . . . . 9
|
189 | 188 | adantr 481 |
. . . . . . . 8
|
190 | 141, 187,
189 | mpbir2and 957 |
. . . . . . 7
|
191 | 185, 186,
190 | subeq0d 10400 |
. . . . . 6
|
192 | 180, 181,
183, 184, 191 | sq11d 13045 |
. . . . 5
|
193 | 179, 192 | breqtrrd 4681 |
. . . 4
|
194 | 39, 4 | letri3d 10179 |
. . . . 5
|
195 | 194 | adantr 481 |
. . . 4
|
196 | 177, 193,
195 | mpbir2and 957 |
. . 3
|
197 | 20 | adantr 481 |
. . . 4
|
198 | 13 | adantr 481 |
. . . 4
|
199 | 16 | adantr 481 |
. . . 4
|
200 | 64 | adantr 481 |
. . . 4
|
201 | 41 | adantr 481 |
. . . . . . 7
|
202 | 7 | adantr 481 |
. . . . . . 7
|
203 | 129 | adantr 481 |
. . . . . . 7
|
204 | 11 | adantr 481 |
. . . . . . 7
|
205 | 24 | adantr 481 |
. . . . . . . 8
|
206 | 17 | adantr 481 |
. . . . . . . 8
|
207 | | prmnn 15388 |
. . . . . . . . . . . . 13
|
208 | 47, 207 | syl 17 |
. . . . . . . . . . . 12
|
209 | 208 | nnne0d 11065 |
. . . . . . . . . . 11
|
210 | 209 | neneqd 2799 |
. . . . . . . . . 10
|
211 | 210 | adantr 481 |
. . . . . . . . 9
|
212 | 80, 24, 17 | subdid 10486 |
. . . . . . . . . . . . . . 15
|
213 | 80, 24 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
214 | 21, 24 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
215 | 80, 17 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
216 | 14, 17 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
217 | 17, 24 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . 18
|
218 | 25 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
|
219 | 21, 17 | pncan2d 10394 |
. . . . . . . . . . . . . . . . . . . 20
|
220 | 218, 219 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . 19
|
221 | 220 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
222 | 26 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
|
223 | 14, 24 | pncan2d 10394 |
. . . . . . . . . . . . . . . . . . . 20
|
224 | 222, 223 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . 19
|
225 | 224 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
226 | 217, 221,
225 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . 17
|
227 | 80, 21, 24 | subdird 10487 |
. . . . . . . . . . . . . . . . 17
|
228 | 80, 14, 17 | subdird 10487 |
. . . . . . . . . . . . . . . . 17
|
229 | 226, 227,
228 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . 16
|
230 | 213, 214,
215, 216, 229 | subeqxfrd 29511 |
. . . . . . . . . . . . . . 15
|
231 | 212, 230 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
232 | 20, 23 | sqmuld 13020 |
. . . . . . . . . . . . . . 15
|
233 | 13, 16 | sqmuld 13020 |
. . . . . . . . . . . . . . 15
|
234 | 232, 233 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
235 | 20, 23 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
236 | 13, 16 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
237 | | subsq 12972 |
. . . . . . . . . . . . . . 15
|
238 | 235, 236,
237 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
239 | 231, 234,
238 | 3eqtr2d 2662 |
. . . . . . . . . . . . 13
|
240 | 239 | adantr 481 |
. . . . . . . . . . . 12
|
241 | 235 | adantr 481 |
. . . . . . . . . . . . . 14
|
242 | | simpll 790 |
. . . . . . . . . . . . . . . 16
|
243 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
244 | 243 | neqned 2801 |
. . . . . . . . . . . . . . . 16
|
245 | 89, 90 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . 19
|
246 | | dvdssqim 15273 |
. . . . . . . . . . . . . . . . . . 19
|
247 | 79, 245, 246 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
248 | 247 | imp 445 |
. . . . . . . . . . . . . . . . 17
|
249 | 248 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
250 | 95 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
251 | 245 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
252 | 235 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
253 | 236 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
254 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
255 | 252, 253,
254 | subne0d 10401 |
. . . . . . . . . . . . . . . . . . 19
|
256 | 251, 255 | znsqcld 29512 |
. . . . . . . . . . . . . . . . . 18
|
257 | | dvdsle 15032 |
. . . . . . . . . . . . . . . . . 18
|
258 | 250, 256,
257 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
259 | 258 | imp 445 |
. . . . . . . . . . . . . . . 16
|
260 | 242, 244,
249, 259 | syl21anc 1325 |
. . . . . . . . . . . . . . 15
|
261 | 39, 41 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . 22
|
262 | 4, 7 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . 22
|
263 | 261, 262 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . 21
|
264 | 263 | resqcld 13035 |
. . . . . . . . . . . . . . . . . . . 20
|
265 | 61 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
266 | 127, 265 | rpmulcld 11888 |
. . . . . . . . . . . . . . . . . . . . . 22
|
267 | 66 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
268 | 57 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
269 | 267, 268 | rpmulcld 11888 |
. . . . . . . . . . . . . . . . . . . . . 22
|
270 | 266, 269 | rpaddcld 11887 |
. . . . . . . . . . . . . . . . . . . . 21
|
271 | | 2z 11409 |
. . . . . . . . . . . . . . . . . . . . . 22
|
272 | 271 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
273 | 270, 272 | rpexpcld 13032 |
. . . . . . . . . . . . . . . . . . . 20
|
274 | 264, 273 | ltaddrp2d 11906 |
. . . . . . . . . . . . . . . . . . 19
|
275 | | bhmafibid2 29645 |
. . . . . . . . . . . . . . . . . . . . . 22
|
276 | 39, 7, 4, 41, 275 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . 21
|
277 | 74, 276 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . 20
|
278 | 82 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
|
279 | 278 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
|
280 | 279 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
|
281 | 277, 280 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . 19
|
282 | 274, 281 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . 18
|
283 | 282, 81 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . 17
|
284 | 242, 283 | syl 17 |
. . . . . . . . . . . . . . . 16
|
285 | 264, 100 | ltnled 10184 |
. . . . . . . . . . . . . . . . 17
|
286 | 242, 285 | syl 17 |
. . . . . . . . . . . . . . . 16
|
287 | 284, 286 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
288 | 260, 287 | condan 835 |
. . . . . . . . . . . . . 14
|
289 | 241, 288 | subeq0bd 10456 |
. . . . . . . . . . . . 13
|
290 | 289 | oveq2d 6666 |
. . . . . . . . . . . 12
|
291 | 235, 236 | addcld 10059 |
. . . . . . . . . . . . . 14
|
292 | 291 | mul01d 10235 |
. . . . . . . . . . . . 13
|
293 | 292 | adantr 481 |
. . . . . . . . . . . 12
|
294 | 240, 290,
293 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
295 | 24, 17 | subcld 10392 |
. . . . . . . . . . . . 13
|
296 | 80, 295 | mul0ord 10677 |
. . . . . . . . . . . 12
|
297 | 296 | adantr 481 |
. . . . . . . . . . 11
|
298 | 294, 297 | mpbid 222 |
. . . . . . . . . 10
|
299 | 298 | ord 392 |
. . . . . . . . 9
|
300 | 211, 299 | mpd 15 |
. . . . . . . 8
|
301 | 205, 206,
300 | subeq0d 10400 |
. . . . . . 7
|
302 | 201, 202,
203, 204, 301 | sq11d 13045 |
. . . . . 6
|
303 | 302 | oveq2d 6666 |
. . . . 5
|
304 | 303, 288 | eqtr3d 2658 |
. . . 4
|
305 | 197, 198,
199, 200, 304 | mulcan2ad 10663 |
. . 3
|
306 | 137, 164 | zsubcld 11487 |
. . . . . 6
|
307 | | dvdsmul1 15003 |
. . . . . 6
|
308 | 79, 306, 307 | syl2anc 693 |
. . . . 5
|
309 | 308, 239 | breqtrd 4679 |
. . . 4
|
310 | | euclemma 15425 |
. . . . 5
|
311 | 47, 91, 245, 310 | syl3anc 1326 |
. . . 4
|
312 | 309, 311 | mpbid 222 |
. . 3
|
313 | 196, 305,
312 | mpjaodan 827 |
. 2
|
314 | 313 | oveq1d 6665 |
. . . . 5
|
315 | 314 | oveq2d 6666 |
. . . 4
|
316 | 315, 220,
224 | 3eqtr3d 2664 |
. . 3
|
317 | 7, 41, 11, 129, 316 | sq11d 13045 |
. 2
|
318 | 313, 317 | jca 554 |
1
|