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 |
|
eulerpart.s |
⊢ 𝑆 = ( 𝑓 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) ) |
12 |
|
cnvimass |
⊢ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ⊆ dom ( 𝐺 ‘ 𝐴 ) |
13 |
1 2 3 4 5 6 7 8 9 10
|
eulerpartgbij |
⊢ 𝐺 : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) |
14 |
|
f1of |
⊢ ( 𝐺 : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) → 𝐺 : ( 𝑇 ∩ 𝑅 ) ⟶ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ) |
15 |
13 14
|
ax-mp |
⊢ 𝐺 : ( 𝑇 ∩ 𝑅 ) ⟶ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) |
16 |
15
|
ffvelrni |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐺 ‘ 𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ) |
17 |
|
elin |
⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ↔ ( ( 𝐺 ‘ 𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) ∧ ( 𝐺 ‘ 𝐴 ) ∈ 𝑅 ) ) |
18 |
16 17
|
sylib |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( 𝐺 ‘ 𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) ∧ ( 𝐺 ‘ 𝐴 ) ∈ 𝑅 ) ) |
19 |
18
|
simpld |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐺 ‘ 𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) ) |
20 |
|
elmapi |
⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) → ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } ) |
21 |
|
fdm |
⊢ ( ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } → dom ( 𝐺 ‘ 𝐴 ) = ℕ ) |
22 |
19 20 21
|
3syl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → dom ( 𝐺 ‘ 𝐴 ) = ℕ ) |
23 |
12 22
|
sseqtrid |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ⊆ ℕ ) |
24 |
23
|
sselda |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ) → 𝑘 ∈ ℕ ) |
25 |
1 2 3 4 5 6 7 8 9 10
|
eulerpartlemgvv |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) = if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) ) |
26 |
25
|
oveq1d |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) · 𝑘 ) = ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) ) |
27 |
24 26
|
syldan |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ) → ( ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) · 𝑘 ) = ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) ) |
28 |
27
|
sumeq2dv |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ( ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) ) |
29 |
|
eqeq2 |
⊢ ( 𝑚 = 𝑘 → ( ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 ↔ ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) ) |
30 |
29
|
2rexbidv |
⊢ ( 𝑚 = 𝑘 → ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 ↔ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) ) |
31 |
30
|
elrab |
⊢ ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ↔ ( 𝑘 ∈ ℕ ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) ) |
32 |
31
|
simprbi |
⊢ ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) |
33 |
32
|
iftrued |
⊢ ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) = 1 ) |
34 |
33
|
oveq1d |
⊢ ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = ( 1 · 𝑘 ) ) |
35 |
|
elrabi |
⊢ ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → 𝑘 ∈ ℕ ) |
36 |
35
|
nncnd |
⊢ ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → 𝑘 ∈ ℂ ) |
37 |
36
|
mulid2d |
⊢ ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → ( 1 · 𝑘 ) = 𝑘 ) |
38 |
34 37
|
eqtrd |
⊢ ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = 𝑘 ) |
39 |
38
|
sumeq2i |
⊢ Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } 𝑘 |
40 |
|
id |
⊢ ( 𝑘 = ( ( 2 ↑ ( 2nd ‘ 𝑤 ) ) · ( 1st ‘ 𝑤 ) ) → 𝑘 = ( ( 2 ↑ ( 2nd ‘ 𝑤 ) ) · ( 1st ‘ 𝑤 ) ) ) |
41 |
1 2 3 4 5 6 7 8 9 10
|
eulerpartlemgf |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∈ Fin ) |
42 |
35
|
adantl |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ℕ ) |
43 |
42 25
|
syldan |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) = if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) ) |
44 |
32
|
adantl |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) |
45 |
44
|
iftrued |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) = 1 ) |
46 |
43 45
|
eqtrd |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) = 1 ) |
47 |
|
1nn |
⊢ 1 ∈ ℕ |
48 |
46 47
|
eqeltrdi |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℕ ) |
49 |
19 20
|
syl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } ) |
50 |
|
ffn |
⊢ ( ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } → ( 𝐺 ‘ 𝐴 ) Fn ℕ ) |
51 |
|
elpreima |
⊢ ( ( 𝐺 ‘ 𝐴 ) Fn ℕ → ( 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℕ ) ) ) |
52 |
49 50 51
|
3syl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℕ ) ) ) |
53 |
52
|
adantr |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ( 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℕ ) ) ) |
54 |
42 48 53
|
mpbir2and |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ) |
55 |
54
|
ex |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ) ) |
56 |
55
|
ssrdv |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ⊆ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ) |
57 |
|
ssfi |
⊢ ( ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∈ Fin ∧ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ⊆ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ) → { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ∈ Fin ) |
58 |
41 56 57
|
syl2anc |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ∈ Fin ) |
59 |
|
cnvexg |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ◡ 𝐴 ∈ V ) |
60 |
|
imaexg |
⊢ ( ◡ 𝐴 ∈ V → ( ◡ 𝐴 “ ℕ ) ∈ V ) |
61 |
|
inex1g |
⊢ ( ( ◡ 𝐴 “ ℕ ) ∈ V → ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ V ) |
62 |
59 60 61
|
3syl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ V ) |
63 |
|
snex |
⊢ { 𝑡 } ∈ V |
64 |
|
fvex |
⊢ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∈ V |
65 |
63 64
|
xpex |
⊢ ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ∈ V |
66 |
65
|
rgenw |
⊢ ∀ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ∈ V |
67 |
|
iunexg |
⊢ ( ( ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ V ∧ ∀ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ∈ V ) → ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ∈ V ) |
68 |
62 66 67
|
sylancl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ∈ V ) |
69 |
|
eqid |
⊢ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) = ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) |
70 |
1 2 3 4 5 6 7 8 9 10 69
|
eulerpartlemgh |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐹 ↾ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) : ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) –1-1-onto→ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) |
71 |
|
f1oeng |
⊢ ( ( ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ∈ V ∧ ( 𝐹 ↾ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) : ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) –1-1-onto→ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ≈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) |
72 |
68 70 71
|
syl2anc |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ≈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) |
73 |
|
enfii |
⊢ ( ( { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ∈ Fin ∧ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ≈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ∈ Fin ) |
74 |
58 72 73
|
syl2anc |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ∈ Fin ) |
75 |
|
fvres |
⊢ ( 𝑤 ∈ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → ( ( 𝐹 ↾ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) ) |
76 |
75
|
adantl |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑤 ∈ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( ( 𝐹 ↾ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) ) |
77 |
|
inss2 |
⊢ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ 𝐽 |
78 |
|
simpr |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) |
79 |
77 78
|
sselid |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ 𝐽 ) |
80 |
79
|
snssd |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → { 𝑡 } ⊆ 𝐽 ) |
81 |
|
bitsss |
⊢ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ⊆ ℕ0 |
82 |
|
xpss12 |
⊢ ( ( { 𝑡 } ⊆ 𝐽 ∧ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ⊆ ℕ0 ) → ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) ) |
83 |
80 81 82
|
sylancl |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) ) |
84 |
83
|
ralrimiva |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ∀ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) ) |
85 |
|
iunss |
⊢ ( ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) ↔ ∀ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) ) |
86 |
84 85
|
sylibr |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) ) |
87 |
86
|
sselda |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑤 ∈ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → 𝑤 ∈ ( 𝐽 × ℕ0 ) ) |
88 |
4 5
|
oddpwdcv |
⊢ ( 𝑤 ∈ ( 𝐽 × ℕ0 ) → ( 𝐹 ‘ 𝑤 ) = ( ( 2 ↑ ( 2nd ‘ 𝑤 ) ) · ( 1st ‘ 𝑤 ) ) ) |
89 |
87 88
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑤 ∈ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( 𝐹 ‘ 𝑤 ) = ( ( 2 ↑ ( 2nd ‘ 𝑤 ) ) · ( 1st ‘ 𝑤 ) ) ) |
90 |
76 89
|
eqtrd |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑤 ∈ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( ( 𝐹 ↾ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) ‘ 𝑤 ) = ( ( 2 ↑ ( 2nd ‘ 𝑤 ) ) · ( 1st ‘ 𝑤 ) ) ) |
91 |
42
|
nncnd |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ℂ ) |
92 |
40 74 70 90 91
|
fsumf1o |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } 𝑘 = Σ 𝑤 ∈ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ( ( 2 ↑ ( 2nd ‘ 𝑤 ) ) · ( 1st ‘ 𝑤 ) ) ) |
93 |
39 92
|
syl5eq |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = Σ 𝑤 ∈ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ( ( 2 ↑ ( 2nd ‘ 𝑤 ) ) · ( 1st ‘ 𝑤 ) ) ) |
94 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
95 |
|
0cn |
⊢ 0 ∈ ℂ |
96 |
94 95
|
ifcli |
⊢ if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) ∈ ℂ |
97 |
96
|
a1i |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) ∈ ℂ ) |
98 |
|
ssrab2 |
⊢ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ⊆ ℕ |
99 |
|
simpr |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) |
100 |
98 99
|
sselid |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ℕ ) |
101 |
100
|
nncnd |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ℂ ) |
102 |
97 101
|
mulcld |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) ∈ ℂ ) |
103 |
|
simpr |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → 𝑘 ∈ ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) |
104 |
103
|
eldifbd |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ¬ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) |
105 |
23
|
ssdifssd |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ⊆ ℕ ) |
106 |
105
|
sselda |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → 𝑘 ∈ ℕ ) |
107 |
31
|
notbii |
⊢ ( ¬ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ↔ ¬ ( 𝑘 ∈ ℕ ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) ) |
108 |
|
imnan |
⊢ ( ( 𝑘 ∈ ℕ → ¬ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) ↔ ¬ ( 𝑘 ∈ ℕ ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) ) |
109 |
107 108
|
sylbb2 |
⊢ ( ¬ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → ( 𝑘 ∈ ℕ → ¬ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) ) |
110 |
104 106 109
|
sylc |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ¬ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) |
111 |
110
|
iffalsed |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) = 0 ) |
112 |
111
|
oveq1d |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = ( 0 · 𝑘 ) ) |
113 |
|
nnsscn |
⊢ ℕ ⊆ ℂ |
114 |
105 113
|
sstrdi |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ⊆ ℂ ) |
115 |
114
|
sselda |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → 𝑘 ∈ ℂ ) |
116 |
115
|
mul02d |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ( 0 · 𝑘 ) = 0 ) |
117 |
112 116
|
eqtrd |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑘 ∈ ( ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = 0 ) |
118 |
56 102 117 41
|
fsumss |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = Σ 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) ) |
119 |
93 118
|
eqtr3d |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑤 ∈ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ( ( 2 ↑ ( 2nd ‘ 𝑤 ) ) · ( 1st ‘ 𝑤 ) ) = Σ 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) ) |
120 |
1 2 3 4 5 6 7 8 9
|
eulerpartlemt0 |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ) ) |
121 |
120
|
simp1bi |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 ∈ ( ℕ0 ↑m ℕ ) ) |
122 |
|
elmapi |
⊢ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) → 𝐴 : ℕ ⟶ ℕ0 ) |
123 |
121 122
|
syl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 : ℕ ⟶ ℕ0 ) |
124 |
123
|
adantr |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝐴 : ℕ ⟶ ℕ0 ) |
125 |
|
cnvimass |
⊢ ( ◡ 𝐴 “ ℕ ) ⊆ dom 𝐴 |
126 |
125 123
|
fssdm |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ 𝐴 “ ℕ ) ⊆ ℕ ) |
127 |
126
|
adantr |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( ◡ 𝐴 “ ℕ ) ⊆ ℕ ) |
128 |
|
inss1 |
⊢ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ ( ◡ 𝐴 “ ℕ ) |
129 |
128 78
|
sselid |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) |
130 |
127 129
|
sseldd |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ ℕ ) |
131 |
124 130
|
ffvelrnd |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 ) |
132 |
|
bitsfi |
⊢ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 → ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∈ Fin ) |
133 |
131 132
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ∈ Fin ) |
134 |
130
|
nncnd |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ ℂ ) |
135 |
|
2cnd |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → 2 ∈ ℂ ) |
136 |
|
simprr |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) |
137 |
81 136
|
sselid |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → 𝑛 ∈ ℕ0 ) |
138 |
135 137
|
expcld |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( 2 ↑ 𝑛 ) ∈ ℂ ) |
139 |
138
|
anassrs |
⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) → ( 2 ↑ 𝑛 ) ∈ ℂ ) |
140 |
133 134 139
|
fsummulc1 |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = Σ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) ) |
141 |
140
|
sumeq2dv |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = Σ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) Σ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) ) |
142 |
|
bitsinv1 |
⊢ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 → Σ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( 2 ↑ 𝑛 ) = ( 𝐴 ‘ 𝑡 ) ) |
143 |
142
|
oveq1d |
⊢ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 → ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ) |
144 |
131 143
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ) |
145 |
144
|
sumeq2dv |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = Σ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ) |
146 |
|
vex |
⊢ 𝑡 ∈ V |
147 |
|
vex |
⊢ 𝑛 ∈ V |
148 |
146 147
|
op2ndd |
⊢ ( 𝑤 = 〈 𝑡 , 𝑛 〉 → ( 2nd ‘ 𝑤 ) = 𝑛 ) |
149 |
148
|
oveq2d |
⊢ ( 𝑤 = 〈 𝑡 , 𝑛 〉 → ( 2 ↑ ( 2nd ‘ 𝑤 ) ) = ( 2 ↑ 𝑛 ) ) |
150 |
146 147
|
op1std |
⊢ ( 𝑤 = 〈 𝑡 , 𝑛 〉 → ( 1st ‘ 𝑤 ) = 𝑡 ) |
151 |
149 150
|
oveq12d |
⊢ ( 𝑤 = 〈 𝑡 , 𝑛 〉 → ( ( 2 ↑ ( 2nd ‘ 𝑤 ) ) · ( 1st ‘ 𝑤 ) ) = ( ( 2 ↑ 𝑛 ) · 𝑡 ) ) |
152 |
|
inss2 |
⊢ ( 𝑇 ∩ 𝑅 ) ⊆ 𝑅 |
153 |
152
|
sseli |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 ∈ 𝑅 ) |
154 |
|
cnveq |
⊢ ( 𝑓 = 𝐴 → ◡ 𝑓 = ◡ 𝐴 ) |
155 |
154
|
imaeq1d |
⊢ ( 𝑓 = 𝐴 → ( ◡ 𝑓 “ ℕ ) = ( ◡ 𝐴 “ ℕ ) ) |
156 |
155
|
eleq1d |
⊢ ( 𝑓 = 𝐴 → ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ↔ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) ) |
157 |
156 8
|
elab2g |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐴 ∈ 𝑅 ↔ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) ) |
158 |
153 157
|
mpbid |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ 𝐴 “ ℕ ) ∈ Fin ) |
159 |
|
ssfi |
⊢ ( ( ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ ( ◡ 𝐴 “ ℕ ) ) → ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ Fin ) |
160 |
158 128 159
|
sylancl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ Fin ) |
161 |
134
|
adantrr |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → 𝑡 ∈ ℂ ) |
162 |
138 161
|
mulcld |
⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ) → ( ( 2 ↑ 𝑛 ) · 𝑡 ) ∈ ℂ ) |
163 |
151 160 133 162
|
fsum2d |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) Σ 𝑛 ∈ ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = Σ 𝑤 ∈ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ( ( 2 ↑ ( 2nd ‘ 𝑤 ) ) · ( 1st ‘ 𝑤 ) ) ) |
164 |
141 145 163
|
3eqtr3d |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) = Σ 𝑤 ∈ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ( ( 2 ↑ ( 2nd ‘ 𝑤 ) ) · ( 1st ‘ 𝑤 ) ) ) |
165 |
|
inss1 |
⊢ ( 𝑇 ∩ 𝑅 ) ⊆ 𝑇 |
166 |
165
|
sseli |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 ∈ 𝑇 ) |
167 |
155
|
sseq1d |
⊢ ( 𝑓 = 𝐴 → ( ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 ↔ ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ) ) |
168 |
167 9
|
elrab2 |
⊢ ( 𝐴 ∈ 𝑇 ↔ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ) ) |
169 |
168
|
simprbi |
⊢ ( 𝐴 ∈ 𝑇 → ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ) |
170 |
166 169
|
syl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ) |
171 |
|
df-ss |
⊢ ( ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ↔ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) = ( ◡ 𝐴 “ ℕ ) ) |
172 |
170 171
|
sylib |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) = ( ◡ 𝐴 “ ℕ ) ) |
173 |
172
|
sumeq1d |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) = Σ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ) |
174 |
164 173
|
eqtr3d |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑤 ∈ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) ( ( 2 ↑ ( 2nd ‘ 𝑤 ) ) · ( 1st ‘ 𝑤 ) ) = Σ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ) |
175 |
28 119 174
|
3eqtr2d |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ( ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) · 𝑘 ) = Σ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ) |
176 |
|
fveq2 |
⊢ ( 𝑘 = 𝑡 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑡 ) ) |
177 |
|
id |
⊢ ( 𝑘 = 𝑡 → 𝑘 = 𝑡 ) |
178 |
176 177
|
oveq12d |
⊢ ( 𝑘 = 𝑡 → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) ) |
179 |
178
|
cbvsumv |
⊢ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑡 ) · 𝑡 ) |
180 |
175 179
|
eqtr4di |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ( ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) ) |
181 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
182 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
183 |
|
prssi |
⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → { 0 , 1 } ⊆ ℕ0 ) |
184 |
181 182 183
|
mp2an |
⊢ { 0 , 1 } ⊆ ℕ0 |
185 |
|
fss |
⊢ ( ( ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } ∧ { 0 , 1 } ⊆ ℕ0 ) → ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ ℕ0 ) |
186 |
184 185
|
mpan2 |
⊢ ( ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } → ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ ℕ0 ) |
187 |
|
nn0ex |
⊢ ℕ0 ∈ V |
188 |
|
nnex |
⊢ ℕ ∈ V |
189 |
187 188
|
elmap |
⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ℕ0 ↑m ℕ ) ↔ ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ ℕ0 ) |
190 |
189
|
biimpri |
⊢ ( ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ ℕ0 → ( 𝐺 ‘ 𝐴 ) ∈ ( ℕ0 ↑m ℕ ) ) |
191 |
20 186 190
|
3syl |
⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) → ( 𝐺 ‘ 𝐴 ) ∈ ( ℕ0 ↑m ℕ ) ) |
192 |
191
|
anim1i |
⊢ ( ( ( 𝐺 ‘ 𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) ∧ ( 𝐺 ‘ 𝐴 ) ∈ 𝑅 ) → ( ( 𝐺 ‘ 𝐴 ) ∈ ( ℕ0 ↑m ℕ ) ∧ ( 𝐺 ‘ 𝐴 ) ∈ 𝑅 ) ) |
193 |
|
elin |
⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ↔ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ℕ0 ↑m ℕ ) ∧ ( 𝐺 ‘ 𝐴 ) ∈ 𝑅 ) ) |
194 |
192 17 193
|
3imtr4i |
⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) → ( 𝐺 ‘ 𝐴 ) ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ) |
195 |
8 11
|
eulerpartlemsv2 |
⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺 ‘ 𝐴 ) ) = Σ 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ( ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) · 𝑘 ) ) |
196 |
16 194 195
|
3syl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺 ‘ 𝐴 ) ) = Σ 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ( ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) · 𝑘 ) ) |
197 |
121 153
|
elind |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ) |
198 |
8 11
|
eulerpartlemsv2 |
⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) ) |
199 |
197 198
|
syl |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) ) |
200 |
180 196 199
|
3eqtr4d |
⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺 ‘ 𝐴 ) ) = ( 𝑆 ‘ 𝐴 ) ) |