sermono

Description: The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 30-Jun-2013)

	Ref	Expression
Hypotheses	sermono.1	$⊢ φ \to K \in ℤ_{\geq M}$
	sermono.2	$⊢ φ \to N \in ℤ_{\geq K}$
	sermono.3	$⊢ (φ \land x \in (M \dots N)) \to F (x) \in ℝ$
	sermono.4	$⊢ (φ \land x \in (K + 1 \dots N)) \to 0 \leq F (x)$
Assertion	sermono	$⊢ φ \to seq M (+ F) (K) \leq seq M (+ F) (N)$

Proof

Step	Hyp	Ref	Expression
1		sermono.1	$⊢ φ \to K \in ℤ_{\geq M}$
2		sermono.2	$⊢ φ \to N \in ℤ_{\geq K}$
3		sermono.3	$⊢ (φ \land x \in (M \dots N)) \to F (x) \in ℝ$
4		sermono.4	$⊢ (φ \land x \in (K + 1 \dots N)) \to 0 \leq F (x)$
5		elfzuz	$⊢ k \in (K \dots N) \to k \in ℤ_{\geq K}$
6		uztrn	$⊢ (k \in ℤ_{\geq K} \land K \in ℤ_{\geq M}) \to k \in ℤ_{\geq M}$
7	5 1 6	syl2anr	$⊢ (φ \land k \in (K \dots N)) \to k \in ℤ_{\geq M}$
8		elfzuz3	$⊢ k \in (K \dots N) \to N \in ℤ_{\geq k}$
9	8	adantl	$⊢ (φ \land k \in (K \dots N)) \to N \in ℤ_{\geq k}$
10		fzss2	$⊢ N \in ℤ_{\geq k} \to (M \dots k) \subseteq (M \dots N)$
11	9 10	syl	$⊢ (φ \land k \in (K \dots N)) \to (M \dots k) \subseteq (M \dots N)$
12	11	sselda	$⊢ ((φ \land k \in (K \dots N)) \land x \in (M \dots k)) \to x \in (M \dots N)$
13	3	adantlr	$⊢ ((φ \land k \in (K \dots N)) \land x \in (M \dots N)) \to F (x) \in ℝ$
14	12 13	syldan	$⊢ ((φ \land k \in (K \dots N)) \land x \in (M \dots k)) \to F (x) \in ℝ$
15		readdcl	$⊢ (x \in ℝ \land y \in ℝ) \to x + y \in ℝ$
16	15	adantl	$⊢ ((φ \land k \in (K \dots N)) \land (x \in ℝ \land y \in ℝ)) \to x + y \in ℝ$
17	7 14 16	seqcl	$⊢ (φ \land k \in (K \dots N)) \to seq M (+ F) (k) \in ℝ$
18		fveq2	$⊢ x = k + 1 \to F (x) = F (k + 1)$
19	18	breq2d	$⊢ x = k + 1 \to (0 \leq F (x) \leftrightarrow 0 \leq F (k + 1))$
20	4	ralrimiva	$⊢ φ \to \forall x \in (K + 1 \dots N) 0 \leq F (x)$
21	20	adantr	$⊢ (φ \land k \in (K \dots N - 1)) \to \forall x \in (K + 1 \dots N) 0 \leq F (x)$
22		simpr	$⊢ (φ \land k \in (K \dots N - 1)) \to k \in (K \dots N - 1)$
23	1	adantr	$⊢ (φ \land k \in (K \dots N - 1)) \to K \in ℤ_{\geq M}$
24		eluzelz	$⊢ K \in ℤ_{\geq M} \to K \in ℤ$
25	23 24	syl	$⊢ (φ \land k \in (K \dots N - 1)) \to K \in ℤ$
26	2	adantr	$⊢ (φ \land k \in (K \dots N - 1)) \to N \in ℤ_{\geq K}$
27		eluzelz	$⊢ N \in ℤ_{\geq K} \to N \in ℤ$
28	26 27	syl	$⊢ (φ \land k \in (K \dots N - 1)) \to N \in ℤ$
29		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
30	28 29	syl	$⊢ (φ \land k \in (K \dots N - 1)) \to N - 1 \in ℤ$
31		elfzelz	$⊢ k \in (K \dots N - 1) \to k \in ℤ$
32	31	adantl	$⊢ (φ \land k \in (K \dots N - 1)) \to k \in ℤ$
33		1zzd	$⊢ (φ \land k \in (K \dots N - 1)) \to 1 \in ℤ$
34		fzaddel	$⊢ ((K \in ℤ \land N - 1 \in ℤ) \land (k \in ℤ \land 1 \in ℤ)) \to (k \in (K \dots N - 1) \leftrightarrow k + 1 \in (K + 1 \dots N - 1 + 1))$
35	25 30 32 33 34	syl22anc	$⊢ (φ \land k \in (K \dots N - 1)) \to (k \in (K \dots N - 1) \leftrightarrow k + 1 \in (K + 1 \dots N - 1 + 1))$
36	22 35	mpbid	$⊢ (φ \land k \in (K \dots N - 1)) \to k + 1 \in (K + 1 \dots N - 1 + 1)$
37		zcn	$⊢ N \in ℤ \to N \in ℂ$
38		ax-1cn	$⊢ 1 \in ℂ$
39		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
40	37 38 39	sylancl	$⊢ N \in ℤ \to N - 1 + 1 = N$
41	28 40	syl	$⊢ (φ \land k \in (K \dots N - 1)) \to N - 1 + 1 = N$
42	41	oveq2d	$⊢ (φ \land k \in (K \dots N - 1)) \to (K + 1 \dots N - 1 + 1) = (K + 1 \dots N)$
43	36 42	eleqtrd	$⊢ (φ \land k \in (K \dots N - 1)) \to k + 1 \in (K + 1 \dots N)$
44	19 21 43	rspcdva	$⊢ (φ \land k \in (K \dots N - 1)) \to 0 \leq F (k + 1)$
45		fzelp1	$⊢ k \in (K \dots N - 1) \to k \in (K \dots N - 1 + 1)$
46	45	adantl	$⊢ (φ \land k \in (K \dots N - 1)) \to k \in (K \dots N - 1 + 1)$
47	41	oveq2d	$⊢ (φ \land k \in (K \dots N - 1)) \to (K \dots N - 1 + 1) = (K \dots N)$
48	46 47	eleqtrd	$⊢ (φ \land k \in (K \dots N - 1)) \to k \in (K \dots N)$
49	48 17	syldan	$⊢ (φ \land k \in (K \dots N - 1)) \to seq M (+ F) (k) \in ℝ$
50	18	eleq1d	$⊢ x = k + 1 \to (F (x) \in ℝ \leftrightarrow F (k + 1) \in ℝ)$
51	3	ralrimiva	$⊢ φ \to \forall x \in (M \dots N) F (x) \in ℝ$
52	51	adantr	$⊢ (φ \land k \in (K \dots N - 1)) \to \forall x \in (M \dots N) F (x) \in ℝ$
53		fzss1	$⊢ K \in ℤ_{\geq M} \to (K \dots N) \subseteq (M \dots N)$
54	23 53	syl	$⊢ (φ \land k \in (K \dots N - 1)) \to (K \dots N) \subseteq (M \dots N)$
55		fzp1elp1	$⊢ k \in (K \dots N - 1) \to k + 1 \in (K \dots N - 1 + 1)$
56	55	adantl	$⊢ (φ \land k \in (K \dots N - 1)) \to k + 1 \in (K \dots N - 1 + 1)$
57	56 47	eleqtrd	$⊢ (φ \land k \in (K \dots N - 1)) \to k + 1 \in (K \dots N)$
58	54 57	sseldd	$⊢ (φ \land k \in (K \dots N - 1)) \to k + 1 \in (M \dots N)$
59	50 52 58	rspcdva	$⊢ (φ \land k \in (K \dots N - 1)) \to F (k + 1) \in ℝ$
60	49 59	addge01d	$⊢ (φ \land k \in (K \dots N - 1)) \to (0 \leq F (k + 1) \leftrightarrow seq M (+ F) (k) \leq seq M (+ F) (k) + F (k + 1))$
61	44 60	mpbid	$⊢ (φ \land k \in (K \dots N - 1)) \to seq M (+ F) (k) \leq seq M (+ F) (k) + F (k + 1)$
62	48 7	syldan	$⊢ (φ \land k \in (K \dots N - 1)) \to k \in ℤ_{\geq M}$
63		seqp1	$⊢ k \in ℤ_{\geq M} \to seq M (+ F) (k + 1) = seq M (+ F) (k) + F (k + 1)$
64	62 63	syl	$⊢ (φ \land k \in (K \dots N - 1)) \to seq M (+ F) (k + 1) = seq M (+ F) (k) + F (k + 1)$
65	61 64	breqtrrd	$⊢ (φ \land k \in (K \dots N - 1)) \to seq M (+ F) (k) \leq seq M (+ F) (k + 1)$
66	2 17 65	monoord	$⊢ φ \to seq M (+ F) (K) \leq seq M (+ F) (N)$

Metamath Proof Explorer

Theorem sermono

Proof