intlewftc

Description: Inequality inference by invoking fundamental theorem of calculus. (Contributed by metakunt, 22-Jul-2024)

	Ref	Expression
Hypotheses	intlewftc.1	$⊢ φ \to A \in ℝ$
	intlewftc.2	$⊢ φ \to B \in ℝ$
	intlewftc.3	$⊢ φ \to A \leq B$
	intlewftc.4	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
	intlewftc.5	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℝ$
	intlewftc.6	$⊢ φ \to D = ℝ D F$
	intlewftc.7	$⊢ φ \to E = ℝ D G$
	intlewftc.8	$⊢ φ \to D : (A, B) \underset{cn}{⟶} ℝ$
	intlewftc.9	$⊢ φ \to E : (A, B) \underset{cn}{⟶} ℝ$
	intlewftc.10	$⊢ φ \to D \in 𝐿^{1}$
	intlewftc.11	$⊢ φ \to E \in 𝐿^{1}$
	intlewftc.12	$⊢ φ \to D = (x \in (A, B) ⟼ P)$
	intlewftc.13	$⊢ φ \to E = (x \in (A, B) ⟼ Q)$
	intlewftc.14	$⊢ (φ \land x \in (A, B)) \to P \leq Q$
	intlewftc.15	$⊢ φ \to F (A) \leq G (A)$
Assertion	intlewftc	$⊢ φ \to F (B) \leq G (B)$

Proof

