Step | Hyp | Ref
| Expression |
1 | | perfectALTVlem.2 |
. . . 4
|
2 | | 1re 10039 |
. . . . . 6
|
3 | 2 | a1i 11 |
. . . . 5
|
4 | | perfectALTVlem.1 |
. . . . . . . 8
|
5 | | perfectALTVlem.3 |
. . . . . . . 8
Odd |
6 | | perfectALTVlem.4 |
. . . . . . . 8
|
7 | 4, 1, 5, 6 | perfectALTVlem1 41630 |
. . . . . . 7
|
8 | 7 | simp3d 1075 |
. . . . . 6
|
9 | 8 | nnred 11035 |
. . . . 5
|
10 | 1 | nnred 11035 |
. . . . 5
|
11 | 8 | nnge1d 11063 |
. . . . 5
|
12 | | 2cn 11091 |
. . . . . . . . . . 11
|
13 | | exp1 12866 |
. . . . . . . . . . 11
|
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . 10
|
15 | | df-2 11079 |
. . . . . . . . . 10
|
16 | 14, 15 | eqtri 2644 |
. . . . . . . . 9
|
17 | | 2re 11090 |
. . . . . . . . . . 11
|
18 | 17 | a1i 11 |
. . . . . . . . . 10
|
19 | | 1zzd 11408 |
. . . . . . . . . 10
|
20 | 4 | peano2nnd 11037 |
. . . . . . . . . . 11
|
21 | 20 | nnzd 11481 |
. . . . . . . . . 10
|
22 | | 1lt2 11194 |
. . . . . . . . . . 11
|
23 | 22 | a1i 11 |
. . . . . . . . . 10
|
24 | 4 | nnrpd 11870 |
. . . . . . . . . . . 12
|
25 | | ltaddrp 11867 |
. . . . . . . . . . . 12
|
26 | 2, 24, 25 | sylancr 695 |
. . . . . . . . . . 11
|
27 | | ax-1cn 9994 |
. . . . . . . . . . . 12
|
28 | 4 | nncnd 11036 |
. . . . . . . . . . . 12
|
29 | | addcom 10222 |
. . . . . . . . . . . 12
|
30 | 27, 28, 29 | sylancr 695 |
. . . . . . . . . . 11
|
31 | 26, 30 | breqtrd 4679 |
. . . . . . . . . 10
|
32 | | ltexp2a 12912 |
. . . . . . . . . 10
|
33 | 18, 19, 21, 23, 31, 32 | syl32anc 1334 |
. . . . . . . . 9
|
34 | 16, 33 | syl5eqbrr 4689 |
. . . . . . . 8
|
35 | 7 | simp1d 1073 |
. . . . . . . . . 10
|
36 | 35 | nnred 11035 |
. . . . . . . . 9
|
37 | 3, 3, 36 | ltaddsubd 10627 |
. . . . . . . 8
|
38 | 34, 37 | mpbid 222 |
. . . . . . 7
|
39 | | 1rp 11836 |
. . . . . . . . 9
|
40 | 39 | a1i 11 |
. . . . . . . 8
|
41 | | peano2rem 10348 |
. . . . . . . . . . 11
|
42 | 36, 41 | syl 17 |
. . . . . . . . . 10
|
43 | | expgt1 12898 |
. . . . . . . . . . . 12
|
44 | 18, 20, 23, 43 | syl3anc 1326 |
. . . . . . . . . . 11
|
45 | | posdif 10521 |
. . . . . . . . . . . 12
|
46 | 2, 36, 45 | sylancr 695 |
. . . . . . . . . . 11
|
47 | 44, 46 | mpbid 222 |
. . . . . . . . . 10
|
48 | 42, 47 | jca 554 |
. . . . . . . . 9
|
49 | | elrp 11834 |
. . . . . . . . 9
|
50 | 48, 49 | sylibr 224 |
. . . . . . . 8
|
51 | | nnrp 11842 |
. . . . . . . . 9
|
52 | 1, 51 | syl 17 |
. . . . . . . 8
|
53 | 40, 50, 52 | ltdiv2d 11895 |
. . . . . . 7
|
54 | 38, 53 | mpbid 222 |
. . . . . 6
|
55 | 1 | nncnd 11036 |
. . . . . . 7
|
56 | 55 | div1d 10793 |
. . . . . 6
|
57 | 54, 56 | breqtrd 4679 |
. . . . 5
|
58 | 3, 9, 10, 11, 57 | lelttrd 10195 |
. . . 4
|
59 | | eluz2b2 11761 |
. . . 4
|
60 | 1, 58, 59 | sylanbrc 698 |
. . 3
|
61 | | fzfid 12772 |
. . . . . . . . . . . 12
|
62 | | dvdsssfz1 15040 |
. . . . . . . . . . . . 13
|
63 | 1, 62 | syl 17 |
. . . . . . . . . . . 12
|
64 | | ssfi 8180 |
. . . . . . . . . . . 12
|
65 | 61, 63, 64 | syl2anc 693 |
. . . . . . . . . . 11
|
66 | 65 | ad2antrr 762 |
. . . . . . . . . 10
|
67 | | ssrab2 3687 |
. . . . . . . . . . . . 13
|
68 | 67 | a1i 11 |
. . . . . . . . . . . 12
|
69 | 68 | sselda 3603 |
. . . . . . . . . . 11
|
70 | 69 | nnred 11035 |
. . . . . . . . . 10
|
71 | 69 | nnnn0d 11351 |
. . . . . . . . . . 11
|
72 | 71 | nn0ge0d 11354 |
. . . . . . . . . 10
|
73 | | df-tp 4182 |
. . . . . . . . . . . 12
|
74 | | prssi 4353 |
. . . . . . . . . . . . . . 15
|
75 | 8, 1, 74 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
76 | 75 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
77 | | simplrl 800 |
. . . . . . . . . . . . . 14
|
78 | 77 | snssd 4340 |
. . . . . . . . . . . . 13
|
79 | 76, 78 | unssd 3789 |
. . . . . . . . . . . 12
|
80 | 73, 79 | syl5eqss 3649 |
. . . . . . . . . . 11
|
81 | | eltpi 4229 |
. . . . . . . . . . . . 13
|
82 | 7 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . 19
|
83 | 82 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
|
84 | 8 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
|
85 | | dvdsmul2 15004 |
. . . . . . . . . . . . . . . . . 18
|
86 | 83, 84, 85 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
87 | 82 | nncnd 11036 |
. . . . . . . . . . . . . . . . . 18
|
88 | 82 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . 18
|
89 | 55, 87, 88 | divcan2d 10803 |
. . . . . . . . . . . . . . . . 17
|
90 | 86, 89 | breqtrd 4679 |
. . . . . . . . . . . . . . . 16
|
91 | | breq1 4656 |
. . . . . . . . . . . . . . . 16
|
92 | 90, 91 | syl5ibrcom 237 |
. . . . . . . . . . . . . . 15
|
93 | 92 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
94 | 1 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
|
95 | | iddvds 14995 |
. . . . . . . . . . . . . . . . 17
|
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
|
97 | | breq1 4656 |
. . . . . . . . . . . . . . . 16
|
98 | 96, 97 | syl5ibrcom 237 |
. . . . . . . . . . . . . . 15
|
99 | 98 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
100 | | simplrr 801 |
. . . . . . . . . . . . . . 15
|
101 | | breq1 4656 |
. . . . . . . . . . . . . . 15
|
102 | 100, 101 | syl5ibrcom 237 |
. . . . . . . . . . . . . 14
|
103 | 93, 99, 102 | 3jaod 1392 |
. . . . . . . . . . . . 13
|
104 | 81, 103 | syl5 34 |
. . . . . . . . . . . 12
|
105 | 104 | imp 445 |
. . . . . . . . . . 11
|
106 | 80, 105 | ssrabdv 3681 |
. . . . . . . . . 10
|
107 | 66, 70, 72, 106 | fsumless 14528 |
. . . . . . . . 9
|
108 | | simpr 477 |
. . . . . . . . . . . 12
|
109 | | disjsn 4246 |
. . . . . . . . . . . 12
|
110 | 108, 109 | sylibr 224 |
. . . . . . . . . . 11
|
111 | 73 | a1i 11 |
. . . . . . . . . . 11
|
112 | | tpfi 8236 |
. . . . . . . . . . . 12
|
113 | 112 | a1i 11 |
. . . . . . . . . . 11
|
114 | 80 | sselda 3603 |
. . . . . . . . . . . 12
|
115 | 114 | nncnd 11036 |
. . . . . . . . . . 11
|
116 | 110, 111,
113, 115 | fsumsplit 14471 |
. . . . . . . . . 10
|
117 | 8 | nncnd 11036 |
. . . . . . . . . . . . . . 15
|
118 | | id 22 |
. . . . . . . . . . . . . . . 16
|
119 | 118 | sumsn 14475 |
. . . . . . . . . . . . . . 15
|
120 | 8, 117, 119 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
121 | | id 22 |
. . . . . . . . . . . . . . . 16
|
122 | 121 | sumsn 14475 |
. . . . . . . . . . . . . . 15
|
123 | 1, 55, 122 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
124 | 120, 123 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
125 | | incom 3805 |
. . . . . . . . . . . . . . 15
|
126 | 9, 57 | gtned 10172 |
. . . . . . . . . . . . . . . 16
|
127 | | disjsn2 4247 |
. . . . . . . . . . . . . . . 16
|
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . 15
|
129 | 125, 128 | syl5eqr 2670 |
. . . . . . . . . . . . . 14
|
130 | | df-pr 4180 |
. . . . . . . . . . . . . . 15
|
131 | 130 | a1i 11 |
. . . . . . . . . . . . . 14
|
132 | | prfi 8235 |
. . . . . . . . . . . . . . 15
|
133 | 132 | a1i 11 |
. . . . . . . . . . . . . 14
|
134 | 75 | sselda 3603 |
. . . . . . . . . . . . . . 15
|
135 | 134 | nncnd 11036 |
. . . . . . . . . . . . . 14
|
136 | 129, 131,
133, 135 | fsumsplit 14471 |
. . . . . . . . . . . . 13
|
137 | 87, 55 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
138 | 55, 137, 87, 88 | divdird 10839 |
. . . . . . . . . . . . . 14
|
139 | 35 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
|
140 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
141 | 139, 140,
55 | subdird 10487 |
. . . . . . . . . . . . . . . . . . 19
|
142 | 55 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . . . 20
|
143 | 142 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
144 | 141, 143 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
145 | 144 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
146 | 139, 55 | mulcld 10060 |
. . . . . . . . . . . . . . . . . 18
|
147 | 55, 146 | pncan3d 10395 |
. . . . . . . . . . . . . . . . 17
|
148 | 145, 147 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
149 | 148 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
150 | 139, 55, 87, 88 | divassd 10836 |
. . . . . . . . . . . . . . 15
|
151 | 149, 150 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
152 | 55, 87, 88 | divcan3d 10806 |
. . . . . . . . . . . . . . 15
|
153 | 152 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
154 | 138, 151,
153 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
|
155 | 124, 136,
154 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
|
156 | 155 | ad2antrr 762 |
. . . . . . . . . . 11
|
157 | 77 | nncnd 11036 |
. . . . . . . . . . . 12
|
158 | | id 22 |
. . . . . . . . . . . . 13
|
159 | 158 | sumsn 14475 |
. . . . . . . . . . . 12
|
160 | 157, 157,
159 | syl2anc 693 |
. . . . . . . . . . 11
|
161 | 156, 160 | oveq12d 6668 |
. . . . . . . . . 10
|
162 | 116, 161 | eqtrd 2656 |
. . . . . . . . 9
|
163 | 4 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . 17
|
164 | | expp1 12867 |
. . . . . . . . . . . . . . . . 17
|
165 | 12, 163, 164 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
166 | | 2nn 11185 |
. . . . . . . . . . . . . . . . . . 19
|
167 | | nnexpcl 12873 |
. . . . . . . . . . . . . . . . . . 19
|
168 | 166, 163,
167 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
|
169 | 168 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
|
170 | | mulcom 10022 |
. . . . . . . . . . . . . . . . 17
|
171 | 169, 12, 170 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
172 | 165, 171 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
173 | 172 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
174 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
|
175 | 174, 169,
55 | mulassd 10063 |
. . . . . . . . . . . . . 14
|
176 | | isodd7 41577 |
. . . . . . . . . . . . . . . . . . 19
Odd |
177 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
|
178 | 176, 177 | sylbi 207 |
. . . . . . . . . . . . . . . . . 18
Odd |
179 | 5, 178 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
180 | | 2z 11409 |
. . . . . . . . . . . . . . . . . . 19
|
181 | 180 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
182 | | rpexp1i 15433 |
. . . . . . . . . . . . . . . . . 18
|
183 | 181, 94, 163, 182 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
184 | 179, 183 | mpd 15 |
. . . . . . . . . . . . . . . 16
|
185 | | sgmmul 24926 |
. . . . . . . . . . . . . . . 16
|
186 | 140, 168,
1, 184, 185 | syl13anc 1328 |
. . . . . . . . . . . . . . 15
|
187 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . 20
|
188 | 28, 27, 187 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
|
189 | 188 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
|
190 | 189 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
191 | | 1sgm2ppw 24925 |
. . . . . . . . . . . . . . . . . 18
|
192 | 20, 191 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
193 | 190, 192 | eqtr3d 2658 |
. . . . . . . . . . . . . . . 16
|
194 | 193 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
195 | 186, 6, 194 | 3eqtr3d 2664 |
. . . . . . . . . . . . . 14
|
196 | 173, 175,
195 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
|
197 | 196 | oveq1d 6665 |
. . . . . . . . . . . 12
|
198 | | 1nn0 11308 |
. . . . . . . . . . . . . . 15
|
199 | | sgmnncl 24873 |
. . . . . . . . . . . . . . 15
|
200 | 198, 1, 199 | sylancr 695 |
. . . . . . . . . . . . . 14
|
201 | 200 | nncnd 11036 |
. . . . . . . . . . . . 13
|
202 | 201, 87, 88 | divcan3d 10806 |
. . . . . . . . . . . 12
|
203 | 197, 150,
202 | 3eqtr3d 2664 |
. . . . . . . . . . 11
|
204 | | sgmval 24868 |
. . . . . . . . . . . 12
|
205 | 27, 1, 204 | sylancr 695 |
. . . . . . . . . . 11
|
206 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
207 | 67, 206 | sseldi 3601 |
. . . . . . . . . . . . . 14
|
208 | 207 | nncnd 11036 |
. . . . . . . . . . . . 13
|
209 | 208 | cxp1d 24452 |
. . . . . . . . . . . 12
|
210 | 209 | sumeq2dv 14433 |
. . . . . . . . . . 11
|
211 | 203, 205,
210 | 3eqtrrd 2661 |
. . . . . . . . . 10
|
212 | 211 | ad2antrr 762 |
. . . . . . . . 9
|
213 | 107, 162,
212 | 3brtr3d 4684 |
. . . . . . . 8
|
214 | 36, 9 | remulcld 10070 |
. . . . . . . . . . 11
|
215 | 214 | ad2antrr 762 |
. . . . . . . . . 10
|
216 | 77 | nnrpd 11870 |
. . . . . . . . . 10
|
217 | 215, 216 | ltaddrpd 11905 |
. . . . . . . . 9
|
218 | 77 | nnred 11035 |
. . . . . . . . . . 11
|
219 | 215, 218 | readdcld 10069 |
. . . . . . . . . 10
|
220 | 215, 219 | ltnled 10184 |
. . . . . . . . 9
|
221 | 217, 220 | mpbid 222 |
. . . . . . . 8
|
222 | 213, 221 | condan 835 |
. . . . . . 7
|
223 | | elpri 4197 |
. . . . . . 7
|
224 | 222, 223 | syl 17 |
. . . . . 6
|
225 | 224 | expr 643 |
. . . . 5
|
226 | 225 | ralrimiva 2966 |
. . . 4
|
227 | 3, 58 | gtned 10172 |
. . . . . . . . . 10
|
228 | 227 | necomd 2849 |
. . . . . . . . 9
|
229 | | 1nn 11031 |
. . . . . . . . . . . . 13
|
230 | 229 | a1i 11 |
. . . . . . . . . . . 12
|
231 | | 1dvds 14996 |
. . . . . . . . . . . . 13
|
232 | 94, 231 | syl 17 |
. . . . . . . . . . . 12
|
233 | | breq1 4656 |
. . . . . . . . . . . . . 14
|
234 | | eqeq1 2626 |
. . . . . . . . . . . . . . 15
|
235 | | eqeq1 2626 |
. . . . . . . . . . . . . . 15
|
236 | 234, 235 | orbi12d 746 |
. . . . . . . . . . . . . 14
|
237 | 233, 236 | imbi12d 334 |
. . . . . . . . . . . . 13
|
238 | 237 | rspcv 3305 |
. . . . . . . . . . . 12
|
239 | 230, 226,
232, 238 | syl3c 66 |
. . . . . . . . . . 11
|
240 | 239 | ord 392 |
. . . . . . . . . 10
|
241 | 240 | necon1ad 2811 |
. . . . . . . . 9
|
242 | 228, 241 | mpd 15 |
. . . . . . . 8
|
243 | 242 | eqeq2d 2632 |
. . . . . . 7
|
244 | 243 | orbi1d 739 |
. . . . . 6
|
245 | 244 | imbi2d 330 |
. . . . 5
|
246 | 245 | ralbidv 2986 |
. . . 4
|
247 | 226, 246 | mpbird 247 |
. . 3
|
248 | | isprm2 15395 |
. . 3
|
249 | 60, 247, 248 | sylanbrc 698 |
. 2
|
250 | 214 | ltp1d 10954 |
. . . 4
|
251 | | peano2re 10209 |
. . . . . 6
|
252 | 214, 251 | syl 17 |
. . . . 5
|
253 | 214, 252 | ltnled 10184 |
. . . 4
|
254 | 250, 253 | mpbid 222 |
. . 3
|
255 | 207 | nnred 11035 |
. . . . . . . 8
|
256 | 207 | nnnn0d 11351 |
. . . . . . . . 9
|
257 | 256 | nn0ge0d 11354 |
. . . . . . . 8
|
258 | | df-tp 4182 |
. . . . . . . . . 10
|
259 | | snssi 4339 |
. . . . . . . . . . . 12
|
260 | 229, 259 | mp1i 13 |
. . . . . . . . . . 11
|
261 | 75, 260 | unssd 3789 |
. . . . . . . . . 10
|
262 | 258, 261 | syl5eqss 3649 |
. . . . . . . . 9
|
263 | | eltpi 4229 |
. . . . . . . . . . 11
|
264 | | breq1 4656 |
. . . . . . . . . . . . 13
|
265 | 232, 264 | syl5ibrcom 237 |
. . . . . . . . . . . 12
|
266 | 92, 98, 265 | 3jaod 1392 |
. . . . . . . . . . 11
|
267 | 263, 266 | syl5 34 |
. . . . . . . . . 10
|
268 | 267 | imp 445 |
. . . . . . . . 9
|
269 | 262, 268 | ssrabdv 3681 |
. . . . . . . 8
|
270 | 65, 255, 257, 269 | fsumless 14528 |
. . . . . . 7
|
271 | 270 | adantr 481 |
. . . . . 6
|
272 | 55, 87, 88 | diveq1ad 10810 |
. . . . . . . . . . . . 13
|
273 | 272 | necon3bid 2838 |
. . . . . . . . . . . 12
|
274 | 273 | biimpar 502 |
. . . . . . . . . . 11
|
275 | 274 | necomd 2849 |
. . . . . . . . . 10
|
276 | 228 | adantr 481 |
. . . . . . . . . 10
|
277 | 275, 276 | nelprd 4203 |
. . . . . . . . 9
|
278 | | disjsn 4246 |
. . . . . . . . 9
|
279 | 277, 278 | sylibr 224 |
. . . . . . . 8
|
280 | 258 | a1i 11 |
. . . . . . . 8
|
281 | | tpfi 8236 |
. . . . . . . . 9
|
282 | 281 | a1i 11 |
. . . . . . . 8
|
283 | 262 | adantr 481 |
. . . . . . . . . 10
|
284 | 283 | sselda 3603 |
. . . . . . . . 9
|
285 | 284 | nncnd 11036 |
. . . . . . . 8
|
286 | 279, 280,
282, 285 | fsumsplit 14471 |
. . . . . . 7
|
287 | | id 22 |
. . . . . . . . . . 11
|
288 | 287 | sumsn 14475 |
. . . . . . . . . 10
|
289 | 140, 27, 288 | sylancl 694 |
. . . . . . . . 9
|
290 | 155, 289 | oveq12d 6668 |
. . . . . . . 8
|
291 | 290 | adantr 481 |
. . . . . . 7
|
292 | 286, 291 | eqtrd 2656 |
. . . . . 6
|
293 | 211 | adantr 481 |
. . . . . 6
|
294 | 271, 292,
293 | 3brtr3d 4684 |
. . . . 5
|
295 | 294 | ex 450 |
. . . 4
|
296 | 295 | necon1bd 2812 |
. . 3
|
297 | 254, 296 | mpd 15 |
. 2
|
298 | 249, 297 | jca 554 |
1
|