This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ibladdlem

Description: Lemma for ibladd . (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses ibladd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
ibladd.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
ibladd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 = ( 𝐵 + 𝐶 ) )
ibladd.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
ibladd.5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
ibladd.6 ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) ∈ ℝ )
ibladd.7 ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ∈ ℝ )
Assertion ibladdlem ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 ibladd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
2 ibladd.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
3 ibladd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 = ( 𝐵 + 𝐶 ) )
4 ibladd.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
5 ibladd.5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
6 ibladd.6 ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) ∈ ℝ )
7 ibladd.7 ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ∈ ℝ )
8 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 )
9 1 2 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
10 3 9 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ ℝ )
11 0re ⊢ 0 ∈ ℝ
12 ifcl ⊢ ( ( 𝐷 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ∈ ℝ )
13 10 11 12 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ∈ ℝ )
14 13 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ∈ ℝ* )
15 max1 ⊢ ( ( 0 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐷 , 𝐷 , 0 ) )
16 11 10 15 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ 𝐷 , 𝐷 , 0 ) )
17 elxrge0 ⊢ ( if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ∈ ( 0 [,] +∞ ) ↔ ( if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ∈ ℝ* ∧ 0 ≤ if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ) )
18 14 16 17 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ∈ ( 0 [,] +∞ ) )
19 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
20 19 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,] +∞ ) )
21 18 20 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) ∈ ( 0 [,] +∞ ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) ∈ ( 0 [,] +∞ ) )
23 8 22 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ∈ ( 0 [,] +∞ ) )
24 23 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
25 reex ⊢ ℝ ∈ V
26 25 a1i ⊢ ( 𝜑 → ℝ ∈ V )
27 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 )
28 ifcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
29 1 11 28 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
30 11 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ℝ )
31 29 30 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 ) ∈ ℝ )
32 27 31 eqeltrid ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ∈ ℝ )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ∈ ℝ )
34 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 )
35 ifcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
36 2 11 35 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
37 36 30 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 ) ∈ ℝ )
38 34 37 eqeltrid ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ∈ ℝ )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ∈ ℝ )
40 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) )
41 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) )
42 26 33 39 40 41 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) )
43 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
44 ibar ⊢ ( 𝑥 ∈ 𝐴 → ( 0 ≤ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) ) )
45 44 ifbid ⊢ ( 𝑥 ∈ 𝐴 → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) )
46 ibar ⊢ ( 𝑥 ∈ 𝐴 → ( 0 ≤ 𝐶 ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) ) )
47 46 ifbid ⊢ ( 𝑥 ∈ 𝐴 → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) )
48 45 47 oveq12d ⊢ ( 𝑥 ∈ 𝐴 → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) )
49 43 48 eqtr2d ⊢ ( 𝑥 ∈ 𝐴 → ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
50 00id ⊢ ( 0 + 0 ) = 0
51 simpl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) → 𝑥 ∈ 𝐴 )
52 51 con3i ⊢ ( ¬ 𝑥 ∈ 𝐴 → ¬ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) )
53 52 iffalsed ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) = 0 )
54 simpl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) → 𝑥 ∈ 𝐴 )
55 54 con3i ⊢ ( ¬ 𝑥 ∈ 𝐴 → ¬ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) )
56 55 iffalsed ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) = 0 )
57 53 56 oveq12d ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) = ( 0 + 0 ) )
58 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) = 0 )
59 50 57 58 3eqtr4a ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
60 49 59 pm2.61i ⊢ ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 )
61 60 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ ( if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) + if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
62 42 61 eqtrdi ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) )
63 62 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) )
64 4 1 mbfdm2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
65 mblss ⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
66 64 65 syl ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
67 rembl ⊢ ℝ ∈ dom vol
68 67 a1i ⊢ ( 𝜑 → ℝ ∈ dom vol )
69 32 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ∈ ℝ )
70 eldifn ⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
71 70 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ¬ 𝑥 ∈ 𝐴 )
72 71 intnanrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ¬ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) )
73 72 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) = 0 )
74 45 mpteq2ia ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) )
75 1 4 mbfpos ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn )
76 74 75 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∈ MblFn )
77 66 68 69 73 76 mbfss ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∈ MblFn )
78 max1 ⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
79 11 1 78 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
80 elrege0 ⊢ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) )
81 29 79 80 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
82 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
83 82 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,) +∞ ) )
84 81 83 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐵 , 𝐵 , 0 ) , 0 ) ∈ ( 0 [,) +∞ ) )
85 27 84 eqeltrid ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
86 85 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
87 86 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
88 38 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ∈ ℝ )
89 71 56 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) = 0 )
90 47 mpteq2ia ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) )
91 2 5 mbfpos ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ MblFn )
92 90 91 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ∈ MblFn )
93 66 68 88 89 92 mbfss ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ∈ MblFn )
94 max1 ⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
95 11 2 94 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
96 elrege0 ⊢ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
97 36 95 96 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ( 0 [,) +∞ ) )
98 97 83 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐶 , 𝐶 , 0 ) , 0 ) ∈ ( 0 [,) +∞ ) )
99 34 98 eqeltrid ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ∈ ( 0 [,) +∞ ) )
100 99 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ∈ ( 0 [,) +∞ ) )
101 100 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
102 77 87 6 93 101 7 itg2add ⊢ ( 𝜑 → ( ∫2 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ) )
103 63 102 eqtr3d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ) )
104 6 7 readdcld ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) ) ) ) ∈ ℝ )
105 103 104 eqeltrd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) ∈ ℝ )
106 29 36 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ℝ )
107 106 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ℝ* )
108 29 36 79 95 addge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
109 elxrge0 ⊢ ( ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ℝ* ∧ 0 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
110 107 108 109 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ( 0 [,] +∞ ) )
111 110 20 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
112 111 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
113 112 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
114 max2 ⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
115 11 1 114 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
116 max2 ⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
117 11 2 116 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
118 1 2 29 36 115 117 le2addd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
119 3 118 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
120 breq1 ⊢ ( 𝐷 = if ( 0 ≤ 𝐷 , 𝐷 , 0 ) → ( 𝐷 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ↔ if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
121 breq1 ⊢ ( 0 = if ( 0 ≤ 𝐷 , 𝐷 , 0 ) → ( 0 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ↔ if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
122 120 121 ifboth ⊢ ( ( 𝐷 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∧ 0 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) → if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
123 119 108 122 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐷 , 𝐷 , 0 ) ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
124 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) = if ( 0 ≤ 𝐷 , 𝐷 , 0 ) )
125 124 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) = if ( 0 ≤ 𝐷 , 𝐷 , 0 ) )
126 43 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
127 123 125 126 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
128 127 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) )
129 0le0 ⊢ 0 ≤ 0
130 129 a1i ⊢ ( ¬ 𝑥 ∈ 𝐴 → 0 ≤ 0 )
131 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) = 0 )
132 130 131 58 3brtr4d ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
133 128 132 pm2.61d1 ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝐷 , 𝐷 , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
134 8 133 eqbrtrid ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
135 134 ralrimivw ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) )
136 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) )
137 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) )
138 26 23 112 136 137 ofrfval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) )
139 135 138 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) )
140 itg2le ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) )
141 24 113 139 140 syl3anc ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) )
142 itg2lecl ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ) ∈ ℝ )
143 24 105 141 142 syl3anc ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷 ) , 𝐷 , 0 ) ) ) ∈ ℝ )