isumltss

Description: A partial sum of a series with positive terms is less than the infinite sum. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Mar-2015)

	Ref	Expression
Hypotheses	isumltss.1	$⊢ Z = ℤ_{\geq M}$
	isumltss.2	$⊢ φ \to M \in ℤ$
	isumltss.3	$⊢ φ \to A \in Fin$
	isumltss.4	$⊢ φ \to A \subseteq Z$
	isumltss.5	$⊢ (φ \land k \in Z) \to F (k) = B$
	isumltss.6	$⊢ (φ \land k \in Z) \to B \in ℝ^{+}$
	isumltss.7	$⊢ φ \to seq M (+ F) \in dom ⇝$
Assertion	isumltss	$⊢ φ \to \sum_{k \in A} B < \sum_{k \in Z} B$

Proof

Step	Hyp	Ref	Expression
1		isumltss.1	$⊢ Z = ℤ_{\geq M}$
2		isumltss.2	$⊢ φ \to M \in ℤ$
3		isumltss.3	$⊢ φ \to A \in Fin$
4		isumltss.4	$⊢ φ \to A \subseteq Z$
5		isumltss.5	$⊢ (φ \land k \in Z) \to F (k) = B$
6		isumltss.6	$⊢ (φ \land k \in Z) \to B \in ℝ^{+}$
7		isumltss.7	$⊢ φ \to seq M (+ F) \in dom ⇝$
8	1	uzinf	$⊢ M \in ℤ \to \neg Z \in Fin$
9	2 8	syl	$⊢ φ \to \neg Z \in Fin$
10		ssdif0	$⊢ Z \subseteq A \leftrightarrow Z ∖ A = \emptyset$
11		eqss	$⊢ A = Z \leftrightarrow (A \subseteq Z \land Z \subseteq A)$
12		eleq1	$⊢ A = Z \to (A \in Fin \leftrightarrow Z \in Fin)$
13	3 12	syl5ibcom	$⊢ φ \to (A = Z \to Z \in Fin)$
14	11 13	biimtrrid	$⊢ φ \to ((A \subseteq Z \land Z \subseteq A) \to Z \in Fin)$
15	4 14	mpand	$⊢ φ \to (Z \subseteq A \to Z \in Fin)$
16	10 15	biimtrrid	$⊢ φ \to (Z ∖ A = \emptyset \to Z \in Fin)$
17	9 16	mtod	$⊢ φ \to \neg Z ∖ A = \emptyset$
18		neq0	$⊢ \neg Z ∖ A = \emptyset \leftrightarrow \exists x x \in (Z ∖ A)$
19	17 18	sylib	$⊢ φ \to \exists x x \in (Z ∖ A)$
20	3	adantr	$⊢ (φ \land x \in (Z ∖ A)) \to A \in Fin$
21	4	adantr	$⊢ (φ \land x \in (Z ∖ A)) \to A \subseteq Z$
22	21	sselda	$⊢ ((φ \land x \in (Z ∖ A)) \land k \in A) \to k \in Z$
23	6	adantlr	$⊢ ((φ \land x \in (Z ∖ A)) \land k \in Z) \to B \in ℝ^{+}$
24	23	rpred	$⊢ ((φ \land x \in (Z ∖ A)) \land k \in Z) \to B \in ℝ$
25	22 24	syldan	$⊢ ((φ \land x \in (Z ∖ A)) \land k \in A) \to B \in ℝ$
26	20 25	fsumrecl	$⊢ (φ \land x \in (Z ∖ A)) \to \sum_{k \in A} B \in ℝ$
27		snfi	$⊢ \{x\} \in Fin$
28		unfi	$⊢ (A \in Fin \land \{x\} \in Fin) \to A \cup \{x\} \in Fin$
29	20 27 28	sylancl	$⊢ (φ \land x \in (Z ∖ A)) \to A \cup \{x\} \in Fin$
30		eldifi	$⊢ x \in (Z ∖ A) \to x \in Z$
31	30	snssd	$⊢ x \in (Z ∖ A) \to \{x\} \subseteq Z$
32	4 31	anim12i	$⊢ (φ \land x \in (Z ∖ A)) \to (A \subseteq Z \land \{x\} \subseteq Z)$
33		unss	$⊢ (A \subseteq Z \land \{x\} \subseteq Z) \leftrightarrow A \cup \{x\} \subseteq Z$
34	32 33	sylib	$⊢ (φ \land x \in (Z ∖ A)) \to A \cup \{x\} \subseteq Z$
35	34	sselda	$⊢ ((φ \land x \in (Z ∖ A)) \land k \in (A \cup \{x\})) \to k \in Z$
36	35 24	syldan	$⊢ ((φ \land x \in (Z ∖ A)) \land k \in (A \cup \{x\})) \to B \in ℝ$
37	29 36	fsumrecl	$⊢ (φ \land x \in (Z ∖ A)) \to \sum_{k \in A \cup \{x\}} B \in ℝ$
38	2	adantr	$⊢ (φ \land x \in (Z ∖ A)) \to M \in ℤ$
39	5	adantlr	$⊢ ((φ \land x \in (Z ∖ A)) \land k \in Z) \to F (k) = B$
40	7	adantr	$⊢ (φ \land x \in (Z ∖ A)) \to seq M (+ F) \in dom ⇝$
41	1 38 39 24 40	isumrecl	$⊢ (φ \land x \in (Z ∖ A)) \to \sum_{k \in Z} B \in ℝ$
42	27	a1i	$⊢ (φ \land x \in (Z ∖ A)) \to \{x\} \in Fin$
43		vex	$⊢ x \in V$
44	43	snnz	$⊢ \{x\} \neq \emptyset$
45	44	a1i	$⊢ (φ \land x \in (Z ∖ A)) \to \{x\} \neq \emptyset$
46	31	adantl	$⊢ (φ \land x \in (Z ∖ A)) \to \{x\} \subseteq Z$
47	46	sselda	$⊢ ((φ \land x \in (Z ∖ A)) \land k \in \{x\}) \to k \in Z$
48	47 23	syldan	$⊢ ((φ \land x \in (Z ∖ A)) \land k \in \{x\}) \to B \in ℝ^{+}$
49	42 45 48	fsumrpcl	$⊢ (φ \land x \in (Z ∖ A)) \to \sum_{k \in \{x\}} B \in ℝ^{+}$
50	26 49	ltaddrpd	$⊢ (φ \land x \in (Z ∖ A)) \to \sum_{k \in A} B < \sum_{k \in A} B + \sum_{k \in \{x\}} B$
51		eldifn	$⊢ x \in (Z ∖ A) \to \neg x \in A$
52	51	adantl	$⊢ (φ \land x \in (Z ∖ A)) \to \neg x \in A$
53		disjsn	$⊢ A \cap \{x\} = \emptyset \leftrightarrow \neg x \in A$
54	52 53	sylibr	$⊢ (φ \land x \in (Z ∖ A)) \to A \cap \{x\} = \emptyset$
55		eqidd	$⊢ (φ \land x \in (Z ∖ A)) \to A \cup \{x\} = A \cup \{x\}$
56	23	rpcnd	$⊢ ((φ \land x \in (Z ∖ A)) \land k \in Z) \to B \in ℂ$
57	35 56	syldan	$⊢ ((φ \land x \in (Z ∖ A)) \land k \in (A \cup \{x\})) \to B \in ℂ$
58	54 55 29 57	fsumsplit	$⊢ (φ \land x \in (Z ∖ A)) \to \sum_{k \in A \cup \{x\}} B = \sum_{k \in A} B + \sum_{k \in \{x\}} B$
59	50 58	breqtrrd	$⊢ (φ \land x \in (Z ∖ A)) \to \sum_{k \in A} B < \sum_{k \in A \cup \{x\}} B$
60	23	rpge0d	$⊢ ((φ \land x \in (Z ∖ A)) \land k \in Z) \to 0 \leq B$
61	1 38 29 34 39 24 60 40	isumless	$⊢ (φ \land x \in (Z ∖ A)) \to \sum_{k \in A \cup \{x\}} B \leq \sum_{k \in Z} B$
62	26 37 41 59 61	ltletrd	$⊢ (φ \land x \in (Z ∖ A)) \to \sum_{k \in A} B < \sum_{k \in Z} B$
63	19 62	exlimddv	$⊢ φ \to \sum_{k \in A} B < \sum_{k \in Z} B$

Metamath Proof Explorer

Theorem isumltss

Proof