mettrifi

Description: Generalized triangle inequality for arbitrary finite sums. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 4-Jun-2014)

	Ref	Expression
Hypotheses	mettrifi.2	$⊢ φ \to D \in Met (X)$
	mettrifi.3	$⊢ φ \to N \in ℤ_{\geq M}$
	mettrifi.4	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in X$
Assertion	mettrifi	$⊢ φ \to F (M) D F (N) \leq \sum_{k = M}^{N - 1} (F (k) D F (k + 1))$

Proof

Step	Hyp	Ref	Expression
1		mettrifi.2	$⊢ φ \to D \in Met (X)$
2		mettrifi.3	$⊢ φ \to N \in ℤ_{\geq M}$
3		mettrifi.4	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in X$
4		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
5	2 4	syl	$⊢ φ \to N \in (M \dots N)$
6		eleq1	$⊢ x = M \to (x \in (M \dots N) \leftrightarrow M \in (M \dots N))$
7		fveq2	$⊢ x = M \to F (x) = F (M)$
8	7	oveq2d	$⊢ x = M \to F (M) D F (x) = F (M) D F (M)$
9		oveq1	$⊢ x = M \to x - 1 = M - 1$
10	9	oveq2d	$⊢ x = M \to (M \dots x - 1) = (M \dots M - 1)$
11	10	sumeq1d	$⊢ x = M \to \sum_{k = M}^{x - 1} (F (k) D F (k + 1)) = \sum_{k = M}^{M - 1} (F (k) D F (k + 1))$
12	8 11	breq12d	$⊢ x = M \to (F (M) D F (x) \leq \sum_{k = M}^{x - 1} (F (k) D F (k + 1)) \leftrightarrow F (M) D F (M) \leq \sum_{k = M}^{M - 1} (F (k) D F (k + 1)))$
13	6 12	imbi12d	$⊢ x = M \to ((x \in (M \dots N) \to F (M) D F (x) \leq \sum_{k = M}^{x - 1} (F (k) D F (k + 1))) \leftrightarrow (M \in (M \dots N) \to F (M) D F (M) \leq \sum_{k = M}^{M - 1} (F (k) D F (k + 1))))$
14	13	imbi2d	$⊢ x = M \to ((φ \to (x \in (M \dots N) \to F (M) D F (x) \leq \sum_{k = M}^{x - 1} (F (k) D F (k + 1)))) \leftrightarrow (φ \to (M \in (M \dots N) \to F (M) D F (M) \leq \sum_{k = M}^{M - 1} (F (k) D F (k + 1)))))$
15		eleq1	$⊢ x = n \to (x \in (M \dots N) \leftrightarrow n \in (M \dots N))$
16		fveq2	$⊢ x = n \to F (x) = F (n)$
17	16	oveq2d	$⊢ x = n \to F (M) D F (x) = F (M) D F (n)$
18		oveq1	$⊢ x = n \to x - 1 = n - 1$
19	18	oveq2d	$⊢ x = n \to (M \dots x - 1) = (M \dots n - 1)$
20	19	sumeq1d	$⊢ x = n \to \sum_{k = M}^{x - 1} (F (k) D F (k + 1)) = \sum_{k = M}^{n - 1} (F (k) D F (k + 1))$
21	17 20	breq12d	$⊢ x = n \to (F (M) D F (x) \leq \sum_{k = M}^{x - 1} (F (k) D F (k + 1)) \leftrightarrow F (M) D F (n) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1)))$
22	15 21	imbi12d	$⊢ x = n \to ((x \in (M \dots N) \to F (M) D F (x) \leq \sum_{k = M}^{x - 1} (F (k) D F (k + 1))) \leftrightarrow (n \in (M \dots N) \to F (M) D F (n) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1))))$
23	22	imbi2d	$⊢ x = n \to ((φ \to (x \in (M \dots N) \to F (M) D F (x) \leq \sum_{k = M}^{x - 1} (F (k) D F (k + 1)))) \leftrightarrow (φ \to (n \in (M \dots N) \to F (M) D F (n) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1)))))$
24		eleq1	$⊢ x = n + 1 \to (x \in (M \dots N) \leftrightarrow n + 1 \in (M \dots N))$
25		fveq2	$⊢ x = n + 1 \to F (x) = F (n + 1)$
26	25	oveq2d	$⊢ x = n + 1 \to F (M) D F (x) = F (M) D F (n + 1)$
27		oveq1	$⊢ x = n + 1 \to x - 1 = n + 1 - 1$
28	27	oveq2d	$⊢ x = n + 1 \to (M \dots x - 1) = (M \dots n + 1 - 1)$
29	28	sumeq1d	$⊢ x = n + 1 \to \sum_{k = M}^{x - 1} (F (k) D F (k + 1)) = \sum_{k = M}^{n + 1 - 1} (F (k) D F (k + 1))$
30	26 29	breq12d	$⊢ x = n + 1 \to (F (M) D F (x) \leq \sum_{k = M}^{x - 1} (F (k) D F (k + 1)) \leftrightarrow F (M) D F (n + 1) \leq \sum_{k = M}^{n + 1 - 1} (F (k) D F (k + 1)))$
31	24 30	imbi12d	$⊢ x = n + 1 \to ((x \in (M \dots N) \to F (M) D F (x) \leq \sum_{k = M}^{x - 1} (F (k) D F (k + 1))) \leftrightarrow (n + 1 \in (M \dots N) \to F (M) D F (n + 1) \leq \sum_{k = M}^{n + 1 - 1} (F (k) D F (k + 1))))$
32	31	imbi2d	$⊢ x = n + 1 \to ((φ \to (x \in (M \dots N) \to F (M) D F (x) \leq \sum_{k = M}^{x - 1} (F (k) D F (k + 1)))) \leftrightarrow (φ \to (n + 1 \in (M \dots N) \to F (M) D F (n + 1) \leq \sum_{k = M}^{n + 1 - 1} (F (k) D F (k + 1)))))$
33		eleq1	$⊢ x = N \to (x \in (M \dots N) \leftrightarrow N \in (M \dots N))$
34		fveq2	$⊢ x = N \to F (x) = F (N)$
35	34	oveq2d	$⊢ x = N \to F (M) D F (x) = F (M) D F (N)$
36		oveq1	$⊢ x = N \to x - 1 = N - 1$
37	36	oveq2d	$⊢ x = N \to (M \dots x - 1) = (M \dots N - 1)$
38	37	sumeq1d	$⊢ x = N \to \sum_{k = M}^{x - 1} (F (k) D F (k + 1)) = \sum_{k = M}^{N - 1} (F (k) D F (k + 1))$
39	35 38	breq12d	$⊢ x = N \to (F (M) D F (x) \leq \sum_{k = M}^{x - 1} (F (k) D F (k + 1)) \leftrightarrow F (M) D F (N) \leq \sum_{k = M}^{N - 1} (F (k) D F (k + 1)))$
40	33 39	imbi12d	$⊢ x = N \to ((x \in (M \dots N) \to F (M) D F (x) \leq \sum_{k = M}^{x - 1} (F (k) D F (k + 1))) \leftrightarrow (N \in (M \dots N) \to F (M) D F (N) \leq \sum_{k = M}^{N - 1} (F (k) D F (k + 1))))$
41	40	imbi2d	$⊢ x = N \to ((φ \to (x \in (M \dots N) \to F (M) D F (x) \leq \sum_{k = M}^{x - 1} (F (k) D F (k + 1)))) \leftrightarrow (φ \to (N \in (M \dots N) \to F (M) D F (N) \leq \sum_{k = M}^{N - 1} (F (k) D F (k + 1)))))$
42		0le0	$⊢ 0 \leq 0$
43	42	a1i	$⊢ φ \to 0 \leq 0$
44		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
45	2 44	syl	$⊢ φ \to M \in (M \dots N)$
46	3	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) F (k) \in X$
47		fveq2	$⊢ k = M \to F (k) = F (M)$
48	47	eleq1d	$⊢ k = M \to (F (k) \in X \leftrightarrow F (M) \in X)$
49	48	rspcv	$⊢ M \in (M \dots N) \to (\forall k \in (M \dots N) F (k) \in X \to F (M) \in X)$
50	45 46 49	sylc	$⊢ φ \to F (M) \in X$
51		met0	$⊢ (D \in Met (X) \land F (M) \in X) \to F (M) D F (M) = 0$
52	1 50 51	syl2anc	$⊢ φ \to F (M) D F (M) = 0$
53		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
54	2 53	syl	$⊢ φ \to M \in ℤ$
55	54	zred	$⊢ φ \to M \in ℝ$
56	55	ltm1d	$⊢ φ \to M - 1 < M$
57		peano2zm	$⊢ M \in ℤ \to M - 1 \in ℤ$
58		fzn	$⊢ (M \in ℤ \land M - 1 \in ℤ) \to (M - 1 < M \leftrightarrow (M \dots M - 1) = \emptyset)$
59	54 57 58	syl2anc2	$⊢ φ \to (M - 1 < M \leftrightarrow (M \dots M - 1) = \emptyset)$
60	56 59	mpbid	$⊢ φ \to (M \dots M - 1) = \emptyset$
61	60	sumeq1d	$⊢ φ \to \sum_{k = M}^{M - 1} (F (k) D F (k + 1)) = \sum_{k \in \emptyset} (F (k) D F (k + 1))$
62		sum0	$⊢ \sum_{k \in \emptyset} (F (k) D F (k + 1)) = 0$
63	61 62	eqtrdi	$⊢ φ \to \sum_{k = M}^{M - 1} (F (k) D F (k + 1)) = 0$
64	43 52 63	3brtr4d	$⊢ φ \to F (M) D F (M) \leq \sum_{k = M}^{M - 1} (F (k) D F (k + 1))$
65	64	a1d	$⊢ φ \to (M \in (M \dots N) \to F (M) D F (M) \leq \sum_{k = M}^{M - 1} (F (k) D F (k + 1)))$
66	65	a1i	$⊢ M \in ℤ \to (φ \to (M \in (M \dots N) \to F (M) D F (M) \leq \sum_{k = M}^{M - 1} (F (k) D F (k + 1))))$
67		peano2fzr	$⊢ (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to n \in (M \dots N)$
68	67	ex	$⊢ n \in ℤ_{\geq M} \to (n + 1 \in (M \dots N) \to n \in (M \dots N))$
69	68	adantl	$⊢ (φ \land n \in ℤ_{\geq M}) \to (n + 1 \in (M \dots N) \to n \in (M \dots N))$
70	69	imim1d	$⊢ (φ \land n \in ℤ_{\geq M}) \to ((n \in (M \dots N) \to F (M) D F (n) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1))) \to (n + 1 \in (M \dots N) \to F (M) D F (n) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1))))$
71	1	3ad2ant1	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to D \in Met (X)$
72	50	3ad2ant1	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to F (M) \in X$
73		simp3	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to n + 1 \in (M \dots N)$
74	46	3ad2ant1	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to \forall k \in (M \dots N) F (k) \in X$
75		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
76	75	eleq1d	$⊢ k = n + 1 \to (F (k) \in X \leftrightarrow F (n + 1) \in X)$
77	76	rspcv	$⊢ n + 1 \in (M \dots N) \to (\forall k \in (M \dots N) F (k) \in X \to F (n + 1) \in X)$
78	73 74 77	sylc	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to F (n + 1) \in X$
79		fveq2	$⊢ k = n \to F (k) = F (n)$
80	79	eleq1d	$⊢ k = n \to (F (k) \in X \leftrightarrow F (n) \in X)$
81	80	cbvralvw	$⊢ \forall k \in (M \dots N) F (k) \in X \leftrightarrow \forall n \in (M \dots N) F (n) \in X$
82	74 81	sylib	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to \forall n \in (M \dots N) F (n) \in X$
83	69	3impia	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to n \in (M \dots N)$
84		rsp	$⊢ \forall n \in (M \dots N) F (n) \in X \to (n \in (M \dots N) \to F (n) \in X)$
85	82 83 84	sylc	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to F (n) \in X$
86		mettri	$⊢ (D \in Met (X) \land (F (M) \in X \land F (n + 1) \in X \land F (n) \in X)) \to F (M) D F (n + 1) \leq (F (M) D F (n)) + (F (n) D F (n + 1))$
87	71 72 78 85 86	syl13anc	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to F (M) D F (n + 1) \leq (F (M) D F (n)) + (F (n) D F (n + 1))$
88		metcl	$⊢ (D \in Met (X) \land F (M) \in X \land F (n + 1) \in X) \to F (M) D F (n + 1) \in ℝ$
89	71 72 78 88	syl3anc	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to F (M) D F (n + 1) \in ℝ$
90		metcl	$⊢ (D \in Met (X) \land F (M) \in X \land F (n) \in X) \to F (M) D F (n) \in ℝ$
91	71 72 85 90	syl3anc	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to F (M) D F (n) \in ℝ$
92		metcl	$⊢ (D \in Met (X) \land F (n) \in X \land F (n + 1) \in X) \to F (n) D F (n + 1) \in ℝ$
93	71 85 78 92	syl3anc	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to F (n) D F (n + 1) \in ℝ$
94	91 93	readdcld	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to (F (M) D F (n)) + (F (n) D F (n + 1)) \in ℝ$
95		fzfid	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to (M \dots n) \in Fin$
96	71	adantr	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n)) \to D \in Met (X)$
97		elfzuz3	$⊢ n \in (M \dots N) \to N \in ℤ_{\geq n}$
98	83 97	syl	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to N \in ℤ_{\geq n}$
99		fzss2	$⊢ N \in ℤ_{\geq n} \to (M \dots n) \subseteq (M \dots N)$
100	98 99	syl	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to (M \dots n) \subseteq (M \dots N)$
101	100	sselda	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n)) \to k \in (M \dots N)$
102	3	3ad2antl1	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots N)) \to F (k) \in X$
103	101 102	syldan	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n)) \to F (k) \in X$
104		elfzuz	$⊢ k \in (M \dots n) \to k \in ℤ_{\geq M}$
105	104	adantl	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n)) \to k \in ℤ_{\geq M}$
106		peano2uz	$⊢ k \in ℤ_{\geq M} \to k + 1 \in ℤ_{\geq M}$
107	105 106	syl	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n)) \to k + 1 \in ℤ_{\geq M}$
108		elfzuz3	$⊢ n + 1 \in (M \dots N) \to N \in ℤ_{\geq (n + 1)}$
109	73 108	syl	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to N \in ℤ_{\geq (n + 1)}$
110	109	adantr	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n)) \to N \in ℤ_{\geq (n + 1)}$
111		elfzuz3	$⊢ k \in (M \dots n) \to n \in ℤ_{\geq k}$
112	111	adantl	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n)) \to n \in ℤ_{\geq k}$
113		eluzp1p1	$⊢ n \in ℤ_{\geq k} \to n + 1 \in ℤ_{\geq (k + 1)}$
114	112 113	syl	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n)) \to n + 1 \in ℤ_{\geq (k + 1)}$
115		uztrn	$⊢ (N \in ℤ_{\geq (n + 1)} \land n + 1 \in ℤ_{\geq (k + 1)}) \to N \in ℤ_{\geq (k + 1)}$
116	110 114 115	syl2anc	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n)) \to N \in ℤ_{\geq (k + 1)}$
117		elfzuzb	$⊢ k + 1 \in (M \dots N) \leftrightarrow (k + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq (k + 1)})$
118	107 116 117	sylanbrc	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n)) \to k + 1 \in (M \dots N)$
119		fveq2	$⊢ n = k + 1 \to F (n) = F (k + 1)$
120	119	eleq1d	$⊢ n = k + 1 \to (F (n) \in X \leftrightarrow F (k + 1) \in X)$
121	120	rspccva	$⊢ (\forall n \in (M \dots N) F (n) \in X \land k + 1 \in (M \dots N)) \to F (k + 1) \in X$
122	82 121	sylan	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k + 1 \in (M \dots N)) \to F (k + 1) \in X$
123	118 122	syldan	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n)) \to F (k + 1) \in X$
124		metcl	$⊢ (D \in Met (X) \land F (k) \in X \land F (k + 1) \in X) \to F (k) D F (k + 1) \in ℝ$
125	96 103 123 124	syl3anc	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n)) \to F (k) D F (k + 1) \in ℝ$
126	95 125	fsumrecl	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to \sum_{k = M}^{n} (F (k) D F (k + 1)) \in ℝ$
127		letr	$⊢ (F (M) D F (n + 1) \in ℝ \land (F (M) D F (n)) + (F (n) D F (n + 1)) \in ℝ \land \sum_{k = M}^{n} (F (k) D F (k + 1)) \in ℝ) \to ((F (M) D F (n + 1) \leq (F (M) D F (n)) + (F (n) D F (n + 1)) \land (F (M) D F (n)) + (F (n) D F (n + 1)) \leq \sum_{k = M}^{n} (F (k) D F (k + 1))) \to F (M) D F (n + 1) \leq \sum_{k = M}^{n} (F (k) D F (k + 1)))$
128	89 94 126 127	syl3anc	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to ((F (M) D F (n + 1) \leq (F (M) D F (n)) + (F (n) D F (n + 1)) \land (F (M) D F (n)) + (F (n) D F (n + 1)) \leq \sum_{k = M}^{n} (F (k) D F (k + 1))) \to F (M) D F (n + 1) \leq \sum_{k = M}^{n} (F (k) D F (k + 1)))$
129	87 128	mpand	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to ((F (M) D F (n)) + (F (n) D F (n + 1)) \leq \sum_{k = M}^{n} (F (k) D F (k + 1)) \to F (M) D F (n + 1) \leq \sum_{k = M}^{n} (F (k) D F (k + 1)))$
130		fzfid	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to (M \dots n - 1) \in Fin$
131		fzssp1	$⊢ (M \dots n - 1) \subseteq (M \dots n - 1 + 1)$
132		eluzelz	$⊢ n \in ℤ_{\geq M} \to n \in ℤ$
133	132	3ad2ant2	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to n \in ℤ$
134	133	zcnd	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to n \in ℂ$
135		ax-1cn	$⊢ 1 \in ℂ$
136		npcan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n - 1 + 1 = n$
137	134 135 136	sylancl	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to n - 1 + 1 = n$
138	137	oveq2d	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to (M \dots n - 1 + 1) = (M \dots n)$
139	131 138	sseqtrid	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to (M \dots n - 1) \subseteq (M \dots n)$
140	139	sselda	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n - 1)) \to k \in (M \dots n)$
141	140 125	syldan	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n - 1)) \to F (k) D F (k + 1) \in ℝ$
142	130 141	fsumrecl	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to \sum_{k = M}^{n - 1} (F (k) D F (k + 1)) \in ℝ$
143	91 142 93	leadd1d	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to (F (M) D F (n) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1)) \leftrightarrow (F (M) D F (n)) + (F (n) D F (n + 1)) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1)) + (F (n) D F (n + 1)))$
144		simp2	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to n \in ℤ_{\geq M}$
145	125	recnd	$⊢ ((φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \land k \in (M \dots n)) \to F (k) D F (k + 1) \in ℂ$
146		fvoveq1	$⊢ k = n \to F (k + 1) = F (n + 1)$
147	79 146	oveq12d	$⊢ k = n \to F (k) D F (k + 1) = F (n) D F (n + 1)$
148	144 145 147	fsumm1	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to \sum_{k = M}^{n} (F (k) D F (k + 1)) = \sum_{k = M}^{n - 1} (F (k) D F (k + 1)) + (F (n) D F (n + 1))$
149	148	breq2d	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to ((F (M) D F (n)) + (F (n) D F (n + 1)) \leq \sum_{k = M}^{n} (F (k) D F (k + 1)) \leftrightarrow (F (M) D F (n)) + (F (n) D F (n + 1)) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1)) + (F (n) D F (n + 1)))$
150	143 149	bitr4d	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to (F (M) D F (n) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1)) \leftrightarrow (F (M) D F (n)) + (F (n) D F (n + 1)) \leq \sum_{k = M}^{n} (F (k) D F (k + 1)))$
151		pncan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n + 1 - 1 = n$
152	134 135 151	sylancl	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to n + 1 - 1 = n$
153	152	oveq2d	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to (M \dots n + 1 - 1) = (M \dots n)$
154	153	sumeq1d	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to \sum_{k = M}^{n + 1 - 1} (F (k) D F (k + 1)) = \sum_{k = M}^{n} (F (k) D F (k + 1))$
155	154	breq2d	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to (F (M) D F (n + 1) \leq \sum_{k = M}^{n + 1 - 1} (F (k) D F (k + 1)) \leftrightarrow F (M) D F (n + 1) \leq \sum_{k = M}^{n} (F (k) D F (k + 1)))$
156	129 150 155	3imtr4d	$⊢ (φ \land n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to (F (M) D F (n) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1)) \to F (M) D F (n + 1) \leq \sum_{k = M}^{n + 1 - 1} (F (k) D F (k + 1)))$
157	156	3expia	$⊢ (φ \land n \in ℤ_{\geq M}) \to (n + 1 \in (M \dots N) \to (F (M) D F (n) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1)) \to F (M) D F (n + 1) \leq \sum_{k = M}^{n + 1 - 1} (F (k) D F (k + 1))))$
158	157	a2d	$⊢ (φ \land n \in ℤ_{\geq M}) \to ((n + 1 \in (M \dots N) \to F (M) D F (n) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1))) \to (n + 1 \in (M \dots N) \to F (M) D F (n + 1) \leq \sum_{k = M}^{n + 1 - 1} (F (k) D F (k + 1))))$
159	70 158	syld	$⊢ (φ \land n \in ℤ_{\geq M}) \to ((n \in (M \dots N) \to F (M) D F (n) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1))) \to (n + 1 \in (M \dots N) \to F (M) D F (n + 1) \leq \sum_{k = M}^{n + 1 - 1} (F (k) D F (k + 1))))$
160	159	expcom	$⊢ n \in ℤ_{\geq M} \to (φ \to ((n \in (M \dots N) \to F (M) D F (n) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1))) \to (n + 1 \in (M \dots N) \to F (M) D F (n + 1) \leq \sum_{k = M}^{n + 1 - 1} (F (k) D F (k + 1)))))$
161	160	a2d	$⊢ n \in ℤ_{\geq M} \to ((φ \to (n \in (M \dots N) \to F (M) D F (n) \leq \sum_{k = M}^{n - 1} (F (k) D F (k + 1)))) \to (φ \to (n + 1 \in (M \dots N) \to F (M) D F (n + 1) \leq \sum_{k = M}^{n + 1 - 1} (F (k) D F (k + 1)))))$
162	14 23 32 41 66 161	uzind4	$⊢ N \in ℤ_{\geq M} \to (φ \to (N \in (M \dots N) \to F (M) D F (N) \leq \sum_{k = M}^{N - 1} (F (k) D F (k + 1))))$
163	2 162	mpcom	$⊢ φ \to (N \in (M \dots N) \to F (M) D F (N) \leq \sum_{k = M}^{N - 1} (F (k) D F (k + 1)))$
164	5 163	mpd	$⊢ φ \to F (M) D F (N) \leq \sum_{k = M}^{N - 1} (F (k) D F (k + 1))$

Metamath Proof Explorer

Theorem mettrifi

Proof