Step |
Hyp |
Ref |
Expression |
1 |
|
eulerpartlems.r |
⊢ 𝑅 = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } |
2 |
|
eulerpartlems.s |
⊢ 𝑆 = ( 𝑓 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) ) |
3 |
|
simpl |
⊢ ( ( 𝑔 = 𝑓 ∧ 𝑘 ∈ ℕ ) → 𝑔 = 𝑓 ) |
4 |
3
|
fveq1d |
⊢ ( ( 𝑔 = 𝑓 ∧ 𝑘 ∈ ℕ ) → ( 𝑔 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) ) |
5 |
4
|
oveq1d |
⊢ ( ( 𝑔 = 𝑓 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) ) |
6 |
5
|
sumeq2dv |
⊢ ( 𝑔 = 𝑓 → Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) ) |
7 |
6
|
eleq1d |
⊢ ( 𝑔 = 𝑓 → ( Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 ↔ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 ) ) |
8 |
1 2
|
eulerpartlemsv2 |
⊢ ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝑔 ) = Σ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ) |
9 |
1 2
|
eulerpartlemsv1 |
⊢ ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝑔 ) = Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ) |
10 |
8 9
|
eqtr3d |
⊢ ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → Σ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ) |
11 |
1 2
|
eulerpartlemelr |
⊢ ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ) |
12 |
11
|
simprd |
⊢ ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( ◡ 𝑔 “ ℕ ) ∈ Fin ) |
13 |
11
|
simpld |
⊢ ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → 𝑔 : ℕ ⟶ ℕ0 ) |
14 |
13
|
adantr |
⊢ ( ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → 𝑔 : ℕ ⟶ ℕ0 ) |
15 |
|
cnvimass |
⊢ ( ◡ 𝑔 “ ℕ ) ⊆ dom 𝑔 |
16 |
15 13
|
fssdm |
⊢ ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( ◡ 𝑔 “ ℕ ) ⊆ ℕ ) |
17 |
16
|
sselda |
⊢ ( ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → 𝑘 ∈ ℕ ) |
18 |
14 17
|
ffvelrnd |
⊢ ( ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → ( 𝑔 ‘ 𝑘 ) ∈ ℕ0 ) |
19 |
17
|
nnnn0d |
⊢ ( ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → 𝑘 ∈ ℕ0 ) |
20 |
18 19
|
nn0mulcld |
⊢ ( ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 ) |
21 |
12 20
|
fsumnn0cl |
⊢ ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → Σ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 ) |
22 |
10 21
|
eqeltrrd |
⊢ ( 𝑔 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 ) |
23 |
7 22
|
vtoclga |
⊢ ( 𝑓 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 ) |
24 |
2 23
|
fmpti |
⊢ 𝑆 : ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ⟶ ℕ0 |