clim2ser2

Description: The limit of an infinite series with an initial segment added. (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 ℂ$
	clim2ser2.5	$⊢ φ \to seq (N + 1) (+ F) ⇝ A$
Assertion	clim2ser2	$⊢ φ \to seq M (+ 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		clim2ser2.5	$⊢ φ \to seq (N + 1) (+ 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 M (+ F) \in V$
16	15	a1i	$⊢ φ \to seq M (+ F) \in V$
17	8 1	eleqtrrdi	$⊢ φ \to N + 1 \in Z$
18	1	uztrn2	$⊢ (N + 1 \in Z \land k \in ℤ_{\geq (N + 1)}) \to k \in Z$
19	17 18	sylan	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to k \in Z$
20	19 3	syldan	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to F (k) \in ℂ$
21	5 10 20	serf	$⊢ φ \to seq (N + 1) (+ F) : ℤ_{\geq (N + 1)} ⟶ ℂ$
22	21	ffvelcdmda	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq (N + 1) (+ F) (j) \in ℂ$
23	14	adantr	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (+ F) (N) \in ℂ$
24		addcl	$⊢ (k \in ℂ \land x \in ℂ) \to k + x \in ℂ$
25	24	adantl	$⊢ ((φ \land j \in ℤ_{\geq (N + 1)}) \land (k \in ℂ \land x \in ℂ)) \to k + x \in ℂ$
26		addass	$⊢ (k \in ℂ \land x \in ℂ \land y \in ℂ) \to k + x + y = k + x + y$
27	26	adantl	$⊢ ((φ \land j \in ℤ_{\geq (N + 1)}) \land (k \in ℂ \land x \in ℂ \land y \in ℂ)) \to k + x + y = k + x + y$
28		simpr	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to j \in ℤ_{\geq (N + 1)}$
29	6	adantr	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to N \in ℤ_{\geq M}$
30		elfzuz	$⊢ k \in (M \dots j) \to k \in ℤ_{\geq M}$
31	30 1	eleqtrrdi	$⊢ k \in (M \dots j) \to k \in Z$
32	31 3	sylan2	$⊢ (φ \land k \in (M \dots j)) \to F (k) \in ℂ$
33	32	adantlr	$⊢ ((φ \land j \in ℤ_{\geq (N + 1)}) \land k \in (M \dots j)) \to F (k) \in ℂ$
34	25 27 28 29 33	seqsplit	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (+ F) (j) = seq M (+ F) (N) + seq (N + 1) (+ F) (j)$
35	23 22 34	comraddd	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (+ F) (j) = seq (N + 1) (+ F) (j) + seq M (+ F) (N)$
36	5 10 4 14 16 22 35	climaddc1	$⊢ φ \to seq M (+ F) ⇝ (A + seq M (+ F) (N))$

Metamath Proof Explorer

Theorem clim2ser2

Proof