fsumcvg3

Description: A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	fsumcvg3.1	$⊢ Z = ℤ_{\geq M}$
	fsumcvg3.2	$⊢ φ \to M \in ℤ$
	fsumcvg3.3	$⊢ φ \to A \in Fin$
	fsumcvg3.4	$⊢ φ \to A \subseteq Z$
	fsumcvg3.5	$⊢ (φ \land k \in Z) \to F (k) = if (k \in A, B, 0)$
	fsumcvg3.6	$⊢ (φ \land k \in A) \to B \in ℂ$
Assertion	fsumcvg3	$⊢ φ \to seq M (+ F) \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		fsumcvg3.1	$⊢ Z = ℤ_{\geq M}$
2		fsumcvg3.2	$⊢ φ \to M \in ℤ$
3		fsumcvg3.3	$⊢ φ \to A \in Fin$
4		fsumcvg3.4	$⊢ φ \to A \subseteq Z$
5		fsumcvg3.5	$⊢ (φ \land k \in Z) \to F (k) = if (k \in A, B, 0)$
6		fsumcvg3.6	$⊢ (φ \land k \in A) \to B \in ℂ$
7		sseq1	$⊢ A = \emptyset \to (A \subseteq (M \dots n) \leftrightarrow \emptyset \subseteq (M \dots n))$
8	7	rexbidv	$⊢ A = \emptyset \to (\exists n \in ℤ_{\geq M} A \subseteq (M \dots n) \leftrightarrow \exists n \in ℤ_{\geq M} \emptyset \subseteq (M \dots n))$
9	4	adantr	$⊢ (φ \land A \neq \emptyset) \to A \subseteq Z$
10	9 1	sseqtrdi	$⊢ (φ \land A \neq \emptyset) \to A \subseteq ℤ_{\geq M}$
11		ltso	$⊢ < Or ℝ$
12	3	adantr	$⊢ (φ \land A \neq \emptyset) \to A \in Fin$
13		simpr	$⊢ (φ \land A \neq \emptyset) \to A \neq \emptyset$
14		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
15		zssre	$⊢ ℤ \subseteq ℝ$
16	14 15	sstri	$⊢ ℤ_{\geq M} \subseteq ℝ$
17	1 16	eqsstri	$⊢ Z \subseteq ℝ$
18	9 17	sstrdi	$⊢ (φ \land A \neq \emptyset) \to A \subseteq ℝ$
19	12 13 18	3jca	$⊢ (φ \land A \neq \emptyset) \to (A \in Fin \land A \neq \emptyset \land A \subseteq ℝ)$
20		fisupcl	$⊢ (< Or ℝ \land (A \in Fin \land A \neq \emptyset \land A \subseteq ℝ)) \to sup (A ℝ <) \in A$
21	11 19 20	sylancr	$⊢ (φ \land A \neq \emptyset) \to sup (A ℝ <) \in A$
22	10 21	sseldd	$⊢ (φ \land A \neq \emptyset) \to sup (A ℝ <) \in ℤ_{\geq M}$
23		fimaxre2	$⊢ (A \subseteq ℝ \land A \in Fin) \to \exists k \in ℝ \forall n \in A n \leq k$
24	18 12 23	syl2anc	$⊢ (φ \land A \neq \emptyset) \to \exists k \in ℝ \forall n \in A n \leq k$
25	18 13 24	3jca	$⊢ (φ \land A \neq \emptyset) \to (A \subseteq ℝ \land A \neq \emptyset \land \exists k \in ℝ \forall n \in A n \leq k)$
26		suprub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists k \in ℝ \forall n \in A n \leq k) \land k \in A) \to k \leq sup (A ℝ <)$
27	25 26	sylan	$⊢ ((φ \land A \neq \emptyset) \land k \in A) \to k \leq sup (A ℝ <)$
28	10	sselda	$⊢ ((φ \land A \neq \emptyset) \land k \in A) \to k \in ℤ_{\geq M}$
29	14 22	sselid	$⊢ (φ \land A \neq \emptyset) \to sup (A ℝ <) \in ℤ$
30	29	adantr	$⊢ ((φ \land A \neq \emptyset) \land k \in A) \to sup (A ℝ <) \in ℤ$
31		elfz5	$⊢ (k \in ℤ_{\geq M} \land sup (A ℝ <) \in ℤ) \to (k \in (M \dots sup (A ℝ <)) \leftrightarrow k \leq sup (A ℝ <))$
32	28 30 31	syl2anc	$⊢ ((φ \land A \neq \emptyset) \land k \in A) \to (k \in (M \dots sup (A ℝ <)) \leftrightarrow k \leq sup (A ℝ <))$
33	27 32	mpbird	$⊢ ((φ \land A \neq \emptyset) \land k \in A) \to k \in (M \dots sup (A ℝ <))$
34	33	ex	$⊢ (φ \land A \neq \emptyset) \to (k \in A \to k \in (M \dots sup (A ℝ <)))$
35	34	ssrdv	$⊢ (φ \land A \neq \emptyset) \to A \subseteq (M \dots sup (A ℝ <))$
36		oveq2	$⊢ n = sup (A ℝ <) \to (M \dots n) = (M \dots sup (A ℝ <))$
37	36	sseq2d	$⊢ n = sup (A ℝ <) \to (A \subseteq (M \dots n) \leftrightarrow A \subseteq (M \dots sup (A ℝ <)))$
38	37	rspcev	$⊢ (sup (A ℝ <) \in ℤ_{\geq M} \land A \subseteq (M \dots sup (A ℝ <))) \to \exists n \in ℤ_{\geq M} A \subseteq (M \dots n)$
39	22 35 38	syl2anc	$⊢ (φ \land A \neq \emptyset) \to \exists n \in ℤ_{\geq M} A \subseteq (M \dots n)$
40		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
41	2 40	syl	$⊢ φ \to M \in ℤ_{\geq M}$
42		0ss	$⊢ \emptyset \subseteq (M \dots M)$
43		oveq2	$⊢ n = M \to (M \dots n) = (M \dots M)$
44	43	sseq2d	$⊢ n = M \to (\emptyset \subseteq (M \dots n) \leftrightarrow \emptyset \subseteq (M \dots M))$
45	44	rspcev	$⊢ (M \in ℤ_{\geq M} \land \emptyset \subseteq (M \dots M)) \to \exists n \in ℤ_{\geq M} \emptyset \subseteq (M \dots n)$
46	41 42 45	sylancl	$⊢ φ \to \exists n \in ℤ_{\geq M} \emptyset \subseteq (M \dots n)$
47	8 39 46	pm2.61ne	$⊢ φ \to \exists n \in ℤ_{\geq M} A \subseteq (M \dots n)$
48	1	eleq2i	$⊢ k \in Z \leftrightarrow k \in ℤ_{\geq M}$
49	48 5	sylan2br	$⊢ (φ \land k \in ℤ_{\geq M}) \to F (k) = if (k \in A, B, 0)$
50	49	adantlr	$⊢ ((φ \land (n \in ℤ_{\geq M} \land A \subseteq (M \dots n))) \land k \in ℤ_{\geq M}) \to F (k) = if (k \in A, B, 0)$
51		simprl	$⊢ (φ \land (n \in ℤ_{\geq M} \land A \subseteq (M \dots n))) \to n \in ℤ_{\geq M}$
52	6	adantlr	$⊢ ((φ \land (n \in ℤ_{\geq M} \land A \subseteq (M \dots n))) \land k \in A) \to B \in ℂ$
53		simprr	$⊢ (φ \land (n \in ℤ_{\geq M} \land A \subseteq (M \dots n))) \to A \subseteq (M \dots n)$
54	50 51 52 53	fsumcvg2	$⊢ (φ \land (n \in ℤ_{\geq M} \land A \subseteq (M \dots n))) \to seq M (+ F) ⇝ seq M (+ F) (n)$
55		climrel	$⊢ Rel ⇝$
56	55	releldmi	$⊢ seq M (+ F) ⇝ seq M (+ F) (n) \to seq M (+ F) \in dom ⇝$
57	54 56	syl	$⊢ (φ \land (n \in ℤ_{\geq M} \land A \subseteq (M \dots n))) \to seq M (+ F) \in dom ⇝$
58	47 57	rexlimddv	$⊢ φ \to seq M (+ F) \in dom ⇝$

Metamath Proof Explorer

Theorem fsumcvg3

Proof