Step | Hyp | Ref
| Expression |
1 | | neg1cn 11124 |
. . . 4
|
2 | 1 | a1i 11 |
. . 3
|
3 | | neg1ne0 11126 |
. . . 4
|
4 | 3 | a1i 11 |
. . 3
|
5 | | fzfid 12772 |
. . . 4
|
6 | | lgseisen.2 |
. . . . . . . . . 10
|
7 | | eldifi 3732 |
. . . . . . . . . 10
|
8 | | prmnn 15388 |
. . . . . . . . . 10
|
9 | 6, 7, 8 | 3syl 18 |
. . . . . . . . 9
|
10 | 9 | nnred 11035 |
. . . . . . . 8
|
11 | | lgseisen.1 |
. . . . . . . . 9
|
12 | | eldifi 3732 |
. . . . . . . . 9
|
13 | | prmnn 15388 |
. . . . . . . . 9
|
14 | 11, 12, 13 | 3syl 18 |
. . . . . . . 8
|
15 | 10, 14 | nndivred 11069 |
. . . . . . 7
|
16 | 15 | adantr 481 |
. . . . . 6
|
17 | | 2z 11409 |
. . . . . . . 8
|
18 | | elfzelz 12342 |
. . . . . . . . 9
|
19 | 18 | adantl 482 |
. . . . . . . 8
|
20 | | zmulcl 11426 |
. . . . . . . 8
|
21 | 17, 19, 20 | sylancr 695 |
. . . . . . 7
|
22 | 21 | zred 11482 |
. . . . . 6
|
23 | 16, 22 | remulcld 10070 |
. . . . 5
|
24 | 23 | flcld 12599 |
. . . 4
|
25 | 5, 24 | fsumzcl 14466 |
. . 3
|
26 | 2, 4, 25 | expclzd 13013 |
. 2
|
27 | | fzfid 12772 |
. . . . . . 7
|
28 | | fzfid 12772 |
. . . . . . 7
|
29 | | xpfi 8231 |
. . . . . . 7
|
30 | 27, 28, 29 | syl2anc 693 |
. . . . . 6
|
31 | | lgsquad.6 |
. . . . . . 7
|
32 | | opabssxp 5193 |
. . . . . . 7
|
33 | 31, 32 | eqsstri 3635 |
. . . . . 6
|
34 | | ssfi 8180 |
. . . . . 6
|
35 | 30, 33, 34 | sylancl 694 |
. . . . 5
|
36 | | ssrab2 3687 |
. . . . 5
|
37 | | ssfi 8180 |
. . . . 5
|
38 | 35, 36, 37 | sylancl 694 |
. . . 4
|
39 | | hashcl 13147 |
. . . 4
|
40 | 38, 39 | syl 17 |
. . 3
|
41 | | expcl 12878 |
. . 3
|
42 | 1, 40, 41 | sylancr 695 |
. 2
|
43 | 40 | nn0zd 11480 |
. . 3
|
44 | 2, 4, 43 | expne0d 13014 |
. 2
|
45 | 42, 44 | recidd 10796 |
. . . 4
|
46 | | 1div1e1 10717 |
. . . . . . . . 9
|
47 | 46 | negeqi 10274 |
. . . . . . . 8
|
48 | | ax-1cn 9994 |
. . . . . . . . 9
|
49 | | ax-1ne0 10005 |
. . . . . . . . 9
|
50 | | divneg2 10749 |
. . . . . . . . 9
|
51 | 48, 48, 49, 50 | mp3an 1424 |
. . . . . . . 8
|
52 | 47, 51 | eqtr3i 2646 |
. . . . . . 7
|
53 | 52 | oveq1i 6660 |
. . . . . 6
|
54 | 2, 4, 43 | exprecd 13016 |
. . . . . 6
|
55 | 53, 54 | syl5eq 2668 |
. . . . 5
|
56 | 55 | oveq2d 6666 |
. . . 4
|
57 | 35 | adantr 481 |
. . . . . . . . . . . 12
|
58 | | ssrab2 3687 |
. . . . . . . . . . . 12
|
59 | | ssfi 8180 |
. . . . . . . . . . . 12
|
60 | 57, 58, 59 | sylancl 694 |
. . . . . . . . . . 11
|
61 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
62 | 61 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | 62 | elrab 3363 |
. . . . . . . . . . . . . . . . . . 19
|
64 | 63 | simprbi 480 |
. . . . . . . . . . . . . . . . . 18
|
65 | 64 | ad2antll 765 |
. . . . . . . . . . . . . . . . 17
|
66 | 65 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
67 | 14 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
68 | 67 | nncnd 11036 |
. . . . . . . . . . . . . . . . . 18
|
69 | 68 | adantrr 753 |
. . . . . . . . . . . . . . . . 17
|
70 | 21 | zcnd 11483 |
. . . . . . . . . . . . . . . . . 18
|
71 | 70 | adantrr 753 |
. . . . . . . . . . . . . . . . 17
|
72 | 69, 71 | nncand 10397 |
. . . . . . . . . . . . . . . 16
|
73 | 66, 72 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
74 | 73 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
75 | 19 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
|
76 | 75 | adantrr 753 |
. . . . . . . . . . . . . . 15
|
77 | | 2cnd 11093 |
. . . . . . . . . . . . . . 15
|
78 | | 2ne0 11113 |
. . . . . . . . . . . . . . . 16
|
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . 15
|
80 | 76, 77, 79 | divcan3d 10806 |
. . . . . . . . . . . . . 14
|
81 | 74, 80 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
82 | 81 | ralrimivva 2971 |
. . . . . . . . . . . 12
|
83 | | invdisj 4638 |
. . . . . . . . . . . 12
Disj |
84 | 82, 83 | syl 17 |
. . . . . . . . . . 11
Disj
|
85 | 5, 60, 84 | hashiun 14554 |
. . . . . . . . . 10
|
86 | | iunrab 4567 |
. . . . . . . . . . . 12
|
87 | | eldifsni 4320 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
88 | 11, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
89 | 88 | necomd 2849 |
. . . . . . . . . . . . . . . . . . . . 21
|
90 | 89 | neneqd 2799 |
. . . . . . . . . . . . . . . . . . . 20
|
91 | 90 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
92 | | uzid 11702 |
. . . . . . . . . . . . . . . . . . . . 21
|
93 | 17, 92 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
94 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
95 | 94 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
|
96 | | dvdsprm 15415 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | 93, 95, 96 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
|
98 | 91, 97 | mtbird 315 |
. . . . . . . . . . . . . . . . . 18
|
99 | 14 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
|
100 | 99 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
|
101 | 21 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . 21
|
102 | 101 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
|
103 | 100, 102 | npcand 10396 |
. . . . . . . . . . . . . . . . . . 19
|
104 | 103 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
|
105 | 98, 104 | mtbird 315 |
. . . . . . . . . . . . . . . . 17
|
106 | 18 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
107 | | dvdsmul1 15003 |
. . . . . . . . . . . . . . . . . . 19
|
108 | 17, 106, 107 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
|
109 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
110 | 99 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . 20
|
111 | 110, 101 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . 19
|
112 | | dvds2add 15015 |
. . . . . . . . . . . . . . . . . . 19
|
113 | 109, 111,
101, 112 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
114 | 108, 113 | mpan2d 710 |
. . . . . . . . . . . . . . . . 17
|
115 | 105, 114 | mtod 189 |
. . . . . . . . . . . . . . . 16
|
116 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
|
117 | 116 | notbid 308 |
. . . . . . . . . . . . . . . 16
|
118 | 115, 117 | syl5ibrcom 237 |
. . . . . . . . . . . . . . 15
|
119 | 118 | rexlimdva 3031 |
. . . . . . . . . . . . . 14
|
120 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
121 | 33, 120 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
|
122 | | xp1st 7198 |
. . . . . . . . . . . . . . . . 17
|
123 | 121, 122 | syl 17 |
. . . . . . . . . . . . . . . 16
|
124 | | elfzelz 12342 |
. . . . . . . . . . . . . . . 16
|
125 | | odd2np1 15065 |
. . . . . . . . . . . . . . . 16
|
126 | 123, 124,
125 | 3syl 18 |
. . . . . . . . . . . . . . 15
|
127 | | lgsquad.4 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
128 | | oddprm 15515 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
129 | 11, 128 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
130 | 127, 129 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
131 | 130 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
132 | 131 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
|
133 | 132 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . . 21
|
134 | | reflcl 12597 |
. . . . . . . . . . . . . . . . . . . . 21
|
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
136 | 130 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
137 | 136 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
138 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . 22
|
139 | 137, 138 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . . . 21
|
140 | 139 | zred 11482 |
. . . . . . . . . . . . . . . . . . . 20
|
141 | | flle 12600 |
. . . . . . . . . . . . . . . . . . . . 21
|
142 | 133, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
143 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . 22
|
144 | 143 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . 21
|
145 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
146 | 123 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
147 | 145, 146 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
148 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
149 | 147, 148 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
150 | | zmulcl 11426 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
151 | 17, 138, 150 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
152 | | zltp1le 11427 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
153 | 151, 137,
152 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
154 | 149, 153 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
155 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
156 | 155 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
157 | | 2pos 11112 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
158 | 157 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
159 | | ltmuldiv2 10897 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
160 | 144, 132,
156, 158, 159 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
161 | 154, 160 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 22
|
162 | 133 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
163 | 162, 162 | pncan2d 10394 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
164 | 130 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
165 | 164 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
166 | 165 | 2halvesd 11278 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
167 | 166 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
168 | 163, 167 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . 22
|
169 | 161, 168 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
|
170 | 144, 132,
133, 169 | ltsub13d 10633 |
. . . . . . . . . . . . . . . . . . . 20
|
171 | 135, 133,
140, 142, 170 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . 19
|
172 | 133 | flcld 12599 |
. . . . . . . . . . . . . . . . . . . 20
|
173 | | zltp1le 11427 |
. . . . . . . . . . . . . . . . . . . 20
|
174 | 172, 139,
173 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
175 | 171, 174 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
|
176 | | 2t0e0 11183 |
. . . . . . . . . . . . . . . . . . . . 21
|
177 | | 2cn 11091 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
178 | | zcn 11382 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
179 | 178 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
180 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
181 | 177, 179,
180 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
182 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
183 | 181, 48, 182 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
184 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
185 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
186 | 147, 184,
185 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
187 | 183, 186 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . . . 22
|
188 | 187 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . . . . . . 21
|
189 | 176, 188 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . . 20
|
190 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . 21
|
191 | | lemul2 10876 |
. . . . . . . . . . . . . . . . . . . . 21
|
192 | 190, 144,
156, 158, 191 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . 20
|
193 | 189, 192 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
|
194 | 132, 144 | subge02d 10619 |
. . . . . . . . . . . . . . . . . . 19
|
195 | 193, 194 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
|
196 | 172 | peano2zd 11485 |
. . . . . . . . . . . . . . . . . . 19
|
197 | | elfz 12332 |
. . . . . . . . . . . . . . . . . . 19
|
198 | 139, 196,
137, 197 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
199 | 175, 195,
198 | mpbir2and 957 |
. . . . . . . . . . . . . . . . 17
|
200 | 94 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
|
201 | 200, 13 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
202 | 201 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . 19
|
203 | | peano2cn 10208 |
. . . . . . . . . . . . . . . . . . . 20
|
204 | 181, 203 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
205 | 202, 204 | nncand 10397 |
. . . . . . . . . . . . . . . . . 18
|
206 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . 21
|
207 | 202, 181,
206 | sub32d 10424 |
. . . . . . . . . . . . . . . . . . . 20
|
208 | 202, 181,
206 | subsub4d 10423 |
. . . . . . . . . . . . . . . . . . . 20
|
209 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . . 22
|
210 | 209, 165,
179 | subdid 10486 |
. . . . . . . . . . . . . . . . . . . . 21
|
211 | 127 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
212 | 14 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
213 | 212 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
214 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
215 | 213, 214 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
216 | 215 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
217 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
218 | 216, 209,
217 | divcan2d 10803 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
219 | 211, 218 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . 22
|
220 | 219 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
|
221 | 210, 220 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . 20
|
222 | 207, 208,
221 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . . . . 19
|
223 | 222 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
|
224 | 205, 223,
145 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . . . . 17
|
225 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
|
226 | 225 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
227 | 226 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
228 | 227 | rspcev 3309 |
. . . . . . . . . . . . . . . . 17
|
229 | 199, 224,
228 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
230 | 229 | rexlimdvaa 3032 |
. . . . . . . . . . . . . . 15
|
231 | 126, 230 | sylbid 230 |
. . . . . . . . . . . . . 14
|
232 | 119, 231 | impbid 202 |
. . . . . . . . . . . . 13
|
233 | 232 | rabbidva 3188 |
. . . . . . . . . . . 12
|
234 | 86, 233 | syl5eq 2668 |
. . . . . . . . . . 11
|
235 | 234 | fveq2d 6195 |
. . . . . . . . . 10
|
236 | 31 | relopabi 5245 |
. . . . . . . . . . . . . . 15
|
237 | | relss 5206 |
. . . . . . . . . . . . . . 15
|
238 | 58, 236, 237 | mp2 9 |
. . . . . . . . . . . . . 14
|
239 | | relxp 5227 |
. . . . . . . . . . . . . 14
|
240 | 31 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . 18
|
241 | | opabid 4982 |
. . . . . . . . . . . . . . . . . 18
|
242 | 240, 241 | bitri 264 |
. . . . . . . . . . . . . . . . 17
|
243 | | anass 681 |
. . . . . . . . . . . . . . . . . . 19
|
244 | 24 | peano2zd 11485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
245 | 244 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
246 | 245 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
247 | 10 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
248 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
249 | 248 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
250 | | lesub 10507 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
251 | 246, 247,
249, 250 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
252 | 10 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
253 | 252 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
254 | 68, 253 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
255 | 70, 253 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
256 | 67 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
257 | 253, 68, 256 | divcan1d 10802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
258 | 257 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
259 | 16 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
260 | 259, 68, 70 | mul32d 10246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
261 | 255, 258,
260 | 3eqtr2d 2662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
262 | 254, 261 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
263 | 68, 70, 253 | subdird 10487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
264 | 23 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
265 | 253, 264,
68 | subdird 10487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
266 | 262, 263,
265 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
267 | 266 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
268 | 267 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
269 | 23 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
270 | 247, 269 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
271 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
272 | 271 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
273 | 271 | nngt0d 11064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
274 | | ltmul1 10873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
275 | 249, 270,
272, 273, 274 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
276 | | ltsub13 10509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
277 | 249, 247,
269, 276 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
278 | 268, 275,
277 | 3bitr2d 296 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
279 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
280 | 279 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
281 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
282 | | zsubcl 11419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
283 | 280, 281,
282 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
284 | | fllt 12607 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
285 | 269, 283,
284 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
286 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
287 | | zltp1le 11427 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
288 | 286, 283,
287 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
289 | 278, 285,
288 | 3bitrd 294 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
290 | | lgsquad.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
291 | 290 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
292 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
293 | 252, 292 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
294 | 293 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
295 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
296 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
297 | 294, 295,
296 | divcan2d 10803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
298 | 291, 297 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
299 | 298 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
300 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
301 | 24 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
302 | 253, 300,
301 | sub32d 10424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
303 | 253, 301,
300 | subsub4d 10423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
304 | 299, 302,
303 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
305 | 304 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
306 | 305 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
307 | 251, 289,
306 | 3bitr4d 300 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
308 | 307 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . 22
|
309 | | 2nn 11185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
310 | | oddprm 15515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
311 | 6, 310 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
312 | 290, 311 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
313 | | nnmulcl 11043 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
314 | 309, 312,
313 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
315 | 314 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
316 | 315 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
317 | 312 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
318 | 317 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
319 | 24 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
320 | 312 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
321 | 320 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
322 | 321 | 2timesd 11275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
323 | 322 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
324 | 321, 321 | pncan2d 10394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
325 | 323, 324 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
326 | 252 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
327 | 252 | ltm1d 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
328 | 155 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
329 | 157 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
330 | | ltdiv1 10887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
331 | 293, 252,
328, 329, 330 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
332 | 327, 331 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
333 | 290, 332 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
334 | 318, 326,
333 | ltled 10185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
335 | 253, 295,
68, 296 | div32d 10824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
336 | 131 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
337 | 336 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
338 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
339 | 337, 134,
338 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
340 | 19 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
341 | | flltp1 12601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
342 | 337, 341 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
343 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
344 | 343 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
345 | 337, 339,
340, 342, 344 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
346 | | ltdivmul 10898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
347 | 336, 340,
328, 329, 346 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
348 | 345, 347 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
349 | 127, 348 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
350 | 67 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
351 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
352 | 350, 351 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
353 | | ltdivmul 10898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
354 | 352, 22, 328, 329, 353 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
355 | 349, 354 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
356 | 212 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
357 | | zmulcl 11426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
358 | 17, 21, 357 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
359 | | zlem1lt 11429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
360 | 356, 358,
359 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
361 | 355, 360 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
362 | | ledivmul 10899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
363 | 350, 22, 328, 329, 362 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
364 | 361, 363 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
365 | 350 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
366 | 279 | nngt0d 11064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
367 | | lemul2 10876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
368 | 365, 22, 252, 366, 367 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
369 | 364, 368 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
370 | 335, 369 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
371 | 252, 22 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
372 | 67 | nngt0d 11064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
373 | | lemuldiv 10903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
374 | 326, 371,
350, 372, 373 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
375 | 370, 374 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
376 | 253, 70, 68, 256 | div23d 10838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
377 | 375, 376 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
378 | 318, 326,
23, 334, 377 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
379 | 312 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
380 | 379 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
381 | | flge 12606 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
382 | 23, 380, 381 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
383 | 378, 382 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
384 | 325, 383 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
385 | 316, 318,
319, 384 | subled 10630 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
386 | 385 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
387 | 315 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
388 | 387, 24 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
389 | 388 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
390 | 389 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
391 | 312 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
392 | 391 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
393 | | letr 10131 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
394 | 249, 390,
392, 393 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
395 | 386, 394 | mpan2d 710 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
396 | 395 | pm4.71rd 667 |
. . . . . . . . . . . . . . . . . . . . . 22
|
397 | 308, 396 | bitr4d 271 |
. . . . . . . . . . . . . . . . . . . . 21
|
398 | 397 | pm5.32da 673 |
. . . . . . . . . . . . . . . . . . . 20
|
399 | 398 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
400 | 243, 399 | syl5bb 272 |
. . . . . . . . . . . . . . . . . 18
|
401 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
|
402 | 356, 21 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
403 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
404 | 403 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
405 | 404, 127 | syl6breq 4694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
406 | | lemuldiv2 10904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
407 | 340, 352,
328, 329, 406 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
408 | 405, 407 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
409 | 350 | ltm1d 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
410 | 22, 352, 350, 408, 409 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
411 | 22, 350 | posdifd 10614 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
412 | 410, 411 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
413 | | elnnz 11387 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
414 | 402, 412,
413 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
415 | 68, 70, 300 | sub32d 10424 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
416 | 127, 127 | oveq12i 6662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
417 | 67 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
418 | 417, 214 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
419 | 418 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
420 | 419 | 2halvesd 11278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
421 | 416, 420 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
422 | 421 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
423 | 164 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
424 | 423, 423 | pncan2d 10394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
425 | 422, 424 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
426 | 425, 348 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
427 | 352, 336,
22, 426 | ltsub23d 10632 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
428 | 415, 427 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
429 | 130 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
430 | 429 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
431 | | zlem1lt 11429 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
432 | 402, 430,
431 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
433 | 428, 432 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
434 | | fznn 12408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
435 | 430, 434 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
436 | 414, 433,
435 | mpbir2and 957 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
437 | 436 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
438 | 401, 437 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . 21
|
439 | 438 | biantrurd 529 |
. . . . . . . . . . . . . . . . . . . 20
|
440 | 379 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
|
441 | | fznn 12408 |
. . . . . . . . . . . . . . . . . . . . 21
|
442 | 440, 441 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
443 | 439, 442 | bitr3d 270 |
. . . . . . . . . . . . . . . . . . 19
|
444 | 401 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
|
445 | 444 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . 19
|
446 | 443, 445 | anbi12d 747 |
. . . . . . . . . . . . . . . . . 18
|
447 | 388 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
448 | | fznn 12408 |
. . . . . . . . . . . . . . . . . . 19
|
449 | 447, 448 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
450 | 400, 446,
449 | 3bitr4d 300 |
. . . . . . . . . . . . . . . . 17
|
451 | 242, 450 | syl5bb 272 |
. . . . . . . . . . . . . . . 16
|
452 | 451 | pm5.32da 673 |
. . . . . . . . . . . . . . 15
|
453 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
|
454 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
|
455 | 453, 454 | op1std 7178 |
. . . . . . . . . . . . . . . . . 18
|
456 | 455 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . 17
|
457 | 456 | elrab 3363 |
. . . . . . . . . . . . . . . 16
|
458 | | ancom 466 |
. . . . . . . . . . . . . . . 16
|
459 | 457, 458 | bitri 264 |
. . . . . . . . . . . . . . 15
|
460 | | opelxp 5146 |
. . . . . . . . . . . . . . . 16
|
461 | | velsn 4193 |
. . . . . . . . . . . . . . . . 17
|
462 | 461 | anbi1i 731 |
. . . . . . . . . . . . . . . 16
|
463 | 460, 462 | bitri 264 |
. . . . . . . . . . . . . . 15
|
464 | 452, 459,
463 | 3bitr4g 303 |
. . . . . . . . . . . . . 14
|
465 | 238, 239,
464 | eqrelrdv 5216 |
. . . . . . . . . . . . 13
|
466 | 465 | fveq2d 6195 |
. . . . . . . . . . . 12
|
467 | | fzfid 12772 |
. . . . . . . . . . . . . 14
|
468 | | xpsnen2g 8053 |
. . . . . . . . . . . . . 14
|
469 | 402, 467,
468 | syl2anc 693 |
. . . . . . . . . . . . 13
|
470 | | hasheni 13136 |
. . . . . . . . . . . . 13
|
471 | 469, 470 | syl 17 |
. . . . . . . . . . . 12
|
472 | | ltmul2 10874 |
. . . . . . . . . . . . . . . . . . . . 21
|
473 | 22, 350, 252, 366, 472 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . 20
|
474 | 410, 473 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
|
475 | | ltdivmul2 10900 |
. . . . . . . . . . . . . . . . . . . 20
|
476 | 371, 252,
350, 372, 475 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . 19
|
477 | 474, 476 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
|
478 | 376, 477 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . 17
|
479 | | fllt 12607 |
. . . . . . . . . . . . . . . . . 18
|
480 | 23, 280, 479 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
481 | 478, 480 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
482 | | zltlem1 11430 |
. . . . . . . . . . . . . . . . 17
|
483 | 24, 280, 482 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
484 | 481, 483 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
485 | 484, 298 | breqtrrd 4681 |
. . . . . . . . . . . . . 14
|
486 | | eluz2 11693 |
. . . . . . . . . . . . . 14
|
487 | 24, 387, 485, 486 | syl3anbrc 1246 |
. . . . . . . . . . . . 13
|
488 | | uznn0sub 11719 |
. . . . . . . . . . . . 13
|
489 | | hashfz1 13134 |
. . . . . . . . . . . . 13
|
490 | 487, 488,
489 | 3syl 18 |
. . . . . . . . . . . 12
|
491 | 466, 471,
490 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
492 | 491 | sumeq2dv 14433 |
. . . . . . . . . 10
|
493 | 85, 235, 492 | 3eqtr3rd 2665 |
. . . . . . . . 9
|
494 | 314 | nncnd 11036 |
. . . . . . . . . . 11
|
495 | 494 | adantr 481 |
. . . . . . . . . 10
|
496 | 5, 495, 301 | fsumsub 14520 |
. . . . . . . . 9
|
497 | 493, 496 | eqtr3d 2658 |
. . . . . . . 8
|
498 | 497 | oveq2d 6666 |
. . . . . . 7
|
499 | 25 | zcnd 11483 |
. . . . . . . 8
|
500 | 5, 387 | fsumzcl 14466 |
. . . . . . . . 9
|
501 | 500 | zcnd 11483 |
. . . . . . . 8
|
502 | 499, 501 | pncan3d 10395 |
. . . . . . 7
|
503 | | fsumconst 14522 |
. . . . . . . . 9
|
504 | 5, 494, 503 | syl2anc 693 |
. . . . . . . 8
|
505 | | hashcl 13147 |
. . . . . . . . . . 11
|
506 | 5, 505 | syl 17 |
. . . . . . . . . 10
|
507 | 506 | nn0cnd 11353 |
. . . . . . . . 9
|
508 | | 2cnd 11093 |
. . . . . . . . 9
|
509 | 507, 508,
320 | mul12d 10245 |
. . . . . . . 8
|
510 | 504, 509 | eqtrd 2656 |
. . . . . . 7
|
511 | 498, 502,
510 | 3eqtrd 2660 |
. . . . . 6
|
512 | 511 | oveq2d 6666 |
. . . . 5
|
513 | 17 | a1i 11 |
. . . . . 6
|
514 | 506 | nn0zd 11480 |
. . . . . . 7
|
515 | 514, 379 | zmulcld 11488 |
. . . . . 6
|
516 | | expmulz 12906 |
. . . . . 6
|
517 | 2, 4, 513, 515, 516 | syl22anc 1327 |
. . . . 5
|
518 | | neg1sqe1 12959 |
. . . . . . 7
|
519 | 518 | oveq1i 6660 |
. . . . . 6
|
520 | | 1exp 12889 |
. . . . . . 7
|
521 | 515, 520 | syl 17 |
. . . . . 6
|
522 | 519, 521 | syl5eq 2668 |
. . . . 5
|
523 | 512, 517,
522 | 3eqtrd 2660 |
. . . 4
|
524 | 45, 56, 523 | 3eqtr4d 2666 |
. . 3
|
525 | | expaddz 12904 |
. . . 4
|
526 | 2, 4, 25, 43, 525 | syl22anc 1327 |
. . 3
|
527 | 524, 526 | eqtr2d 2657 |
. 2
|
528 | 26, 42, 42, 44, 527 | mulcan2ad 10663 |
1
|