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 
|- ( ph -> A e. RR )
intlewftc.2 
|- ( ph -> B e. RR )
intlewftc.3 
|- ( ph -> A <_ B )
intlewftc.4 
|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
intlewftc.5 
|- ( ph -> G e. ( ( A [,] B ) -cn-> RR ) )
intlewftc.6 
|- ( ph -> D = ( RR _D F ) )
intlewftc.7 
|- ( ph -> E = ( RR _D G ) )
intlewftc.8 
|- ( ph -> D e. ( ( A (,) B ) -cn-> RR ) )
intlewftc.9 
|- ( ph -> E e. ( ( A (,) B ) -cn-> RR ) )
intlewftc.10 
|- ( ph -> D e. L^1 )
intlewftc.11 
|- ( ph -> E e. L^1 )
intlewftc.12 
|- ( ph -> D = ( x e. ( A (,) B ) |-> P ) )
intlewftc.13 
|- ( ph -> E = ( x e. ( A (,) B ) |-> Q ) )
intlewftc.14 
|- ( ( ph /\ x e. ( A (,) B ) ) -> P <_ Q )
intlewftc.15 
|- ( ph -> ( F ` A ) <_ ( G ` A ) )
Assertion intlewftc 
|- ( ph -> ( F ` B ) <_ ( G ` B ) )

Proof

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