This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem telgsum

Description: Telescoping finitely supported group sum ranging over nonnegative integers, using implicit substitution. (Contributed by AV, 31-Dec-2019)

Ref Expression
Hypotheses telgsum.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
telgsum.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
telgsum.m ⊢ − = ( -g ‘ 𝐺 )
telgsum.0 ⊢ 0 = ( 0g ‘ 𝐺 )
telgsum.f ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐵 )
telgsum.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
telgsum.u ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐴 = 0 ) )
telgsum.c ⊢ ( 𝑘 = 𝑖 → 𝐴 = 𝐶 )
telgsum.d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → 𝐴 = 𝐷 )
telgsum.e ⊢ ( 𝑘 = 0 → 𝐴 = 𝐸 )
Assertion telgsum ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ℕ0 ↦ ( 𝐶 − 𝐷 ) ) ) = 𝐸 )

Proof

Step Hyp Ref Expression
1 telgsum.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 telgsum.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
3 telgsum.m ⊢ − = ( -g ‘ 𝐺 )
4 telgsum.0 ⊢ 0 = ( 0g ‘ 𝐺 )
5 telgsum.f ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐵 )
6 telgsum.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
7 telgsum.u ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → 𝐴 = 0 ) )
8 telgsum.c ⊢ ( 𝑘 = 𝑖 → 𝐴 = 𝐶 )
9 telgsum.d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → 𝐴 = 𝐷 )
10 telgsum.e ⊢ ( 𝑘 = 0 → 𝐴 = 𝐸 )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
12 8 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 = 𝑖 ) → 𝐴 = 𝐶 )
13 11 12 csbied ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐴 = 𝐶 )
14 13 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐶 = ⦋ 𝑖 / 𝑘 ⦌ 𝐴 )
15 peano2nn0 ⊢ ( 𝑖 ∈ ℕ0 → ( 𝑖 + 1 ) ∈ ℕ0 )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 + 1 ) ∈ ℕ0 )
17 9 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 = ( 𝑖 + 1 ) ) → 𝐴 = 𝐷 )
18 16 17 csbied ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 = 𝐷 )
19 18 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐷 = ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 )
20 14 19 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝐶 − 𝐷 ) = ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) )
21 20 mpteq2dva ⊢ ( 𝜑 → ( 𝑖 ∈ ℕ0 ↦ ( 𝐶 − 𝐷 ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) ) )
22 21 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ℕ0 ↦ ( 𝐶 − 𝐷 ) ) ) = ( 𝐺 Σg ( 𝑖 ∈ ℕ0 ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) ) ) )
23 1 2 3 4 5 6 7 telgsums ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ℕ0 ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐴 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐴 ) ) ) = ⦋ 0 / 𝑘 ⦌ 𝐴 )
24 c0ex ⊢ 0 ∈ V
25 24 a1i ⊢ ( 𝜑 → 0 ∈ V )
26 10 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → 𝐴 = 𝐸 )
27 25 26 csbied ⊢ ( 𝜑 → ⦋ 0 / 𝑘 ⦌ 𝐴 = 𝐸 )
28 22 23 27 3eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ℕ0 ↦ ( 𝐶 − 𝐷 ) ) ) = 𝐸 )