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		climdm	$⊢ seq M (+ F) \in dom ⇝ \leftrightarrow seq M (+ F) ⇝ ⇝ (seq M (+ F))$
22	21	bilani	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq M (+ F) \in dom ⇝) \to seq M (+ F) ⇝ ⇝ (seq M (+ F))$
23	1 19 20 22	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))$
24	17 23	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))$
25		climrel	$⊢ Rel ⇝$
26	25	releldmi	$⊢ seq N (+ F) ⇝ (⇝ (seq M (+ F)) - seq M (+ F) (N - 1)) \to seq N (+ F) \in dom ⇝$
27	24 26	syl	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq M (+ F) \in dom ⇝) \to seq N (+ F) \in dom ⇝$
28		simpr	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to N - 1 \in ℤ_{\geq M}$
29	28 1	eleqtrrdi	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to N - 1 \in Z$
30	29	adantr	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to N - 1 \in Z$
31		simpll	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to φ$
32	31 3	sylan	$⊢ (((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \land k \in Z) \to F (k) \in ℂ$
33	31 16	syl	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to seq (N - 1 + 1) (+ F) = seq N (+ F)$
34		climdm	$⊢ seq N (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) ⇝ ⇝ (seq N (+ F))$
35	34	bilani	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to seq N (+ F) ⇝ ⇝ (seq N (+ F))$
36	33 35	eqbrtrd	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to seq (N - 1 + 1) (+ F) ⇝ ⇝ (seq N (+ F))$
37	1 30 32 36	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))$
38	25	releldmi	$⊢ seq M (+ F) ⇝ (⇝ (seq N (+ F)) + seq M (+ F) (N - 1)) \to seq M (+ F) \in dom ⇝$
39	37 38	syl	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land seq N (+ F) \in dom ⇝) \to seq M (+ F) \in dom ⇝$
40	27 39	impbida	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝)$
41	40	ex	$⊢ φ \to (N - 1 \in ℤ_{\geq M} \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝))$
42		uzm1	$⊢ N \in ℤ_{\geq M} \to (N = M \lor N - 1 \in ℤ_{\geq M})$
43	9 42	syl	$⊢ φ \to (N = M \lor N - 1 \in ℤ_{\geq M})$
44	7 41 43	mpjaod	$⊢ φ \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝)$

Metamath Proof Explorer

Theorem iserex

Proof