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 sseldi
 |-  ( ph -> ( F ` B ) e. CC )
110 59 29 sseldi
 |-  ( ph -> ( F ` A ) e. CC )
111 109 110 npcand
 |-  ( ph -> ( ( ( F ` B ) - ( F ` A ) ) + ( F ` A ) ) = ( F ` B ) )
112 59 33 sseldi
 |-  ( ph -> ( G ` B ) e. CC )
113 59 34 sseldi
 |-  ( 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 ) )