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

Metamath Proof Explorer

Theorem sersub

Description: The difference of two infinite series. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses sersub.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
sersub.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
sersub.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
sersub.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) )
Assertion sersub ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 sersub.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 sersub.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
3 sersub.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
4 sersub.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) )
5 addcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
6 5 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
7 subcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 − 𝑦 ) ∈ ℂ )
8 7 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 − 𝑦 ) ∈ ℂ )
9 addsub4 ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ) → ( ( 𝑥 + 𝑦 ) − ( 𝑧 + 𝑤 ) ) = ( ( 𝑥 − 𝑧 ) + ( 𝑦 − 𝑤 ) ) )
10 9 eqcomd ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ) → ( ( 𝑥 − 𝑧 ) + ( 𝑦 − 𝑤 ) ) = ( ( 𝑥 + 𝑦 ) − ( 𝑧 + 𝑤 ) ) )
11 10 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ) ) → ( ( 𝑥 − 𝑧 ) + ( 𝑦 − 𝑤 ) ) = ( ( 𝑥 + 𝑦 ) − ( 𝑧 + 𝑤 ) ) )
12 6 8 11 1 2 3 4 seqcaopr2 ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )