Step | Hyp | Ref
| Expression |
1 | | eulerpart.p |
. . . . 5
|
2 | | eulerpart.o |
. . . . 5
|
3 | | eulerpart.d |
. . . . 5
|
4 | | eulerpart.j |
. . . . 5
|
5 | | eulerpart.f |
. . . . 5
|
6 | | eulerpart.h |
. . . . 5
supp |
7 | | eulerpart.m |
. . . . 5
|
8 | | eulerpart.r |
. . . . 5
|
9 | | eulerpart.t |
. . . . 5
|
10 | | eulerpart.g |
. . . . 5
𝟭bits |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemgv 30435 |
. . . 4
𝟭bits |
12 | 11 | fveq1d 6193 |
. . 3
𝟭bits |
13 | 12 | adantr 481 |
. 2
𝟭bits |
14 | | nnex 11026 |
. . 3
|
15 | | imassrn 5477 |
. . . 4
bits
|
16 | 4, 5 | oddpwdc 30416 |
. . . . 5
|
17 | | f1of 6137 |
. . . . 5
|
18 | | frn 6053 |
. . . . 5
|
19 | 16, 17, 18 | mp2b 10 |
. . . 4
|
20 | 15, 19 | sstri 3612 |
. . 3
bits
|
21 | | simpr 477 |
. . 3
|
22 | | indfval 30078 |
. . 3
bits 𝟭bits bits |
23 | 14, 20, 21, 22 | mp3an12i 1428 |
. 2
𝟭bits bits |
24 | | ffn 6045 |
. . . . . 6
|
25 | 16, 17, 24 | mp2b 10 |
. . . . 5
|
26 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemmf 30437 |
. . . . . . . . 9
bits
|
27 | 1, 2, 3, 4, 5, 6, 7 | eulerpartlem1 30429 |
. . . . . . . . . . 11
|
28 | | f1of 6137 |
. . . . . . . . . . 11
|
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . 10
|
30 | 29 | ffvelrni 6358 |
. . . . . . . . 9
bits
bits |
31 | 26, 30 | syl 17 |
. . . . . . . 8
bits |
32 | 31 | elin1d 3802 |
. . . . . . 7
bits |
33 | 32 | adantr 481 |
. . . . . 6
bits
|
34 | 33 | elpwid 4170 |
. . . . 5
bits |
35 | | fvelimab 6253 |
. . . . 5
bits
bits
bits |
36 | 25, 34, 35 | sylancr 695 |
. . . 4
bits
bits |
37 | 4 | ssrab3 3688 |
. . . . . . . . 9
|
38 | 7 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
39 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . 20
bits bits |
40 | 39 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . 19
bits bits |
41 | 40 | anbi2d 740 |
. . . . . . . . . . . . . . . . . 18
bits
bits |
42 | 41 | opabbidv 4716 |
. . . . . . . . . . . . . . . . 17
bits
bits |
43 | 42 | adantl 482 |
. . . . . . . . . . . . . . . 16
bits
bits |
44 | 14, 37 | ssexi 4803 |
. . . . . . . . . . . . . . . . . 18
|
45 | | abid2 2745 |
. . . . . . . . . . . . . . . . . . . 20
bits bits
|
46 | 45 | fvexi 6202 |
. . . . . . . . . . . . . . . . . . 19
bits |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
bits |
48 | 44, 47 | opabex3 7146 |
. . . . . . . . . . . . . . . . 17
bits |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . 16
bits |
50 | 38, 43, 26, 49 | fvmptd 6288 |
. . . . . . . . . . . . . . 15
bits
bits |
51 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
|
52 | 51 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
|
53 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
54 | 51 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
bits bits |
55 | 53, 54 | eleq12d 2695 |
. . . . . . . . . . . . . . . . 17
bits
bits
|
56 | 52, 55 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
bits
bits
|
57 | 56 | cbvopabv 4722 |
. . . . . . . . . . . . . . 15
bits
bits
|
58 | 50, 57 | syl6eq 2672 |
. . . . . . . . . . . . . 14
bits
bits |
59 | 58 | eleq2d 2687 |
. . . . . . . . . . . . 13
bits
bits
|
60 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | eulerpartlemt0 30431 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
61 | 60 | simp1bi 1076 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
62 | | nn0ex 11298 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
63 | 62, 14 | elmap 7886 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
64 | 61, 63 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . 22
|
65 | | ffun 6048 |
. . . . . . . . . . . . . . . . . . . . . 22
|
66 | | funres 5929 |
. . . . . . . . . . . . . . . . . . . . . 22
|
67 | 64, 65, 66 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
|
68 | | fssres 6070 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
69 | 64, 37, 68 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
70 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
71 | 70 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
72 | 69, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
73 | 72 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . 21
|
74 | | fvco 6274 |
. . . . . . . . . . . . . . . . . . . . 21
bits bits |
75 | 67, 73, 74 | syl2an2r 876 |
. . . . . . . . . . . . . . . . . . . 20
bits bits |
76 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . . 22
|
77 | 76 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
bits bits |
78 | 77 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
bits bits |
79 | 75, 78 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
bits bits |
80 | 79 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . 18
bits
bits |
81 | 80 | pm5.32da 673 |
. . . . . . . . . . . . . . . . 17
bits bits |
82 | 81 | opabbidv 4716 |
. . . . . . . . . . . . . . . 16
bits
bits |
83 | 82 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
bits
bits |
84 | | elopab 4983 |
. . . . . . . . . . . . . . 15
bits
bits |
85 | 83, 84 | syl6bb 276 |
. . . . . . . . . . . . . 14
bits
bits |
86 | | ancom 466 |
. . . . . . . . . . . . . . . . 17
bits
bits |
87 | | anass 681 |
. . . . . . . . . . . . . . . . 17
bits
bits |
88 | 86, 87 | bitri 264 |
. . . . . . . . . . . . . . . 16
bits
bits |
89 | 88 | 2exbii 1775 |
. . . . . . . . . . . . . . 15
bits
bits
|
90 | | df-rex 2918 |
. . . . . . . . . . . . . . . . . 18
bits
bits |
91 | 90 | anbi2i 730 |
. . . . . . . . . . . . . . . . 17
bits bits
|
92 | 91 | exbii 1774 |
. . . . . . . . . . . . . . . 16
bits bits
|
93 | | df-rex 2918 |
. . . . . . . . . . . . . . . 16
bits
bits |
94 | | exdistr 1919 |
. . . . . . . . . . . . . . . 16
bits
bits
|
95 | 92, 93, 94 | 3bitr4i 292 |
. . . . . . . . . . . . . . 15
bits
bits
|
96 | 89, 95 | bitr4i 267 |
. . . . . . . . . . . . . 14
bits
bits |
97 | 85, 96 | syl6bb 276 |
. . . . . . . . . . . . 13
bits
bits |
98 | 59, 97 | bitrd 268 |
. . . . . . . . . . . 12
bits
bits |
99 | 98 | biimpa 501 |
. . . . . . . . . . 11
bits
bits |
100 | 99 | adantlr 751 |
. . . . . . . . . 10
bits
bits |
101 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
102 | 101 | adantl 482 |
. . . . . . . . . . . . 13
bits
bits |
103 | | bitsss 15148 |
. . . . . . . . . . . . . . . . 17
bits
|
104 | 103 | sseli 3599 |
. . . . . . . . . . . . . . . 16
bits
|
105 | 104 | anim2i 593 |
. . . . . . . . . . . . . . 15
bits
|
106 | 105 | ad2antlr 763 |
. . . . . . . . . . . . . 14
bits
bits
|
107 | | opelxp 5146 |
. . . . . . . . . . . . . . 15
|
108 | 4, 5 | oddpwdcv 30417 |
. . . . . . . . . . . . . . . 16
|
109 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
|
110 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
|
111 | 109, 110 | op2nd 7177 |
. . . . . . . . . . . . . . . . . 18
|
112 | 111 | oveq2i 6661 |
. . . . . . . . . . . . . . . . 17
|
113 | 109, 110 | op1st 7176 |
. . . . . . . . . . . . . . . . 17
|
114 | 112, 113 | oveq12i 6662 |
. . . . . . . . . . . . . . . 16
|
115 | 108, 114 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
116 | 107, 115 | sylbir 225 |
. . . . . . . . . . . . . 14
|
117 | 106, 116 | syl 17 |
. . . . . . . . . . . . 13
bits
bits |
118 | 102, 117 | eqtr2d 2657 |
. . . . . . . . . . . 12
bits
bits |
119 | 118 | ex 450 |
. . . . . . . . . . 11
bits
bits |
120 | 119 | reximdvva 3019 |
. . . . . . . . . 10
bits
bits
bits |
121 | 100, 120 | mpd 15 |
. . . . . . . . 9
bits
bits |
122 | | ssrexv 3667 |
. . . . . . . . 9
bits bits |
123 | 37, 121, 122 | mpsyl 68 |
. . . . . . . 8
bits
bits |
124 | 123 | adantr 481 |
. . . . . . 7
bits
bits |
125 | | eqeq2 2633 |
. . . . . . . . . 10
|
126 | 125 | rexbidv 3052 |
. . . . . . . . 9
bits bits |
127 | 126 | adantl 482 |
. . . . . . . 8
bits bits
bits |
128 | 127 | rexbidv 3052 |
. . . . . . 7
bits bits
bits |
129 | 124, 128 | mpbid 222 |
. . . . . 6
bits
bits |
130 | 129 | r19.29an 3077 |
. . . . 5
bits bits |
131 | | simp-5l 808 |
. . . . . . . 8
bits bits
|
132 | | simpllr 799 |
. . . . . . . 8
bits bits
|
133 | | simplr 792 |
. . . . . . . . 9
bits bits
bits |
134 | 70 | eleq2d 2687 |
. . . . . . . . . . . . . 14
|
135 | 69, 134 | syl 17 |
. . . . . . . . . . . . 13
|
136 | 135 | biimpar 502 |
. . . . . . . . . . . 12
|
137 | | fvco 6274 |
. . . . . . . . . . . 12
bits bits |
138 | 67, 136, 137 | syl2an2r 876 |
. . . . . . . . . . 11
bits bits |
139 | | fvres 6207 |
. . . . . . . . . . . . 13
|
140 | 139 | fveq2d 6195 |
. . . . . . . . . . . 12
bits bits |
141 | 140 | adantl 482 |
. . . . . . . . . . 11
bits bits |
142 | 138, 141 | eqtrd 2656 |
. . . . . . . . . 10
bits bits |
143 | 131, 132,
142 | syl2anc 693 |
. . . . . . . . 9
bits bits
bits bits |
144 | 133, 143 | eleqtrrd 2704 |
. . . . . . . 8
bits bits
bits
|
145 | 50 | eleq2d 2687 |
. . . . . . . . . 10
bits
bits |
146 | | opabid 4982 |
. . . . . . . . . 10
bits bits |
147 | 145, 146 | syl6bb 276 |
. . . . . . . . 9
bits
bits |
148 | 147 | biimpar 502 |
. . . . . . . 8
bits
bits |
149 | 131, 132,
144, 148 | syl12anc 1324 |
. . . . . . 7
bits bits
bits |
150 | | simpr 477 |
. . . . . . . 8
bits bits
|
151 | 34 | ad4antr 768 |
. . . . . . . . 9
bits bits
bits |
152 | 151, 149 | sseldd 3604 |
. . . . . . . 8
bits bits
|
153 | | opeq1 4402 |
. . . . . . . . . . . 12
|
154 | 153 | eleq1d 2686 |
. . . . . . . . . . 11
|
155 | 153 | fveq2d 6195 |
. . . . . . . . . . . 12
|
156 | | oveq2 6658 |
. . . . . . . . . . . 12
|
157 | 155, 156 | eqeq12d 2637 |
. . . . . . . . . . 11
|
158 | 154, 157 | imbi12d 334 |
. . . . . . . . . 10
|
159 | | opeq2 4403 |
. . . . . . . . . . . . 13
|
160 | 159 | eleq1d 2686 |
. . . . . . . . . . . 12
|
161 | 159 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
162 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
163 | 162 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
164 | 161, 163 | eqeq12d 2637 |
. . . . . . . . . . . 12
|
165 | 160, 164 | imbi12d 334 |
. . . . . . . . . . 11
|
166 | 165, 115 | chvarv 2263 |
. . . . . . . . . 10
|
167 | 158, 166 | chvarv 2263 |
. . . . . . . . 9
|
168 | | eqeq2 2633 |
. . . . . . . . . 10
|
169 | 168 | biimpa 501 |
. . . . . . . . 9
|
170 | 167, 169 | sylan2 491 |
. . . . . . . 8
|
171 | 150, 152,
170 | syl2anc 693 |
. . . . . . 7
bits bits
|
172 | | fveq2 6191 |
. . . . . . . . 9
|
173 | 172 | eqeq1d 2624 |
. . . . . . . 8
|
174 | 173 | rspcev 3309 |
. . . . . . 7
bits
bits |
175 | 149, 171,
174 | syl2anc 693 |
. . . . . 6
bits bits
bits |
176 | | oveq2 6658 |
. . . . . . . . . . 11
|
177 | 176 | eqeq1d 2624 |
. . . . . . . . . 10
|
178 | 162 | oveq1d 6665 |
. . . . . . . . . . 11
|
179 | 178 | eqeq1d 2624 |
. . . . . . . . . 10
|
180 | 177, 179 | sylan9bb 736 |
. . . . . . . . 9
|
181 | | simpl 473 |
. . . . . . . . . . 11
|
182 | 181 | fveq2d 6195 |
. . . . . . . . . 10
|
183 | 182 | fveq2d 6195 |
. . . . . . . . 9
bits bits |
184 | 180, 183 | cbvrexdva2 3176 |
. . . . . . . 8
bits bits |
185 | 184 | cbvrexv 3172 |
. . . . . . 7
bits
bits |
186 | | nfv 1843 |
. . . . . . . . . . . . . 14
|
187 | | nfv 1843 |
. . . . . . . . . . . . . . 15
|
188 | | nfre1 3005 |
. . . . . . . . . . . . . . 15
bits |
189 | 187, 188 | nfan 1828 |
. . . . . . . . . . . . . 14
bits |
190 | 186, 189 | nfan 1828 |
. . . . . . . . . . . . 13
bits |
191 | | simplr 792 |
. . . . . . . . . . . . . . . 16
bits
|
192 | | n0i 3920 |
. . . . . . . . . . . . . . . . . . . 20
bits
bits |
193 | 192 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
bits bits |
194 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
bits bits |
195 | | 0bits 15161 |
. . . . . . . . . . . . . . . . . . . 20
bits |
196 | 194, 195 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
bits |
197 | 193, 196 | nsyl 135 |
. . . . . . . . . . . . . . . . . 18
bits |
198 | 64 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . 22
|
199 | 198 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
bits |
200 | | elnn0 11294 |
. . . . . . . . . . . . . . . . . . . . 21
|
201 | 199, 200 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
bits |
202 | 201 | orcomd 403 |
. . . . . . . . . . . . . . . . . . 19
bits |
203 | 202 | orcanai 952 |
. . . . . . . . . . . . . . . . . 18
bits |
204 | 197, 203 | mpdan 702 |
. . . . . . . . . . . . . . . . 17
bits |
205 | 60 | simp3bi 1078 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
206 | 205 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
207 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
208 | 207 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
209 | 208, 4 | elrab2 3366 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
210 | 209 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
211 | 206, 210 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
212 | 211 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . 21
|
213 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
214 | | elpreima 6337 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
215 | 64, 213, 214 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
216 | 215 | imbi1d 331 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
217 | | impexp 462 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
218 | 216, 217 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . . . 22
|
219 | 218 | ralbidv2 2984 |
. . . . . . . . . . . . . . . . . . . . 21
|
220 | 212, 219 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
|
221 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
222 | 221 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . 22
|
223 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
224 | 223 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . 22
|
225 | 222, 224 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . 21
|
226 | 225 | cbvralv 3171 |
. . . . . . . . . . . . . . . . . . . 20
|
227 | 220, 226 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
|
228 | 227 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . 18
|
229 | 228 | imp 445 |
. . . . . . . . . . . . . . . . 17
|
230 | 204, 229 | syldan 487 |
. . . . . . . . . . . . . . . 16
bits
|
231 | | breq2 4657 |
. . . . . . . . . . . . . . . . . 18
|
232 | 231 | notbid 308 |
. . . . . . . . . . . . . . . . 17
|
233 | 232, 4 | elrab2 3366 |
. . . . . . . . . . . . . . . 16
|
234 | 191, 230,
233 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
bits
|
235 | 234 | adantlrr 757 |
. . . . . . . . . . . . . 14
bits bits
|
236 | 235 | adantr 481 |
. . . . . . . . . . . . 13
bits bits |
237 | | simprr 796 |
. . . . . . . . . . . . 13
bits
bits |
238 | 190, 236,
237 | r19.29af 3076 |
. . . . . . . . . . . 12
bits
|
239 | 238, 237 | jca 554 |
. . . . . . . . . . 11
bits bits |
240 | 239 | ex 450 |
. . . . . . . . . 10
bits
bits |
241 | 240 | reximdv2 3014 |
. . . . . . . . 9
bits
bits |
242 | 241 | imp 445 |
. . . . . . . 8
bits
bits |
243 | 242 | adantlr 751 |
. . . . . . 7
bits
bits |
244 | 185, 243 | sylan2b 492 |
. . . . . 6
bits
bits |
245 | 175, 244 | r19.29vva 3081 |
. . . . 5
bits
bits |
246 | 130, 245 | impbida 877 |
. . . 4
bits bits |
247 | 36, 246 | bitrd 268 |
. . 3
bits
bits |
248 | 247 | ifbid 4108 |
. 2
bits bits |
249 | 13, 23, 248 | 3eqtrd 2660 |
1
bits |