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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
intlewftc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
intlewftc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
intlewftc.4 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
intlewftc.5 ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
intlewftc.6 ⊢ ( 𝜑 → 𝐷 = ( ℝ D 𝐹 ) )
intlewftc.7 ⊢ ( 𝜑 → 𝐸 = ( ℝ D 𝐺 ) )
intlewftc.8 ⊢ ( 𝜑 → 𝐷 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
intlewftc.9 ⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
intlewftc.10 ⊢ ( 𝜑 → 𝐷 ∈ 𝐿1 )
intlewftc.11 ⊢ ( 𝜑 → 𝐸 ∈ 𝐿1 )
intlewftc.12 ⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑃 ) )
intlewftc.13 ⊢ ( 𝜑 → 𝐸 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑄 ) )
intlewftc.14 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑃 ≤ 𝑄 )
intlewftc.15 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝐴 ) )
Assertion intlewftc ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐺 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 intlewftc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 intlewftc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 intlewftc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 intlewftc.4 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
5 intlewftc.5 ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
6 intlewftc.6 ⊢ ( 𝜑 → 𝐷 = ( ℝ D 𝐹 ) )
7 intlewftc.7 ⊢ ( 𝜑 → 𝐸 = ( ℝ D 𝐺 ) )
8 intlewftc.8 ⊢ ( 𝜑 → 𝐷 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
9 intlewftc.9 ⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
10 intlewftc.10 ⊢ ( 𝜑 → 𝐷 ∈ 𝐿1 )
11 intlewftc.11 ⊢ ( 𝜑 → 𝐸 ∈ 𝐿1 )
12 intlewftc.12 ⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑃 ) )
13 intlewftc.13 ⊢ ( 𝜑 → 𝐸 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑄 ) )
14 intlewftc.14 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑃 ≤ 𝑄 )
15 intlewftc.15 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝐴 ) )
16 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
17 4 16 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
18 2 leidd ⊢ ( 𝜑 → 𝐵 ≤ 𝐵 )
19 2 3 18 3jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵 ) )
20 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵 ) ) )
21 1 2 20 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵 ) ) )
22 19 21 mpbird ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
23 17 22 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
24 1 leidd ⊢ ( 𝜑 → 𝐴 ≤ 𝐴 )
25 1 24 3 3jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) )
26 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) )
27 1 2 26 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) )
28 25 27 mpbird ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
29 17 28 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
30 23 29 resubcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ )
31 cncff ⊢ ( 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
32 5 31 syl ⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
33 32 22 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐵 ) ∈ ℝ )
34 32 28 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) ∈ ℝ )
35 33 34 resubcld ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ )
36 12 eleq1d ⊢ ( 𝜑 → ( 𝐷 ∈ 𝐿1 ↔ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑃 ) ∈ 𝐿1 ) )
37 10 36 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑃 ) ∈ 𝐿1 )
38 13 eleq1d ⊢ ( 𝜑 → ( 𝐸 ∈ 𝐿1 ↔ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑄 ) ∈ 𝐿1 ) )
39 11 38 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑄 ) ∈ 𝐿1 )
40 cncff ⊢ ( 𝐷 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) → 𝐷 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
41 8 40 syl ⊢ ( 𝜑 → 𝐷 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
42 12 feq1d ⊢ ( 𝜑 → ( 𝐷 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ↔ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑃 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
43 41 42 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑃 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
44 43 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑃 ∈ ℝ )
45 cncff ⊢ ( 𝐸 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) → 𝐸 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
46 9 45 syl ⊢ ( 𝜑 → 𝐸 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
47 13 feq1d ⊢ ( 𝜑 → ( 𝐸 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ↔ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑄 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
48 46 47 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑄 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
49 48 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑄 ∈ ℝ )
50 37 39 44 49 14 itgle ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝑃 d 𝑥 ≤ ∫ ( 𝐴 (,) 𝐵 ) 𝑄 d 𝑥 )
51 44 itgmpt ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝑃 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑃 ) ‘ 𝑡 ) d 𝑡 )
52 12 fveq1d ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑡 ) = ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑃 ) ‘ 𝑡 ) )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐷 ‘ 𝑡 ) = ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑃 ) ‘ 𝑡 ) )
54 53 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑃 ) ‘ 𝑡 ) = ( 𝐷 ‘ 𝑡 ) )
55 54 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑃 ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐷 ‘ 𝑡 ) d 𝑡 )
56 6 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐷 = ( ℝ D 𝐹 ) )
57 56 fveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐷 ‘ 𝑡 ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
58 57 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐷 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
59 ax-resscn ⊢ ℝ ⊆ ℂ
60 59 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
61 fss ⊢ ( ( 𝐷 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐷 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
62 41 60 61 syl2anc ⊢ ( 𝜑 → 𝐷 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
63 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
64 cncffvrn ⊢ ( ( ℂ ⊆ ℂ ∧ 𝐷 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ) → ( 𝐷 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ↔ 𝐷 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
65 63 8 64 syl2anc ⊢ ( 𝜑 → ( 𝐷 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ↔ 𝐷 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
66 62 65 mpbird ⊢ ( 𝜑 → 𝐷 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
67 6 eleq1d ⊢ ( 𝜑 → ( 𝐷 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ↔ ( ℝ D 𝐹 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) )
68 66 67 mpbid ⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
69 6 10 eqeltrrd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ 𝐿1 )
70 fss ⊢ ( ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
71 17 60 70 syl2anc ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
72 cncffvrn ⊢ ( ( ℂ ⊆ ℂ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ) → ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ↔ 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ) )
73 63 4 72 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ↔ 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ) )
74 71 73 mpbird ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
75 1 2 3 68 69 74 ftc2 ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
76 58 75 eqtrd ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐷 ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
77 55 76 eqtrd ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑃 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
78 51 77 eqtrd ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝑃 d 𝑥 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
79 49 itgmpt ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝑄 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑄 ) ‘ 𝑡 ) d 𝑡 )
80 13 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐸 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑄 ) )
81 80 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑄 ) = 𝐸 )
82 81 fveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑄 ) ‘ 𝑡 ) = ( 𝐸 ‘ 𝑡 ) )
83 82 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑄 ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐸 ‘ 𝑡 ) d 𝑡 )
84 79 83 eqtrd ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝑄 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐸 ‘ 𝑡 ) d 𝑡 )
85 7 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐸 = ( ℝ D 𝐺 ) )
86 85 fveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐸 ‘ 𝑡 ) = ( ( ℝ D 𝐺 ) ‘ 𝑡 ) )
87 86 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐸 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐺 ) ‘ 𝑡 ) d 𝑡 )
88 fss ⊢ ( ( 𝐸 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐸 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
89 46 60 88 syl2anc ⊢ ( 𝜑 → 𝐸 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
90 cncffvrn ⊢ ( ( ℂ ⊆ ℂ ∧ 𝐸 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ) → ( 𝐸 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ↔ 𝐸 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
91 63 9 90 syl2anc ⊢ ( 𝜑 → ( 𝐸 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ↔ 𝐸 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
92 89 91 mpbird ⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
93 7 eleq1d ⊢ ( 𝜑 → ( 𝐸 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ↔ ( ℝ D 𝐺 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) )
94 92 93 mpbid ⊢ ( 𝜑 → ( ℝ D 𝐺 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
95 94 93 mpbird ⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
96 95 93 mpbid ⊢ ( 𝜑 → ( ℝ D 𝐺 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
97 7 11 eqeltrrd ⊢ ( 𝜑 → ( ℝ D 𝐺 ) ∈ 𝐿1 )
98 fss ⊢ ( ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
99 32 60 98 syl2anc ⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
100 cncffvrn ⊢ ( ( ℂ ⊆ ℂ ∧ 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ) → ( 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ↔ 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ) )
101 63 5 100 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ↔ 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ) )
102 99 101 mpbird ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
103 1 2 3 96 97 102 ftc2 ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐺 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) )
104 87 103 eqtrd ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐸 ‘ 𝑡 ) d 𝑡 = ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) )
105 84 104 eqtrd ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝑄 d 𝑥 = ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) )
106 78 105 breq12d ⊢ ( 𝜑 → ( ∫ ( 𝐴 (,) 𝐵 ) 𝑃 d 𝑥 ≤ ∫ ( 𝐴 (,) 𝐵 ) 𝑄 d 𝑥 ↔ ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ≤ ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ) )
107 50 106 mpbid ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ≤ ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) )
108 30 29 35 34 107 15 le2addd ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) + ( 𝐹 ‘ 𝐴 ) ) ≤ ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) + ( 𝐺 ‘ 𝐴 ) ) )
109 59 23 sselid ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
110 59 29 sselid ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
111 109 110 npcand ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) + ( 𝐹 ‘ 𝐴 ) ) = ( 𝐹 ‘ 𝐵 ) )
112 59 33 sselid ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐵 ) ∈ ℂ )
113 59 34 sselid ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) ∈ ℂ )
114 112 113 npcand ⊢ ( 𝜑 → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) + ( 𝐺 ‘ 𝐴 ) ) = ( 𝐺 ‘ 𝐵 ) )
115 111 114 breq12d ⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) + ( 𝐹 ‘ 𝐴 ) ) ≤ ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) + ( 𝐺 ‘ 𝐴 ) ) ↔ ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐺 ‘ 𝐵 ) ) )
116 108 115 mpbid ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐺 ‘ 𝐵 ) )