Step	Hyp	Ref	Expression
1		intlewftc.1	$⊢ φ \to A \in ℝ$
2		intlewftc.2	$⊢ φ \to B \in ℝ$
3		intlewftc.3	$⊢ φ \to A \leq B$
4		intlewftc.4	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
5		intlewftc.5	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℝ$
6		intlewftc.6	$⊢ φ \to D = ℝ D F$
7		intlewftc.7	$⊢ φ \to E = ℝ D G$
8		intlewftc.8	$⊢ φ \to D : (A, B) \underset{cn}{⟶} ℝ$
9		intlewftc.9	$⊢ φ \to E : (A, B) \underset{cn}{⟶} ℝ$
10		intlewftc.10	$⊢ φ \to D \in 𝐿^{1}$
11		intlewftc.11	$⊢ φ \to E \in 𝐿^{1}$
12		intlewftc.12	$⊢ φ \to D = (x \in (A, B) ⟼ P)$
13		intlewftc.13	$⊢ φ \to E = (x \in (A, B) ⟼ Q)$
14		intlewftc.14	$⊢ (φ \land x \in (A, B)) \to P \leq Q$
15		intlewftc.15	$⊢ φ \to F (A) \leq G (A)$
16		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
17	4 16	syl	$⊢ φ \to F : [A, B] ⟶ ℝ$
18	2	leidd	$⊢ φ \to B \leq B$
19	2 3 18	3jca	$⊢ φ \to (B \in ℝ \land A \leq B \land B \leq B)$
20		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (B \in [A, B] \leftrightarrow (B \in ℝ \land A \leq B \land B \leq B))$
21	1 2 20	syl2anc	$⊢ φ \to (B \in [A, B] \leftrightarrow (B \in ℝ \land A \leq B \land B \leq B))$
22	19 21	mpbird	$⊢ φ \to B \in [A, B]$
23	17 22	ffvelrnd	$⊢ φ \to F (B) \in ℝ$
24	1	leidd	$⊢ φ \to A \leq A$
25	1 24 3	3jca	$⊢ φ \to (A \in ℝ \land A \leq A \land A \leq B)$
26		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (A \in [A, B] \leftrightarrow (A \in ℝ \land A \leq A \land A \leq B))$
27	1 2 26	syl2anc	$⊢ φ \to (A \in [A, B] \leftrightarrow (A \in ℝ \land A \leq A \land A \leq B))$
28	25 27	mpbird	$⊢ φ \to A \in [A, B]$
29	17 28	ffvelrnd	$⊢ φ \to F (A) \in ℝ$
30	23 29	resubcld	$⊢ φ \to F (B) - F (A) \in ℝ$
31		cncff	$⊢ G : [A, B] \underset{cn}{⟶} ℝ \to G : [A, B] ⟶ ℝ$
32	5 31	syl	$⊢ φ \to G : [A, B] ⟶ ℝ$
33	32 22	ffvelrnd	$⊢ φ \to G (B) \in ℝ$
34	32 28	ffvelrnd	$⊢ φ \to G (A) \in ℝ$
35	33 34	resubcld	$⊢ φ \to G (B) - G (A) \in ℝ$
36	12	eleq1d	$⊢ φ \to (D \in 𝐿^{1} \leftrightarrow (x \in (A, B) ⟼ P) \in 𝐿^{1})$
37	10 36	mpbid	$⊢ φ \to (x \in (A, B) ⟼ P) \in 𝐿^{1}$
38	13	eleq1d	$⊢ φ \to (E \in 𝐿^{1} \leftrightarrow (x \in (A, B) ⟼ Q) \in 𝐿^{1})$
39	11 38	mpbid	$⊢ φ \to (x \in (A, B) ⟼ Q) \in 𝐿^{1}$
40		cncff	$⊢ D : (A, B) \underset{cn}{⟶} ℝ \to D : (A, B) ⟶ ℝ$
41	8 40	syl	$⊢ φ \to D : (A, B) ⟶ ℝ$
42	12	feq1d	$⊢ φ \to (D : (A, B) ⟶ ℝ \leftrightarrow (x \in (A, B) ⟼ P) : (A, B) ⟶ ℝ)$
43	41 42	mpbid	$⊢ φ \to (x \in (A, B) ⟼ P) : (A, B) ⟶ ℝ$
44	43	fvmptelrn	$⊢ (φ \land x \in (A, B)) \to P \in ℝ$
45		cncff	$⊢ E : (A, B) \underset{cn}{⟶} ℝ \to E : (A, B) ⟶ ℝ$
46	9 45	syl	$⊢ φ \to E : (A, B) ⟶ ℝ$
47	13	feq1d	$⊢ φ \to (E : (A, B) ⟶ ℝ \leftrightarrow (x \in (A, B) ⟼ Q) : (A, B) ⟶ ℝ)$
48	46 47	mpbid	$⊢ φ \to (x \in (A, B) ⟼ Q) : (A, B) ⟶ ℝ$
49	48	fvmptelrn	$⊢ (φ \land x \in (A, B)) \to Q \in ℝ$
50	37 39 44 49 14	itgle	$⊢ φ \to \int_{(A, B)} P d x \leq \int_{(A, B)} Q d x$
51	44	itgmpt	$⊢ φ \to \int_{(A, B)} P d x = \int_{(A, B)} (x \in (A, B) ⟼ P) (t) d t$
52	12	fveq1d	$⊢ φ \to D (t) = (x \in (A, B) ⟼ P) (t)$
53	52	adantr	$⊢ (φ \land t \in (A, B)) \to D (t) = (x \in (A, B) ⟼ P) (t)$
54	53	eqcomd	$⊢ (φ \land t \in (A, B)) \to (x \in (A, B) ⟼ P) (t) = D (t)$
55	54	itgeq2dv	$⊢ φ \to \int_{(A, B)} (x \in (A, B) ⟼ P) (t) d t = \int_{(A, B)} D (t) d t$
56	6	adantr	$⊢ (φ \land t \in (A, B)) \to D = ℝ D F$
57	56	fveq1d	$⊢ (φ \land t \in (A, B)) \to D (t) = F_{ℝ}^{'} (t)$
58	57	itgeq2dv	$⊢ φ \to \int_{(A, B)} D (t) d t = \int_{(A, B)} F_{ℝ}^{'} (t) d t$
59		ax-resscn	$⊢ ℝ \subseteq ℂ$
60	59	a1i	$⊢ φ \to ℝ \subseteq ℂ$
61		fss	$⊢ (D : (A, B) ⟶ ℝ \land ℝ \subseteq ℂ) \to D : (A, B) ⟶ ℂ$
62	41 60 61	syl2anc	$⊢ φ \to D : (A, B) ⟶ ℂ$
63		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
64		cncffvrn	$⊢ (ℂ \subseteq ℂ \land D : (A, B) \underset{cn}{⟶} ℝ) \to (D : (A, B) \underset{cn}{⟶} ℂ \leftrightarrow D : (A, B) ⟶ ℂ)$
65	63 8 64	syl2anc	$⊢ φ \to (D : (A, B) \underset{cn}{⟶} ℂ \leftrightarrow D : (A, B) ⟶ ℂ)$
66	62 65	mpbird	$⊢ φ \to D : (A, B) \underset{cn}{⟶} ℂ$
67	6	eleq1d	$⊢ φ \to (D : (A, B) \underset{cn}{⟶} ℂ \leftrightarrow F_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ)$
68	66 67	mpbid	$⊢ φ \to F_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
69	6 10	eqeltrrd	$⊢ φ \to ℝ D F \in 𝐿^{1}$
70		fss	$⊢ (F : [A, B] ⟶ ℝ \land ℝ \subseteq ℂ) \to F : [A, B] ⟶ ℂ$
71	17 60 70	syl2anc	$⊢ φ \to F : [A, B] ⟶ ℂ$
72		cncffvrn	$⊢ (ℂ \subseteq ℂ \land F : [A, B] \underset{cn}{⟶} ℝ) \to (F : [A, B] \underset{cn}{⟶} ℂ \leftrightarrow F : [A, B] ⟶ ℂ)$
73	63 4 72	syl2anc	$⊢ φ \to (F : [A, B] \underset{cn}{⟶} ℂ \leftrightarrow F : [A, B] ⟶ ℂ)$
74	71 73	mpbird	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
75	1 2 3 68 69 74	ftc2	$⊢ φ \to \int_{(A, B)} F_{ℝ}^{'} (t) d t = F (B) - F (A)$
76	58 75	eqtrd	$⊢ φ \to \int_{(A, B)} D (t) d t = F (B) - F (A)$
77	55 76	eqtrd	$⊢ φ \to \int_{(A, B)} (x \in (A, B) ⟼ P) (t) d t = F (B) - F (A)$
78	51 77	eqtrd	$⊢ φ \to \int_{(A, B)} P d x = F (B) - F (A)$
79	49	itgmpt	$⊢ φ \to \int_{(A, B)} Q d x = \int_{(A, B)} (x \in (A, B) ⟼ Q) (t) d t$
80	13	adantr	$⊢ (φ \land t \in (A, B)) \to E = (x \in (A, B) ⟼ Q)$
81	80	eqcomd	$⊢ (φ \land t \in (A, B)) \to (x \in (A, B) ⟼ Q) = E$
82	81	fveq1d	$⊢ (φ \land t \in (A, B)) \to (x \in (A, B) ⟼ Q) (t) = E (t)$
83	82	itgeq2dv	$⊢ φ \to \int_{(A, B)} (x \in (A, B) ⟼ Q) (t) d t = \int_{(A, B)} E (t) d t$
84	79 83	eqtrd	$⊢ φ \to \int_{(A, B)} Q d x = \int_{(A, B)} E (t) d t$
85	7	adantr	$⊢ (φ \land t \in (A, B)) \to E = ℝ D G$
86	85	fveq1d	$⊢ (φ \land t \in (A, B)) \to E (t) = G_{ℝ}^{'} (t)$
87	86	itgeq2dv	$⊢ φ \to \int_{(A, B)} E (t) d t = \int_{(A, B)} G_{ℝ}^{'} (t) d t$
88		fss	$⊢ (E : (A, B) ⟶ ℝ \land ℝ \subseteq ℂ) \to E : (A, B) ⟶ ℂ$
89	46 60 88	syl2anc	$⊢ φ \to E : (A, B) ⟶ ℂ$
90		cncffvrn	$⊢ (ℂ \subseteq ℂ \land E : (A, B) \underset{cn}{⟶} ℝ) \to (E : (A, B) \underset{cn}{⟶} ℂ \leftrightarrow E : (A, B) ⟶ ℂ)$
91	63 9 90	syl2anc	$⊢ φ \to (E : (A, B) \underset{cn}{⟶} ℂ \leftrightarrow E : (A, B) ⟶ ℂ)$
92	89 91	mpbird	$⊢ φ \to E : (A, B) \underset{cn}{⟶} ℂ$
93	7	eleq1d	$⊢ φ \to (E : (A, B) \underset{cn}{⟶} ℂ \leftrightarrow G_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ)$
94	92 93	mpbid	$⊢ φ \to G_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
95	94 93	mpbird	$⊢ φ \to E : (A, B) \underset{cn}{⟶} ℂ$
96	95 93	mpbid	$⊢ φ \to G_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
97	7 11	eqeltrrd	$⊢ φ \to ℝ D G \in 𝐿^{1}$
98		fss	$⊢ (G : [A, B] ⟶ ℝ \land ℝ \subseteq ℂ) \to G : [A, B] ⟶ ℂ$
99	32 60 98	syl2anc	$⊢ φ \to G : [A, B] ⟶ ℂ$
100		cncffvrn	$⊢ (ℂ \subseteq ℂ \land G : [A, B] \underset{cn}{⟶} ℝ) \to (G : [A, B] \underset{cn}{⟶} ℂ \leftrightarrow G : [A, B] ⟶ ℂ)$
101	63 5 100	syl2anc	$⊢ φ \to (G : [A, B] \underset{cn}{⟶} ℂ \leftrightarrow G : [A, B] ⟶ ℂ)$
102	99 101	mpbird	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℂ$
103	1 2 3 96 97 102	ftc2	$⊢ φ \to \int_{(A, B)} G_{ℝ}^{'} (t) d t = G (B) - G (A)$
104	87 103	eqtrd	$⊢ φ \to \int_{(A, B)} E (t) d t = G (B) - G (A)$
105	84 104	eqtrd	$⊢ φ \to \int_{(A, B)} Q d x = G (B) - G (A)$
106	78 105	breq12d	$⊢ φ \to (\int_{(A, B)} P d x \leq \int_{(A, B)} Q d x \leftrightarrow F (B) - F (A) \leq G (B) - G (A))$
107	50 106	mpbid	$⊢ φ \to F (B) - F (A) \leq G (B) - G (A)$
108	30 29 35 34 107 15	le2addd	$⊢ φ \to F (B) - F (A) + F (A) \leq G (B) - G (A) + G (A)$
109	59 23	sselid	$⊢ φ \to F (B) \in ℂ$
110	59 29	sselid	$⊢ φ \to F (A) \in ℂ$
111	109 110	npcand	$⊢ φ \to F (B) - F (A) + F (A) = F (B)$
112	59 33	sselid	$⊢ φ \to G (B) \in ℂ$
113	59 34	sselid	$⊢ φ \to G (A) \in ℂ$
114	112 113	npcand	$⊢ φ \to G (B) - G (A) + G (A) = G (B)$
115	111 114	breq12d	$⊢ φ \to (F (B) - F (A) + F (A) \leq G (B) - G (A) + G (A) \leftrightarrow F (B) \leq G (B))$
116	108 115	mpbid	$⊢ φ \to F (B) \leq G (B)$

Metamath Proof Explorer

Theorem intlewftc

Proof