Metamath Proof Explorer

Theorem iserex

Description: An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 27-Apr-2014)

Ref Expression
Hypotheses clim2ser.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
iserex.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
iserex.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
Assertion iserex ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )

Proof

Step Hyp Ref Expression
1 clim2ser.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 iserex.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3 iserex.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
4 seqeq1 ⊢ ( 𝑁 = 𝑀 → seq 𝑁 ( + , 𝐹 ) = seq 𝑀 ( + , 𝐹 ) )
5 4 eleq1d ⊢ ( 𝑁 = 𝑀 → ( seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) )
6 5 bicomd ⊢ ( 𝑁 = 𝑀 → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )
7 6 a1i ⊢ ( 𝜑 → ( 𝑁 = 𝑀 → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) ) )
8 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → 𝜑 )
9 2 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
10 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
11 9 10 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
12 11 zcnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
13 ax-1cn ⊢ 1 ∈ ℂ
14 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
15 12 13 14 sylancl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
16 15 seqeq1d ⊢ ( 𝜑 → seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) = seq 𝑁 ( + , 𝐹 ) )
17 8 16 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) = seq 𝑁 ( + , 𝐹 ) )
18 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
19 18 1 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → ( 𝑁 − 1 ) ∈ 𝑍 )
20 8 3 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
21 climdm ⊢ ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑀 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
22 21 bilani ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑀 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
23 1 19 20 22 clim2ser ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) ⇝ ( ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) )
24 17 23 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑁 ( + , 𝐹 ) ⇝ ( ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) )
25 climrel ⊢ Rel ⇝
26 25 releldmi ⊢ ( seq 𝑁 ( + , 𝐹 ) ⇝ ( ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
27 24 26 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
28 simpr ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
29 28 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑁 − 1 ) ∈ 𝑍 )
30 29 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → ( 𝑁 − 1 ) ∈ 𝑍 )
31 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → 𝜑 )
32 31 3 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
33 31 16 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) = seq 𝑁 ( + , 𝐹 ) )
34 climdm ⊢ ( seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( + , 𝐹 ) ) )
35 34 bilani ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑁 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( + , 𝐹 ) ) )
36 33 35 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( + , 𝐹 ) ) )
37 1 30 32 36 clim2ser2 ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑀 ( + , 𝐹 ) ⇝ ( ( ⇝ ‘ seq 𝑁 ( + , 𝐹 ) ) + ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) )
38 25 releldmi ⊢ ( seq 𝑀 ( + , 𝐹 ) ⇝ ( ( ⇝ ‘ seq 𝑁 ( + , 𝐹 ) ) + ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
39 37 38 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
40 27 39 impbida ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )
41 40 ex ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) ) )
42 uzm1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
43 9 42 syl ⊢ ( 𝜑 → ( 𝑁 = 𝑀 ∨ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
44 7 41 43 mpjaod ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )