Step |
Hyp |
Ref |
Expression |
1 |
|
eulerpart.p |
⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) } |
2 |
|
eulerpart.o |
⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 } |
3 |
|
eulerpart.d |
⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 } |
4 |
|
eulerpart.j |
⊢ 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } |
5 |
|
eulerpart.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) |
6 |
|
eulerpart.h |
⊢ 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } |
7 |
|
eulerpart.m |
⊢ 𝑀 = ( 𝑟 ∈ 𝐻 ↦ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) |
8 |
|
eulerpart.r |
⊢ 𝑅 = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } |
9 |
|
eulerpart.t |
⊢ 𝑇 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 } |
10 |
|
eulerpart.g |
⊢ 𝐺 = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) |
11 |
1 2 3 4 5 6 7 8 9 10
|
eulerpartlemgv |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐺 ‘ 𝐴 ) = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ) ) |
12 |
11
|
cnveqd |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ◡ ( 𝐺 ‘ 𝐴 ) = ◡ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ) ) |
13 |
12
|
imaeq1d |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( 𝐺 ‘ 𝐴 ) “ { 1 } ) = ( ◡ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ) “ { 1 } ) ) |
14 |
|
nnex |
⊢ ℕ ∈ V |
15 |
|
imassrn |
⊢ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ⊆ ran 𝐹 |
16 |
4 5
|
oddpwdc |
⊢ 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ |
17 |
|
f1of |
⊢ ( 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ → 𝐹 : ( 𝐽 × ℕ0 ) ⟶ ℕ ) |
18 |
|
frn |
⊢ ( 𝐹 : ( 𝐽 × ℕ0 ) ⟶ ℕ → ran 𝐹 ⊆ ℕ ) |
19 |
16 17 18
|
mp2b |
⊢ ran 𝐹 ⊆ ℕ |
20 |
15 19
|
sstri |
⊢ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ⊆ ℕ |
21 |
|
indpi1 |
⊢ ( ( ℕ ∈ V ∧ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ⊆ ℕ ) → ( ◡ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ) “ { 1 } ) = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ) |
22 |
14 20 21
|
mp2an |
⊢ ( ◡ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ) “ { 1 } ) = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) |
23 |
13 22
|
eqtrdi |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( 𝐺 ‘ 𝐴 ) “ { 1 } ) = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ) |
24 |
|
ffun |
⊢ ( 𝐹 : ( 𝐽 × ℕ0 ) ⟶ ℕ → Fun 𝐹 ) |
25 |
16 17 24
|
mp2b |
⊢ Fun 𝐹 |
26 |
|
inss2 |
⊢ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ⊆ Fin |
27 |
1 2 3 4 5 6 7 8 9 10
|
eulerpartlemmf |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ 𝐻 ) |
28 |
1 2 3 4 5 6 7
|
eulerpartlem1 |
⊢ 𝑀 : 𝐻 –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) |
29 |
|
f1of |
⊢ ( 𝑀 : 𝐻 –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) → 𝑀 : 𝐻 ⟶ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ) |
30 |
28 29
|
ax-mp |
⊢ 𝑀 : 𝐻 ⟶ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) |
31 |
30
|
ffvelrni |
⊢ ( ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ∈ 𝐻 → ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ) |
32 |
27 31
|
syl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ) |
33 |
26 32
|
sselid |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ∈ Fin ) |
34 |
|
imafi |
⊢ ( ( Fun 𝐹 ∧ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ∈ Fin ) → ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ∈ Fin ) |
35 |
25 33 34
|
sylancr |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴 ↾ 𝐽 ) ) ) ) ∈ Fin ) |
36 |
23 35
|
eqeltrd |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( 𝐺 ‘ 𝐴 ) “ { 1 } ) ∈ Fin ) |
37 |
1 2 3 4 5 6 7 8 9 10
|
eulerpartgbij |
⊢ 𝐺 : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) |
38 |
|
f1of |
⊢ ( 𝐺 : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) → 𝐺 : ( 𝑇 ∩ 𝑅 ) ⟶ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ) |
39 |
37 38
|
ax-mp |
⊢ 𝐺 : ( 𝑇 ∩ 𝑅 ) ⟶ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) |
40 |
39
|
ffvelrni |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐺 ‘ 𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ) |
41 |
|
elin |
⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ↔ ( ( 𝐺 ‘ 𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) ∧ ( 𝐺 ‘ 𝐴 ) ∈ 𝑅 ) ) |
42 |
41
|
simplbi |
⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) → ( 𝐺 ‘ 𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) ) |
43 |
|
elmapi |
⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) → ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } ) |
44 |
40 42 43
|
3syl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } ) |
45 |
44
|
ffund |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Fun ( 𝐺 ‘ 𝐴 ) ) |
46 |
|
ssv |
⊢ ℕ0 ⊆ V |
47 |
|
dfn2 |
⊢ ℕ = ( ℕ0 ∖ { 0 } ) |
48 |
|
ssdif |
⊢ ( ℕ0 ⊆ V → ( ℕ0 ∖ { 0 } ) ⊆ ( V ∖ { 0 } ) ) |
49 |
47 48
|
eqsstrid |
⊢ ( ℕ0 ⊆ V → ℕ ⊆ ( V ∖ { 0 } ) ) |
50 |
46 49
|
ax-mp |
⊢ ℕ ⊆ ( V ∖ { 0 } ) |
51 |
|
sspreima |
⊢ ( ( Fun ( 𝐺 ‘ 𝐴 ) ∧ ℕ ⊆ ( V ∖ { 0 } ) ) → ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ⊆ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ( V ∖ { 0 } ) ) ) |
52 |
45 50 51
|
sylancl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ⊆ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ( V ∖ { 0 } ) ) ) |
53 |
|
fvex |
⊢ ( 𝐺 ‘ 𝐴 ) ∈ V |
54 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
55 |
|
suppimacnv |
⊢ ( ( ( 𝐺 ‘ 𝐴 ) ∈ V ∧ 0 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝐴 ) supp 0 ) = ( ◡ ( 𝐺 ‘ 𝐴 ) “ ( V ∖ { 0 } ) ) ) |
56 |
53 54 55
|
mp2an |
⊢ ( ( 𝐺 ‘ 𝐴 ) supp 0 ) = ( ◡ ( 𝐺 ‘ 𝐴 ) “ ( V ∖ { 0 } ) ) |
57 |
|
0ne1 |
⊢ 0 ≠ 1 |
58 |
|
difprsn1 |
⊢ ( 0 ≠ 1 → ( { 0 , 1 } ∖ { 0 } ) = { 1 } ) |
59 |
57 58
|
ax-mp |
⊢ ( { 0 , 1 } ∖ { 0 } ) = { 1 } |
60 |
59
|
eqcomi |
⊢ { 1 } = ( { 0 , 1 } ∖ { 0 } ) |
61 |
60
|
ffs2 |
⊢ ( ( ℕ ∈ V ∧ 0 ∈ ℕ0 ∧ ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } ) → ( ( 𝐺 ‘ 𝐴 ) supp 0 ) = ( ◡ ( 𝐺 ‘ 𝐴 ) “ { 1 } ) ) |
62 |
14 54 61
|
mp3an12 |
⊢ ( ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } → ( ( 𝐺 ‘ 𝐴 ) supp 0 ) = ( ◡ ( 𝐺 ‘ 𝐴 ) “ { 1 } ) ) |
63 |
44 62
|
syl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( 𝐺 ‘ 𝐴 ) supp 0 ) = ( ◡ ( 𝐺 ‘ 𝐴 ) “ { 1 } ) ) |
64 |
56 63
|
eqtr3id |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( 𝐺 ‘ 𝐴 ) “ ( V ∖ { 0 } ) ) = ( ◡ ( 𝐺 ‘ 𝐴 ) “ { 1 } ) ) |
65 |
52 64
|
sseqtrd |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ⊆ ( ◡ ( 𝐺 ‘ 𝐴 ) “ { 1 } ) ) |
66 |
|
ssfi |
⊢ ( ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ { 1 } ) ∈ Fin ∧ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ⊆ ( ◡ ( 𝐺 ‘ 𝐴 ) “ { 1 } ) ) → ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∈ Fin ) |
67 |
36 65 66
|
syl2anc |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∈ Fin ) |