Theorem 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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	isumltss.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	isumltss.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	isumltss.4	⊢ ( 𝜑 → 𝐴 ⊆ 𝑍 )
	isumltss.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
	isumltss.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ+ )
	isumltss.7	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
Assertion	isumltss	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 < Σ 𝑘 ∈ 𝑍 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		isumltss.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		isumltss.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		isumltss.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
4		isumltss.4	⊢ ( 𝜑 → 𝐴 ⊆ 𝑍 )
5		isumltss.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
6		isumltss.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ+ )
7		isumltss.7	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
8	1	uzinf	⊢ ( 𝑀 ∈ ℤ → ¬ 𝑍 ∈ Fin )
9	2 8	syl	⊢ ( 𝜑 → ¬ 𝑍 ∈ Fin )
10		ssdif0	⊢ ( 𝑍 ⊆ 𝐴 ↔ ( 𝑍 ∖ 𝐴 ) = ∅ )
11		eqss	⊢ ( 𝐴 = 𝑍 ↔ ( 𝐴 ⊆ 𝑍 ∧ 𝑍 ⊆ 𝐴 ) )
12		eleq1	⊢ ( 𝐴 = 𝑍 → ( 𝐴 ∈ Fin ↔ 𝑍 ∈ Fin ) )
13	3 12	syl5ibcom	⊢ ( 𝜑 → ( 𝐴 = 𝑍 → 𝑍 ∈ Fin ) )
14	11 13	syl5bir	⊢ ( 𝜑 → ( ( 𝐴 ⊆ 𝑍 ∧ 𝑍 ⊆ 𝐴 ) → 𝑍 ∈ Fin ) )
15	4 14	mpand	⊢ ( 𝜑 → ( 𝑍 ⊆ 𝐴 → 𝑍 ∈ Fin ) )
16	10 15	syl5bir	⊢ ( 𝜑 → ( ( 𝑍 ∖ 𝐴 ) = ∅ → 𝑍 ∈ Fin ) )
17	9 16	mtod	⊢ ( 𝜑 → ¬ ( 𝑍 ∖ 𝐴 ) = ∅ )
18		neq0	⊢ ( ¬ ( 𝑍 ∖ 𝐴 ) = ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) )
19	17 18	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) )
20	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → 𝐴 ∈ Fin )
21	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → 𝐴 ⊆ 𝑍 )
22	21	sselda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝑍 )
23	6	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ+ )
24	23	rpred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
25	22 24	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
26	20 25	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )
27		snfi	⊢ { 𝑥 } ∈ Fin
28		unfi	⊢ ( ( 𝐴 ∈ Fin ∧ { 𝑥 } ∈ Fin ) → ( 𝐴 ∪ { 𝑥 } ) ∈ Fin )
29	20 27 28	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → ( 𝐴 ∪ { 𝑥 } ) ∈ Fin )
30		eldifi	⊢ ( 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) → 𝑥 ∈ 𝑍 )
31	30	snssd	⊢ ( 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) → { 𝑥 } ⊆ 𝑍 )
32	4 31	anim12i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → ( 𝐴 ⊆ 𝑍 ∧ { 𝑥 } ⊆ 𝑍 ) )
33		unss	⊢ ( ( 𝐴 ⊆ 𝑍 ∧ { 𝑥 } ⊆ 𝑍 ) ↔ ( 𝐴 ∪ { 𝑥 } ) ⊆ 𝑍 )
34	32 33	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → ( 𝐴 ∪ { 𝑥 } ) ⊆ 𝑍 )
35	34	sselda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝑥 } ) ) → 𝑘 ∈ 𝑍 )
36	35 24	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝑥 } ) ) → 𝐵 ∈ ℝ )
37	29 36	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑥 } ) 𝐵 ∈ ℝ )
38	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → 𝑀 ∈ ℤ )
39	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
40	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
41	1 38 39 24 40	isumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → Σ 𝑘 ∈ 𝑍 𝐵 ∈ ℝ )
42	27	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → { 𝑥 } ∈ Fin )
43		vex	⊢ 𝑥 ∈ V
44	43	snnz	⊢ { 𝑥 } ≠ ∅
45	44	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → { 𝑥 } ≠ ∅ )
46	31	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → { 𝑥 } ⊆ 𝑍 )
47	46	sselda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) ∧ 𝑘 ∈ { 𝑥 } ) → 𝑘 ∈ 𝑍 )
48	47 23	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) ∧ 𝑘 ∈ { 𝑥 } ) → 𝐵 ∈ ℝ+ )
49	42 45 48	fsumrpcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → Σ 𝑘 ∈ { 𝑥 } 𝐵 ∈ ℝ+ )
50	26 49	ltaddrpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → Σ 𝑘 ∈ 𝐴 𝐵 < ( Σ 𝑘 ∈ 𝐴 𝐵 + Σ 𝑘 ∈ { 𝑥 } 𝐵 ) )
51		eldifn	⊢ ( 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
52	51	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → ¬ 𝑥 ∈ 𝐴 )
53		disjsn	⊢ ( ( 𝐴 ∩ { 𝑥 } ) = ∅ ↔ ¬ 𝑥 ∈ 𝐴 )
54	52 53	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → ( 𝐴 ∩ { 𝑥 } ) = ∅ )
55		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → ( 𝐴 ∪ { 𝑥 } ) = ( 𝐴 ∪ { 𝑥 } ) )
56	23	rpcnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
57	35 56	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝑥 } ) ) → 𝐵 ∈ ℂ )
58	54 55 29 57	fsumsplit	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑥 } ) 𝐵 = ( Σ 𝑘 ∈ 𝐴 𝐵 + Σ 𝑘 ∈ { 𝑥 } 𝐵 ) )
59	50 58	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → Σ 𝑘 ∈ 𝐴 𝐵 < Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑥 } ) 𝐵 )
60	23	rpge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ 𝐵 )
61	1 38 29 34 39 24 60 40	isumless	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → Σ 𝑘 ∈ ( 𝐴 ∪ { 𝑥 } ) 𝐵 ≤ Σ 𝑘 ∈ 𝑍 𝐵 )
62	26 37 41 59 61	ltletrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑍 ∖ 𝐴 ) ) → Σ 𝑘 ∈ 𝐴 𝐵 < Σ 𝑘 ∈ 𝑍 𝐵 )
63	19 62	exlimddv	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 < Σ 𝑘 ∈ 𝑍 𝐵 )