dvfsumge

Description: Compare a finite sum to an integral (the integral here is given as a function with a known derivative). (Contributed by Mario Carneiro, 14-May-2016)

	Ref	Expression
Hypotheses	dvfsumleOLD.m	$⊢ φ \to N \in ℤ_{\geq M}$
	dvfsumleOLD.a	$⊢ φ \to (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℝ$
	dvfsumleOLD.v	$⊢ (φ \land x \in (M, N)) \to B \in V$
	dvfsumleOLD.b	$⊢ φ \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (x \in (M, N) ⟼ B)$
	dvfsumleOLD.c	$⊢ x = M \to A = C$
	dvfsumleOLD.d	$⊢ x = N \to A = D$
	dvfsumleOLD.x	$⊢ (φ \land k \in (M ..^N)) \to X \in ℝ$
	dvfsumge.l	$⊢ (φ \land (k \in (M ..^N) \land x \in (k, k + 1))) \to B \leq X$
Assertion	dvfsumge	$⊢ φ \to D - C \leq \sum_{k \in (M ..^N)} X$

Proof

Step	Hyp	Ref	Expression
1		dvfsumleOLD.m	$⊢ φ \to N \in ℤ_{\geq M}$
2		dvfsumleOLD.a	$⊢ φ \to (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℝ$
3		dvfsumleOLD.v	$⊢ (φ \land x \in (M, N)) \to B \in V$
4		dvfsumleOLD.b	$⊢ φ \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (x \in (M, N) ⟼ B)$
5		dvfsumleOLD.c	$⊢ x = M \to A = C$
6		dvfsumleOLD.d	$⊢ x = N \to A = D$
7		dvfsumleOLD.x	$⊢ (φ \land k \in (M ..^N)) \to X \in ℝ$
8		dvfsumge.l	$⊢ (φ \land (k \in (M ..^N) \land x \in (k, k + 1))) \to B \leq X$
9		df-neg	$⊢ - A = 0 - A$
10	9	mpteq2i	$⊢ (x \in [M, N] ⟼ - A) = (x \in [M, N] ⟼ 0 - A)$
11		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
12	11	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
13		0red	$⊢ φ \to 0 \in ℝ$
14		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
15	1 14	syl	$⊢ φ \to M \in ℤ$
16	15	zred	$⊢ φ \to M \in ℝ$
17		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
18	1 17	syl	$⊢ φ \to N \in ℤ$
19	18	zred	$⊢ φ \to N \in ℝ$
20		iccssre	$⊢ (M \in ℝ \land N \in ℝ) \to [M, N] \subseteq ℝ$
21	16 19 20	syl2anc	$⊢ φ \to [M, N] \subseteq ℝ$
22		ax-resscn	$⊢ ℝ \subseteq ℂ$
23	21 22	sstrdi	$⊢ φ \to [M, N] \subseteq ℂ$
24	22	a1i	$⊢ φ \to ℝ \subseteq ℂ$
25		cncfmptc	$⊢ (0 \in ℝ \land [M, N] \subseteq ℂ \land ℝ \subseteq ℂ) \to (x \in [M, N] ⟼ 0) : [M, N] \underset{cn}{⟶} ℝ$
26	13 23 24 25	syl3anc	$⊢ φ \to (x \in [M, N] ⟼ 0) : [M, N] \underset{cn}{⟶} ℝ$
27		resubcl	$⊢ (0 \in ℝ \land A \in ℝ) \to 0 - A \in ℝ$
28	11 12 26 2 22 27	cncfmpt2ss	$⊢ φ \to (x \in [M, N] ⟼ 0 - A) : [M, N] \underset{cn}{⟶} ℝ$
29	10 28	eqeltrid	$⊢ φ \to (x \in [M, N] ⟼ - A) : [M, N] \underset{cn}{⟶} ℝ$
30		negex	$⊢ - B \in V$
31	30	a1i	$⊢ (φ \land x \in (M, N)) \to - B \in V$
32		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
33	32	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
34		ioossicc	$⊢ (M, N) \subseteq [M, N]$
35	34	sseli	$⊢ x \in (M, N) \to x \in [M, N]$
36		cncff	$⊢ (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℝ \to (x \in [M, N] ⟼ A) : [M, N] ⟶ ℝ$
37	2 36	syl	$⊢ φ \to (x \in [M, N] ⟼ A) : [M, N] ⟶ ℝ$
38	37	fvmptelcdm	$⊢ (φ \land x \in [M, N]) \to A \in ℝ$
39	35 38	sylan2	$⊢ (φ \land x \in (M, N)) \to A \in ℝ$
40	39	recnd	$⊢ (φ \land x \in (M, N)) \to A \in ℂ$
41	33 40 3 4	dvmptneg	$⊢ φ \to \frac{d (x \in (M, N)⟼ - A)}{d_{ℝ} x} = (x \in (M, N) ⟼ - B)$
42	5	negeqd	$⊢ x = M \to - A = - C$
43	6	negeqd	$⊢ x = N \to - A = - D$
44	7	renegcld	$⊢ (φ \land k \in (M ..^N)) \to - X \in ℝ$
45	16	adantr	$⊢ (φ \land k \in (M ..^N)) \to M \in ℝ$
46	45	rexrd	$⊢ (φ \land k \in (M ..^N)) \to M \in ℝ^{*}$
47		elfzole1	$⊢ k \in (M ..^N) \to M \leq k$
48	47	adantl	$⊢ (φ \land k \in (M ..^N)) \to M \leq k$
49		iooss1	$⊢ (M \in ℝ^{*} \land M \leq k) \to (k, k + 1) \subseteq (M, k + 1)$
50	46 48 49	syl2anc	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \subseteq (M, k + 1)$
51	19	adantr	$⊢ (φ \land k \in (M ..^N)) \to N \in ℝ$
52	51	rexrd	$⊢ (φ \land k \in (M ..^N)) \to N \in ℝ^{*}$
53		fzofzp1	$⊢ k \in (M ..^N) \to k + 1 \in (M \dots N)$
54	53	adantl	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in (M \dots N)$
55		elfzle2	$⊢ k + 1 \in (M \dots N) \to k + 1 \leq N$
56	54 55	syl	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \leq N$
57		iooss2	$⊢ (N \in ℝ^{*} \land k + 1 \leq N) \to (M, k + 1) \subseteq (M, N)$
58	52 56 57	syl2anc	$⊢ (φ \land k \in (M ..^N)) \to (M, k + 1) \subseteq (M, N)$
59	50 58	sstrd	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \subseteq (M, N)$
60	59	sselda	$⊢ ((φ \land k \in (M ..^N)) \land x \in (k, k + 1)) \to x \in (M, N)$
61	38	adantlr	$⊢ ((φ \land k \in (M ..^N)) \land x \in [M, N]) \to A \in ℝ$
62	35 61	sylan2	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to A \in ℝ$
63	62	fmpttd	$⊢ (φ \land k \in (M ..^N)) \to (x \in (M, N) ⟼ A) : (M, N) ⟶ ℝ$
64		ioossre	$⊢ (M, N) \subseteq ℝ$
65		dvfre	$⊢ ((x \in (M, N) ⟼ A) : (M, N) ⟶ ℝ \land (M, N) \subseteq ℝ) \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} : dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} ⟶ ℝ$
66	63 64 65	sylancl	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} : dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} ⟶ ℝ$
67	4	adantr	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (x \in (M, N) ⟼ B)$
68	67	dmeqd	$⊢ (φ \land k \in (M ..^N)) \to dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = dom (x \in (M, N) ⟼ B)$
69	3	adantlr	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to B \in V$
70	69	ralrimiva	$⊢ (φ \land k \in (M ..^N)) \to \forall x \in (M, N) B \in V$
71		dmmptg	$⊢ \forall x \in (M, N) B \in V \to dom (x \in (M, N) ⟼ B) = (M, N)$
72	70 71	syl	$⊢ (φ \land k \in (M ..^N)) \to dom (x \in (M, N) ⟼ B) = (M, N)$
73	68 72	eqtrd	$⊢ (φ \land k \in (M ..^N)) \to dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (M, N)$
74	67 73	feq12d	$⊢ (φ \land k \in (M ..^N)) \to (\frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} : dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} ⟶ ℝ \leftrightarrow (x \in (M, N) ⟼ B) : (M, N) ⟶ ℝ)$
75	66 74	mpbid	$⊢ (φ \land k \in (M ..^N)) \to (x \in (M, N) ⟼ B) : (M, N) ⟶ ℝ$
76	75	fvmptelcdm	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to B \in ℝ$
77	60 76	syldan	$⊢ ((φ \land k \in (M ..^N)) \land x \in (k, k + 1)) \to B \in ℝ$
78	77	anasss	$⊢ (φ \land (k \in (M ..^N) \land x \in (k, k + 1))) \to B \in ℝ$
79	7	adantrr	$⊢ (φ \land (k \in (M ..^N) \land x \in (k, k + 1))) \to X \in ℝ$
80	78 79	lenegd	$⊢ (φ \land (k \in (M ..^N) \land x \in (k, k + 1))) \to (B \leq X \leftrightarrow - X \leq - B)$
81	8 80	mpbid	$⊢ (φ \land (k \in (M ..^N) \land x \in (k, k + 1))) \to - X \leq - B$
82	1 29 31 41 42 43 44 81	dvfsumle	$⊢ φ \to \sum_{k \in (M ..^N)} (- X) \leq - D - (- C)$
83		fzofi	$⊢ (M ..^N) \in Fin$
84	83	a1i	$⊢ φ \to (M ..^N) \in Fin$
85	7	recnd	$⊢ (φ \land k \in (M ..^N)) \to X \in ℂ$
86	84 85	fsumneg	$⊢ φ \to \sum_{k \in (M ..^N)} (- X) = - \sum_{k \in (M ..^N)} X$
87	6	eleq1d	$⊢ x = N \to (A \in ℝ \leftrightarrow D \in ℝ)$
88		eqid	$⊢ (x \in [M, N] ⟼ A) = (x \in [M, N] ⟼ A)$
89	88	fmpt	$⊢ \forall x \in [M, N] A \in ℝ \leftrightarrow (x \in [M, N] ⟼ A) : [M, N] ⟶ ℝ$
90	37 89	sylibr	$⊢ φ \to \forall x \in [M, N] A \in ℝ$
91	16	rexrd	$⊢ φ \to M \in ℝ^{*}$
92	19	rexrd	$⊢ φ \to N \in ℝ^{*}$
93		eluzle	$⊢ N \in ℤ_{\geq M} \to M \leq N$
94	1 93	syl	$⊢ φ \to M \leq N$
95		ubicc2	$⊢ (M \in ℝ^{} \land N \in ℝ^{} \land M \leq N) \to N \in [M, N]$
96	91 92 94 95	syl3anc	$⊢ φ \to N \in [M, N]$
97	87 90 96	rspcdva	$⊢ φ \to D \in ℝ$
98	97	recnd	$⊢ φ \to D \in ℂ$
99	5	eleq1d	$⊢ x = M \to (A \in ℝ \leftrightarrow C \in ℝ)$
100		lbicc2	$⊢ (M \in ℝ^{} \land N \in ℝ^{} \land M \leq N) \to M \in [M, N]$
101	91 92 94 100	syl3anc	$⊢ φ \to M \in [M, N]$
102	99 90 101	rspcdva	$⊢ φ \to C \in ℝ$
103	102	recnd	$⊢ φ \to C \in ℂ$
104	98 103	neg2subd	$⊢ φ \to - D - (- C) = C - D$
105	98 103	negsubdi2d	$⊢ φ \to - (D - C) = C - D$
106	104 105	eqtr4d	$⊢ φ \to - D - (- C) = - (D - C)$
107	82 86 106	3brtr3d	$⊢ φ \to - \sum_{k \in (M ..^N)} X \leq - (D - C)$
108	97 102	resubcld	$⊢ φ \to D - C \in ℝ$
109	84 7	fsumrecl	$⊢ φ \to \sum_{k \in (M ..^N)} X \in ℝ$
110	108 109	lenegd	$⊢ φ \to (D - C \leq \sum_{k \in (M ..^N)} X \leftrightarrow - \sum_{k \in (M ..^N)} X \leq - (D - C))$
111	107 110	mpbird	$⊢ φ \to D - C \leq \sum_{k \in (M ..^N)} X$

Metamath Proof Explorer

Theorem dvfsumge

Proof