Step |
Hyp |
Ref |
Expression |
1 |
|
gsummptnn0fz.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
gsummptnn0fz.0 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
3 |
|
gsummptnn0fz.g |
⊢ ( 𝜑 → 𝐺 ∈ CMnd ) |
4 |
|
gsummptnn0fz.f |
⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 ) |
5 |
|
gsummptnn0fz.s |
⊢ ( 𝜑 → 𝑆 ∈ ℕ0 ) |
6 |
|
gsummptnn0fz.u |
⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐶 = 0 ) ) |
7 |
|
nfv |
⊢ Ⅎ 𝑥 ( 𝑆 < 𝑘 → 𝐶 = 0 ) |
8 |
|
nfv |
⊢ Ⅎ 𝑘 𝑆 < 𝑥 |
9 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ 𝐶 |
10 |
9
|
nfeq1 |
⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 |
11 |
8 10
|
nfim |
⊢ Ⅎ 𝑘 ( 𝑆 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) |
12 |
|
breq2 |
⊢ ( 𝑘 = 𝑥 → ( 𝑆 < 𝑘 ↔ 𝑆 < 𝑥 ) ) |
13 |
|
csbeq1a |
⊢ ( 𝑘 = 𝑥 → 𝐶 = ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) |
14 |
13
|
eqeq1d |
⊢ ( 𝑘 = 𝑥 → ( 𝐶 = 0 ↔ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) ) |
15 |
12 14
|
imbi12d |
⊢ ( 𝑘 = 𝑥 → ( ( 𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ( 𝑆 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) ) ) |
16 |
7 11 15
|
cbvralw |
⊢ ( ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) ) |
17 |
6 16
|
sylib |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) ) |
18 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 ) |
19 |
4
|
anim1ci |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 ) ) |
20 |
|
rspcsbela |
⊢ ( ( 𝑥 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) |
21 |
19 20
|
syl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) |
22 |
18 21
|
jca |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 ∈ ℕ0 ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) ) |
23 |
22
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) → ( 𝑥 ∈ ℕ0 ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) ) |
24 |
|
eqid |
⊢ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) = ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) |
25 |
24
|
fvmpts |
⊢ ( ( 𝑥 ∈ ℕ0 ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) |
26 |
23 25
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) |
27 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) |
28 |
26 27
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = 0 ) |
29 |
28
|
ex |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = 0 ) ) |
30 |
29
|
imim2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑆 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) → ( 𝑆 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = 0 ) ) ) |
31 |
30
|
ralimdva |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = 0 ) ) ) |
32 |
17 31
|
mpd |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = 0 ) ) |
33 |
24
|
fmpt |
⊢ ( ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 ↔ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) : ℕ0 ⟶ 𝐵 ) |
34 |
4 33
|
sylib |
⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) : ℕ0 ⟶ 𝐵 ) |
35 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
36 |
|
nn0ex |
⊢ ℕ0 ∈ V |
37 |
35 36
|
pm3.2i |
⊢ ( 𝐵 ∈ V ∧ ℕ0 ∈ V ) |
38 |
|
elmapg |
⊢ ( ( 𝐵 ∈ V ∧ ℕ0 ∈ V ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∈ ( 𝐵 ↑m ℕ0 ) ↔ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) : ℕ0 ⟶ 𝐵 ) ) |
39 |
37 38
|
mp1i |
⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∈ ( 𝐵 ↑m ℕ0 ) ↔ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) : ℕ0 ⟶ 𝐵 ) ) |
40 |
34 39
|
mpbird |
⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∈ ( 𝐵 ↑m ℕ0 ) ) |
41 |
|
fz0ssnn0 |
⊢ ( 0 ... 𝑆 ) ⊆ ℕ0 |
42 |
|
resmpt |
⊢ ( ( 0 ... 𝑆 ) ⊆ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ↾ ( 0 ... 𝑆 ) ) = ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ 𝐶 ) ) |
43 |
41 42
|
ax-mp |
⊢ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ↾ ( 0 ... 𝑆 ) ) = ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ 𝐶 ) |
44 |
43
|
eqcomi |
⊢ ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ 𝐶 ) = ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ↾ ( 0 ... 𝑆 ) ) |
45 |
1 2 3 40 5 44
|
fsfnn0gsumfsffz |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = 0 ) → ( 𝐺 Σg ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ 𝐶 ) ) ) ) |
46 |
32 45
|
mpd |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ 𝐶 ) ) ) |