Metamath Proof Explorer


Theorem intlewftc

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

Ref Expression
Hypotheses intlewftc.1 φ A
intlewftc.2 φ B
intlewftc.3 φ A B
intlewftc.4 φ F : A B cn
intlewftc.5 φ G : A B cn
intlewftc.6 φ D = D F
intlewftc.7 φ E = D G
intlewftc.8 φ D : A B cn
intlewftc.9 φ E : A B cn
intlewftc.10 φ D 𝐿 1
intlewftc.11 φ E 𝐿 1
intlewftc.12 φ D = x A B P
intlewftc.13 φ E = x A B Q
intlewftc.14 φ x A B P Q
intlewftc.15 φ F A G A
Assertion intlewftc φ F B G B

Proof

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