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 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
22 climdm ⊢ ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑀 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
23 21 22 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑀 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
24 1 19 20 23 clim2ser ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) ⇝ ( ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) )
25 17 24 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑁 ( + , 𝐹 ) ⇝ ( ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) )
26 climrel ⊢ Rel ⇝
27 26 releldmi ⊢ ( seq 𝑁 ( + , 𝐹 ) ⇝ ( ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
28 25 27 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
29 simpr ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
30 29 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑁 − 1 ) ∈ 𝑍 )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → ( 𝑁 − 1 ) ∈ 𝑍 )
32 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → 𝜑 )
33 32 3 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
34 32 16 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) = seq 𝑁 ( + , 𝐹 ) )
35 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
36 climdm ⊢ ( seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( + , 𝐹 ) ) )
37 35 36 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑁 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( + , 𝐹 ) ) )
38 34 37 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( + , 𝐹 ) ) )
39 1 31 33 38 clim2ser2 ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑀 ( + , 𝐹 ) ⇝ ( ( ⇝ ‘ seq 𝑁 ( + , 𝐹 ) ) + ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) )
40 26 releldmi ⊢ ( seq 𝑀 ( + , 𝐹 ) ⇝ ( ( ⇝ ‘ seq 𝑁 ( + , 𝐹 ) ) + ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
41 39 40 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
42 28 41 impbida ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )
43 42 ex ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) ) )
44 uzm1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
45 9 44 syl ⊢ ( 𝜑 → ( 𝑁 = 𝑀 ∨ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
46 7 43 45 mpjaod ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )