Metamath Proof Explorer

Theorem itgle

Description: Monotonicity of an integral. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itgle.1 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
itgle.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
itgle.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
itgle.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
itgle.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
Assertion itgle ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ≤ ∫ 𝐴 𝐶 d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgle.1 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
2 itgle.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
3 itgle.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4 itgle.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
5 itgle.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
6 3 iblrelem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) ∈ ℝ ) ) )
7 1 6 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) ∈ ℝ ) )
8 7 simp2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) ∈ ℝ )
9 4 iblrelem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) ) ∈ ℝ ) ) )
10 2 9 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) ) ∈ ℝ ) )
11 10 simp3d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) ) ∈ ℝ )
12 10 simp2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ∈ ℝ )
13 7 simp3d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) ∈ ℝ )
14 3 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 𝐵 ∈ ℝ )
15 14 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 𝐵 ∈ ℝ* )
16 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ≤ 𝐵 )
17 elxrge0 ⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) ↔ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) )
18 15 16 17 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 𝐵 ∈ ( 0 [,] +∞ ) )
19 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
20 19 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ∈ ( 0 [,] +∞ ) )
21 18 20 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ∈ ( 0 [,] +∞ ) )
22 21 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
23 4 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) ) → 𝐶 ∈ ℝ )
24 23 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) ) → 𝐶 ∈ ℝ* )
25 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) ) → 0 ≤ 𝐶 )
26 elxrge0 ⊢ ( 𝐶 ∈ ( 0 [,] +∞ ) ↔ ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) )
27 24 25 26 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
28 19 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) ) → 0 ∈ ( 0 [,] +∞ ) )
29 27 28 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
30 29 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
31 0re ⊢ 0 ∈ ℝ
32 max1 ⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
33 31 4 32 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
34 ifcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
35 4 31 34 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
36 max2 ⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
37 31 4 36 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
38 3 4 35 5 37 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
39 maxle ⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ↔ ( 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∧ 𝐵 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
40 31 3 35 39 mp3an2i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ↔ ( 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∧ 𝐵 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
41 33 38 40 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
42 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
43 42 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
44 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 ) = if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 ) = if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
46 41 43 45 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 ) )
47 46 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 ) ) )
48 0le0 ⊢ 0 ≤ 0
49 48 a1i ⊢ ( ¬ 𝑥 ∈ 𝐴 → 0 ≤ 0 )
50 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 ) = 0 )
51 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 ) = 0 )
52 49 50 51 3brtr4d ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 ) )
53 47 52 pm2.61d1 ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 ) )
54 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 )
55 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 )
56 53 54 55 3brtr4g ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ≤ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) )
57 56 ralrimivw ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ≤ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) )
58 reex ⊢ ℝ ∈ V
59 58 a1i ⊢ ( 𝜑 → ℝ ∈ V )
60 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) )
61 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) )
62 59 21 29 60 61 ofrfval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ≤ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) )
63 57 62 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) )
64 itg2le ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) )
65 22 30 63 64 syl3anc ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) )
66 4 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐶 ∈ ℝ )
67 66 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) ) → - 𝐶 ∈ ℝ )
68 67 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) ) → - 𝐶 ∈ ℝ* )
69 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) ) → 0 ≤ - 𝐶 )
70 elxrge0 ⊢ ( - 𝐶 ∈ ( 0 [,] +∞ ) ↔ ( - 𝐶 ∈ ℝ* ∧ 0 ≤ - 𝐶 ) )
71 68 69 70 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) ) → - 𝐶 ∈ ( 0 [,] +∞ ) )
72 19 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) ) → 0 ∈ ( 0 [,] +∞ ) )
73 71 72 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
74 73 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
75 3 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
76 75 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) ) → - 𝐵 ∈ ℝ )
77 76 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) ) → - 𝐵 ∈ ℝ* )
78 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) ) → 0 ≤ - 𝐵 )
79 elxrge0 ⊢ ( - 𝐵 ∈ ( 0 [,] +∞ ) ↔ ( - 𝐵 ∈ ℝ* ∧ 0 ≤ - 𝐵 ) )
80 77 78 79 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) ) → - 𝐵 ∈ ( 0 [,] +∞ ) )
81 19 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) ) → 0 ∈ ( 0 [,] +∞ ) )
82 80 81 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ∈ ( 0 [,] +∞ ) )
83 82 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
84 max1 ⊢ ( ( 0 ∈ ℝ ∧ - 𝐵 ∈ ℝ ) → 0 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
85 31 75 84 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
86 ifcl ⊢ ( ( - 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ )
87 75 31 86 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ )
88 3 4 lenegd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≤ 𝐶 ↔ - 𝐶 ≤ - 𝐵 ) )
89 5 88 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐶 ≤ - 𝐵 )
90 max2 ⊢ ( ( 0 ∈ ℝ ∧ - 𝐵 ∈ ℝ ) → - 𝐵 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
91 31 75 90 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
92 66 75 87 89 91 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐶 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
93 maxle ⊢ ( ( 0 ∈ ℝ ∧ - 𝐶 ∈ ℝ ∧ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ↔ ( 0 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∧ - 𝐶 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
94 31 66 87 93 mp3an2i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ↔ ( 0 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∧ - 𝐶 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
95 85 92 94 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
96 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) , 0 ) = if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
97 96 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) , 0 ) = if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
98 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) , 0 ) = if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
99 98 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) , 0 ) = if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
100 95 97 99 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) , 0 ) )
101 100 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) , 0 ) ) )
102 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) , 0 ) = 0 )
103 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) , 0 ) = 0 )
104 49 102 103 3brtr4d ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) , 0 ) )
105 101 104 pm2.61d1 ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) , 0 ) )
106 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) , 0 )
107 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) , 0 )
108 105 106 107 3brtr4g ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ≤ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) )
109 108 ralrimivw ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ≤ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) )
110 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) )
111 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) )
112 59 73 82 110 111 ofrfval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ≤ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) )
113 109 112 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) )
114 itg2le ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) )
115 74 83 113 114 syl3anc ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) )
116 8 11 12 13 65 115 le2subd ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) − ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) ) ≤ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) − ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) ) ) )
117 3 1 itgrevallem1 ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) − ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) ) )
118 4 2 itgrevallem1 ⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) − ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐶 ) , - 𝐶 , 0 ) ) ) ) )
119 116 117 118 3brtr4d ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ≤ ∫ 𝐴 𝐶 d 𝑥 )