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	$⊢ Z = ℤ_{\geq M}$
	iserex.2	$⊢ φ \to N \in Z$
	iserex.3	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
Assertion	iserex	$⊢ φ \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝)$

Proof

Step	Hyp	Ref	Expression
1		clim2ser.1	$⊢ Z = ℤ_{\geq M}$
2		iserex.2	$⊢ φ \to N \in Z$
3		iserex.3	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
4		seqeq1	$⊢ N = M \to seq N (+ F) = seq M (+ F)$
5	4	eleq1d	$⊢ N = M \to (seq N (+ F) \in dom ⇝ \leftrightarrow seq M (+ F) \in dom ⇝)$
6	5	bicomd	$⊢ N = M \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝)$
7	6	a1i	$⊢ φ \to (N = M \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝))$
8		simpll	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq M (+ F) \in dom ⇝) \to φ$
9	2 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
10		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
11	9 10	syl	$⊢ φ \to N \in ℤ$
12	11	zcnd	$⊢ φ \to N \in ℂ$
13		ax-1cn	$⊢ 1 \in ℂ$
14		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
15	12 13 14	sylancl	$⊢ φ \to N - 1 + 1 = N$
16	15	seqeq1d	$⊢ φ \to seq (N - 1 + 1) (+ F) = seq N (+ F)$
17	8 16	syl	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq M (+ F) \in dom ⇝) \to seq (N - 1 + 1) (+ F) = seq N (+ F)$
18		simplr	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq M (+ F) \in dom ⇝) \to N - 1 \in ℤ_{\geq M}$
19	18 1	eleqtrrdi	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq M (+ F) \in dom ⇝) \to N - 1 \in Z$
20	8 3	sylan	$⊢ (((φ \land N - 1 \in ℤ_{\geq M}) \land seq M (+ F) \in dom ⇝) \land k \in Z) \to F (k) \in ℂ$
21		simpr	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq M (+ F) \in dom ⇝) \to seq M (+ F) \in dom ⇝$
22		climdm	$⊢ seq M (+ F) \in dom ⇝ \leftrightarrow seq M (+ F) ⇝ ⇝ (seq M (+ F))$
23	21 22	sylib	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq M (+ F) \in dom ⇝) \to seq M (+ F) ⇝ ⇝ (seq M (+ F))$
24	1 19 20 23	clim2ser	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq M (+ F) \in dom ⇝) \to seq (N - 1 + 1) (+ F) ⇝ (⇝ (seq M (+ F)) - seq M (+ F) (N - 1))$
25	17 24	eqbrtrrd	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq M (+ F) \in dom ⇝) \to seq N (+ F) ⇝ (⇝ (seq M (+ F)) - seq M (+ F) (N - 1))$
26		climrel	$⊢ Rel ⇝$
27	26	releldmi	$⊢ seq N (+ F) ⇝ (⇝ (seq M (+ F)) - seq M (+ F) (N - 1)) \to seq N (+ F) \in dom ⇝$
28	25 27	syl	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq M (+ F) \in dom ⇝) \to seq N (+ F) \in dom ⇝$
29		simpr	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to N - 1 \in ℤ_{\geq M}$
30	29 1	eleqtrrdi	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to N - 1 \in Z$
31	30	adantr	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to N - 1 \in Z$
32		simpll	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to φ$
33	32 3	sylan	$⊢ (((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \land k \in Z) \to F (k) \in ℂ$
34	32 16	syl	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to seq (N - 1 + 1) (+ F) = seq N (+ F)$
35		simpr	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to seq N (+ F) \in dom ⇝$
36		climdm	$⊢ seq N (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) ⇝ ⇝ (seq N (+ F))$
37	35 36	sylib	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to seq N (+ F) ⇝ ⇝ (seq N (+ F))$
38	34 37	eqbrtrd	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to seq (N - 1 + 1) (+ F) ⇝ ⇝ (seq N (+ F))$
39	1 31 33 38	clim2ser2	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to seq M (+ F) ⇝ (⇝ (seq N (+ F)) + seq M (+ F) (N - 1))$
40	26	releldmi	$⊢ seq M (+ F) ⇝ (⇝ (seq N (+ F)) + seq M (+ F) (N - 1)) \to seq M (+ F) \in dom ⇝$
41	39 40	syl	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to seq M (+ F) \in dom ⇝$
42	28 41	impbida	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝)$
43	42	ex	$⊢ φ \to (N - 1 \in ℤ_{\geq M} \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝))$
44		uzm1	$⊢ N \in ℤ_{\geq M} \to (N = M \lor N - 1 \in ℤ_{\geq M})$
45	9 44	syl	$⊢ φ \to (N = M \lor N - 1 \in ℤ_{\geq M})$
46	7 43 45	mpjaod	$⊢ φ \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝)$

Metamath Proof Explorer

Theorem iserex

Proof