clim2ser

Description: The limit of an infinite series with an initial segment removed. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 1-Feb-2014)

	Ref	Expression
Hypotheses	clim2ser.1	$⊢ Z = ℤ_{\geq M}$
	clim2ser.2	$⊢ φ \to N \in Z$
	clim2ser.4	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
	clim2ser.5	$⊢ φ \to seq M (+ F) ⇝ A$
Assertion	clim2ser	$⊢ φ \to seq (N + 1) (+ F) ⇝ (A - seq M (+ F) (N))$

Proof

Step	Hyp	Ref	Expression
1		clim2ser.1	$⊢ Z = ℤ_{\geq M}$
2		clim2ser.2	$⊢ φ \to N \in Z$
3		clim2ser.4	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
4		clim2ser.5	$⊢ φ \to seq M (+ F) ⇝ A$
5		eqid	$⊢ ℤ_{\geq (N + 1)} = ℤ_{\geq (N + 1)}$
6	2 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
7		peano2uz	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq M}$
8	6 7	syl	$⊢ φ \to N + 1 \in ℤ_{\geq M}$
9		eluzelz	$⊢ N + 1 \in ℤ_{\geq M} \to N + 1 \in ℤ$
10	8 9	syl	$⊢ φ \to N + 1 \in ℤ$
11		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
12	6 11	syl	$⊢ φ \to M \in ℤ$
13	1 12 3	serf	$⊢ φ \to seq M (+ F) : Z ⟶ ℂ$
14	13 2	ffvelcdmd	$⊢ φ \to seq M (+ F) (N) \in ℂ$
15		seqex	$⊢ seq (N + 1) (+ F) \in V$
16	15	a1i	$⊢ φ \to seq (N + 1) (+ F) \in V$
17	13	adantr	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (+ F) : Z ⟶ ℂ$
18	8 1	eleqtrrdi	$⊢ φ \to N + 1 \in Z$
19	1	uztrn2	$⊢ (N + 1 \in Z \land j \in ℤ_{\geq (N + 1)}) \to j \in Z$
20	18 19	sylan	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to j \in Z$
21	17 20	ffvelcdmd	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (+ F) (j) \in ℂ$
22		addcl	$⊢ (k \in ℂ \land x \in ℂ) \to k + x \in ℂ$
23	22	adantl	$⊢ ((φ \land j \in ℤ_{\geq (N + 1)}) \land (k \in ℂ \land x \in ℂ)) \to k + x \in ℂ$
24		addass	$⊢ (k \in ℂ \land x \in ℂ \land y \in ℂ) \to k + x + y = k + x + y$
25	24	adantl	$⊢ ((φ \land j \in ℤ_{\geq (N + 1)}) \land (k \in ℂ \land x \in ℂ \land y \in ℂ)) \to k + x + y = k + x + y$
26		simpr	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to j \in ℤ_{\geq (N + 1)}$
27	6	adantr	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to N \in ℤ_{\geq M}$
28		elfzuz	$⊢ k \in (M \dots j) \to k \in ℤ_{\geq M}$
29	28 1	eleqtrrdi	$⊢ k \in (M \dots j) \to k \in Z$
30	29 3	sylan2	$⊢ (φ \land k \in (M \dots j)) \to F (k) \in ℂ$
31	30	adantlr	$⊢ ((φ \land j \in ℤ_{\geq (N + 1)}) \land k \in (M \dots j)) \to F (k) \in ℂ$
32	23 25 26 27 31	seqsplit	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (+ F) (j) = seq M (+ F) (N) + seq (N + 1) (+ F) (j)$
33	32	oveq1d	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (+ F) (j) - seq M (+ F) (N) = seq M (+ F) (N) + seq (N + 1) (+ F) (j) - seq M (+ F) (N)$
34	14	adantr	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (+ F) (N) \in ℂ$
35	1	uztrn2	$⊢ (N + 1 \in Z \land k \in ℤ_{\geq (N + 1)}) \to k \in Z$
36	18 35	sylan	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to k \in Z$
37	36 3	syldan	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to F (k) \in ℂ$
38	5 10 37	serf	$⊢ φ \to seq (N + 1) (+ F) : ℤ_{\geq (N + 1)} ⟶ ℂ$
39	38	ffvelcdmda	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq (N + 1) (+ F) (j) \in ℂ$
40	34 39	pncan2d	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (+ F) (N) + seq (N + 1) (+ F) (j) - seq M (+ F) (N) = seq (N + 1) (+ F) (j)$
41	33 40	eqtr2d	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq (N + 1) (+ F) (j) = seq M (+ F) (j) - seq M (+ F) (N)$
42	5 10 4 14 16 21 41	climsubc1	$⊢ φ \to seq (N + 1) (+ F) ⇝ (A - seq M (+ F) (N))$

Metamath Proof Explorer

Theorem clim2ser

Proof