Metamath Proof Explorer

Theorem itg2split

Description: The S.2 integral splits under an almost disjoint union. The proof avoids the use of itg2add , which requires countable choice. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itg2split.a ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
itg2split.b ⊢ ( 𝜑 → 𝐵 ∈ dom vol )
itg2split.i ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = 0 )
itg2split.u ⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
itg2split.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
itg2split.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
itg2split.g ⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
itg2split.h ⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
itg2split.sf ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
itg2split.sg ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) ∈ ℝ )
Assertion itg2split ( 𝜑 → ( ∫2 ‘ 𝐻 ) = ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 itg2split.a ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
2 itg2split.b ⊢ ( 𝜑 → 𝐵 ∈ dom vol )
3 itg2split.i ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = 0 )
4 itg2split.u ⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
5 itg2split.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
6 itg2split.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
7 itg2split.g ⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
8 itg2split.h ⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
9 itg2split.sf ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
10 itg2split.sg ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) ∈ ℝ )
11 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ 𝑈 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
12 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
13 12 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ 𝑈 ) → 0 ∈ ( 0 [,] +∞ ) )
14 11 13 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
15 14 8 fmptd ⊢ ( 𝜑 → 𝐻 : ℝ ⟶ ( 0 [,] +∞ ) )
16 itg2cl ⊢ ( 𝐻 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐻 ) ∈ ℝ* )
17 15 16 syl ⊢ ( 𝜑 → ( ∫2 ‘ 𝐻 ) ∈ ℝ* )
18 9 10 readdcld ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) ∈ ℝ )
19 18 rexrd ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) ∈ ℝ* )
20 1 2 3 4 5 6 7 8 9 10 itg2splitlem ⊢ ( 𝜑 → ( ∫2 ‘ 𝐻 ) ≤ ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) )
21 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ∫2 ‘ 𝐺 ) ∈ ℝ )
22 itg2lecl ⊢ ( ( 𝐻 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) ∈ ℝ ∧ ( ∫2 ‘ 𝐻 ) ≤ ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) ) → ( ∫2 ‘ 𝐻 ) ∈ ℝ )
23 15 18 20 22 syl3anc ⊢ ( 𝜑 → ( ∫2 ‘ 𝐻 ) ∈ ℝ )
24 23 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ∫2 ‘ 𝐻 ) ∈ ℝ )
25 itg1cl ⊢ ( 𝑓 ∈ dom ∫1 → ( ∫1 ‘ 𝑓 ) ∈ ℝ )
26 25 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ∫1 ‘ 𝑓 ) ∈ ℝ )
27 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → 𝑓 ∈ dom ∫1 )
28 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → 𝑔 ∈ dom ∫1 )
29 27 28 itg1add ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ∫1 ‘ ( 𝑓 ∘f + 𝑔 ) ) = ( ( ∫1 ‘ 𝑓 ) + ( ∫1 ‘ 𝑔 ) ) )
30 15 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → 𝐻 : ℝ ⟶ ( 0 [,] +∞ ) )
31 27 28 i1fadd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( 𝑓 ∘f + 𝑔 ) ∈ dom ∫1 )
32 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
33 mblss ⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
34 1 33 syl ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
35 32 34 sstrid ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ ℝ )
36 35 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ ℝ )
37 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = 0 )
38 nfv ⊢ Ⅎ 𝑥 𝜑
39 nfv ⊢ Ⅎ 𝑥 𝑓 ∈ dom ∫1
40 nfcv ⊢ Ⅎ 𝑥 𝑓
41 nfcv ⊢ Ⅎ 𝑥 ∘r ≤
42 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
43 6 42 nfcxfr ⊢ Ⅎ 𝑥 𝐹
44 40 41 43 nfbr ⊢ Ⅎ 𝑥 𝑓 ∘r ≤ 𝐹
45 39 44 nfan ⊢ Ⅎ 𝑥 ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 )
46 nfv ⊢ Ⅎ 𝑥 𝑔 ∈ dom ∫1
47 nfcv ⊢ Ⅎ 𝑥 𝑔
48 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
49 7 48 nfcxfr ⊢ Ⅎ 𝑥 𝐺
50 47 41 49 nfbr ⊢ Ⅎ 𝑥 𝑔 ∘r ≤ 𝐺
51 46 50 nfan ⊢ Ⅎ 𝑥 ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 )
52 45 51 nfan ⊢ Ⅎ 𝑥 ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) )
53 38 52 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) )
54 eldifi ⊢ ( 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) → 𝑥 ∈ ℝ )
55 i1ff ⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 : ℝ ⟶ ℝ )
56 27 55 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → 𝑓 : ℝ ⟶ ℝ )
57 56 ffnd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → 𝑓 Fn ℝ )
58 i1ff ⊢ ( 𝑔 ∈ dom ∫1 → 𝑔 : ℝ ⟶ ℝ )
59 28 58 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → 𝑔 : ℝ ⟶ ℝ )
60 59 ffnd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → 𝑔 Fn ℝ )
61 reex ⊢ ℝ ∈ V
62 61 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ℝ ∈ V )
63 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
64 eqidd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
65 eqidd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) )
66 57 60 62 62 63 64 65 ofval ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) )
67 54 66 sylan2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) )
68 ffvelrn ⊢ ( ( 𝑓 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
69 56 54 68 syl2an ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
70 ffvelrn ⊢ ( ( 𝑔 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑔 ‘ 𝑥 ) ∈ ℝ )
71 59 54 70 syl2an ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑔 ‘ 𝑥 ) ∈ ℝ )
72 69 71 readdcld ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ )
73 72 rexrd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* )
74 73 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* )
75 69 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
76 75 rexrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ* )
77 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
78 ffvelrn ⊢ ( ( 𝐻 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐻 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
79 30 54 78 syl2an ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
80 77 79 sselid ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ℝ* )
81 80 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ ℝ* )
82 71 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ ℝ )
83 0red ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 0 ∈ ℝ )
84 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → 𝑔 ∘r ≤ 𝐺 )
85 61 a1i ⊢ ( ( 𝜑 ∧ 𝑔 Fn ℝ ) → ℝ ∈ V )
86 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑔 ‘ 𝑥 ) ∈ V )
87 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
88 87 4 sseqtrrid ⊢ ( 𝜑 → 𝐵 ⊆ 𝑈 )
89 88 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝑈 )
90 89 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝑈 )
91 90 11 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
92 12 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ 𝐵 ) → 0 ∈ ( 0 [,] +∞ ) )
93 91 92 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
94 93 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℝ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
95 simpr ⊢ ( ( 𝜑 ∧ 𝑔 Fn ℝ ) → 𝑔 Fn ℝ )
96 dffn5 ⊢ ( 𝑔 Fn ℝ ↔ 𝑔 = ( 𝑥 ∈ ℝ ↦ ( 𝑔 ‘ 𝑥 ) ) )
97 95 96 sylib ⊢ ( ( 𝜑 ∧ 𝑔 Fn ℝ ) → 𝑔 = ( 𝑥 ∈ ℝ ↦ ( 𝑔 ‘ 𝑥 ) ) )
98 7 a1i ⊢ ( ( 𝜑 ∧ 𝑔 Fn ℝ ) → 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) ) )
99 85 86 94 97 98 ofrfval2 ⊢ ( ( 𝜑 ∧ 𝑔 Fn ℝ ) → ( 𝑔 ∘r ≤ 𝐺 ↔ ∀ 𝑥 ∈ ℝ ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) ) )
100 60 99 syldan ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( 𝑔 ∘r ≤ 𝐺 ↔ ∀ 𝑥 ∈ ℝ ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) ) )
101 84 100 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ∀ 𝑥 ∈ ℝ ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
102 101 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
103 54 102 sylan2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
104 103 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
105 eldifn ⊢ ( 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) → ¬ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
106 105 adantl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ¬ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
107 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
108 106 107 sylnib ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
109 imnan ⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
110 108 109 sylibr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
111 110 imp ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 ∈ 𝐵 )
112 111 iffalsed ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) = 0 )
113 104 112 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ≤ 0 )
114 82 83 75 113 leadd2dd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + 0 ) )
115 75 recnd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℂ )
116 115 addid1d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + 0 ) = ( 𝑓 ‘ 𝑥 ) )
117 114 116 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( 𝑓 ‘ 𝑥 ) )
118 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → 𝑓 ∘r ≤ 𝐹 )
119 61 a1i ⊢ ( ( 𝜑 ∧ 𝑓 Fn ℝ ) → ℝ ∈ V )
120 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑓 Fn ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) ∈ V )
121 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
122 121 4 sseqtrrid ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
123 122 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝑈 )
124 123 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝑈 )
125 124 11 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
126 12 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,] +∞ ) )
127 125 126 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
128 127 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 Fn ℝ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
129 simpr ⊢ ( ( 𝜑 ∧ 𝑓 Fn ℝ ) → 𝑓 Fn ℝ )
130 dffn5 ⊢ ( 𝑓 Fn ℝ ↔ 𝑓 = ( 𝑥 ∈ ℝ ↦ ( 𝑓 ‘ 𝑥 ) ) )
131 129 130 sylib ⊢ ( ( 𝜑 ∧ 𝑓 Fn ℝ ) → 𝑓 = ( 𝑥 ∈ ℝ ↦ ( 𝑓 ‘ 𝑥 ) ) )
132 6 a1i ⊢ ( ( 𝜑 ∧ 𝑓 Fn ℝ ) → 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) )
133 119 120 128 131 132 ofrfval2 ⊢ ( ( 𝜑 ∧ 𝑓 Fn ℝ ) → ( 𝑓 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) )
134 57 133 syldan ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( 𝑓 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) )
135 118 134 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ∀ 𝑥 ∈ ℝ ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
136 135 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
137 54 136 sylan2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
138 137 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
139 122 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → 𝐴 ⊆ 𝑈 )
140 139 sselda ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝑈 )
141 140 iftrued ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) = 𝐶 )
142 simpr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
143 14 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
144 8 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
145 142 143 144 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
146 54 145 sylan2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
147 146 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
148 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
149 148 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
150 141 147 149 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
151 138 150 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) )
152 74 76 81 117 151 xrletrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( 𝐻 ‘ 𝑥 ) )
153 73 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* )
154 71 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ ℝ )
155 154 rexrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ ℝ* )
156 80 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ ℝ* )
157 69 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
158 0red ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ℝ )
159 137 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
160 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 0 )
161 160 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 0 )
162 159 161 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ≤ 0 )
163 157 158 154 162 leadd1dd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( 0 + ( 𝑔 ‘ 𝑥 ) ) )
164 154 recnd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ ℂ )
165 164 addid2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 0 + ( 𝑔 ‘ 𝑥 ) ) = ( 𝑔 ‘ 𝑥 ) )
166 163 165 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( 𝑔 ‘ 𝑥 ) )
167 103 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
168 146 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
169 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
170 169 eleq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑈 ↔ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ) )
171 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
172 biorf ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ) )
173 171 172 bitr4id ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ 𝐵 ) )
174 173 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ 𝐵 ) )
175 170 174 bitrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑈 ↔ 𝑥 ∈ 𝐵 ) )
176 175 ifbid ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) = if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
177 168 176 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
178 167 177 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) )
179 153 155 156 166 178 xrletrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( 𝐻 ‘ 𝑥 ) )
180 152 179 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( 𝐻 ‘ 𝑥 ) )
181 67 180 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) )
182 181 ex ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) ) )
183 53 182 ralrimi ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ∀ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) )
184 nfv ⊢ Ⅎ 𝑦 ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 )
185 nfcv ⊢ Ⅎ 𝑥 ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 )
186 nfcv ⊢ Ⅎ 𝑥 ≤
187 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
188 8 187 nfcxfr ⊢ Ⅎ 𝑥 𝐻
189 nfcv ⊢ Ⅎ 𝑥 𝑦
190 188 189 nffv ⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑦 )
191 185 186 190 nfbr ⊢ Ⅎ 𝑥 ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 ) ≤ ( 𝐻 ‘ 𝑦 )
192 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) = ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 ) )
193 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑦 ) )
194 192 193 breq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) ↔ ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 ) ≤ ( 𝐻 ‘ 𝑦 ) ) )
195 184 191 194 cbvralw ⊢ ( ∀ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 ) ≤ ( 𝐻 ‘ 𝑦 ) )
196 183 195 sylib ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ∀ 𝑦 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 ) ≤ ( 𝐻 ‘ 𝑦 ) )
197 196 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 ) ≤ ( 𝐻 ‘ 𝑦 ) )
198 30 31 36 37 197 itg2uba ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ∫1 ‘ ( 𝑓 ∘f + 𝑔 ) ) ≤ ( ∫2 ‘ 𝐻 ) )
199 29 198 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ( ∫1 ‘ 𝑓 ) + ( ∫1 ‘ 𝑔 ) ) ≤ ( ∫2 ‘ 𝐻 ) )
200 26 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ∫1 ‘ 𝑓 ) ∈ ℝ )
201 itg1cl ⊢ ( 𝑔 ∈ dom ∫1 → ( ∫1 ‘ 𝑔 ) ∈ ℝ )
202 28 201 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ∫1 ‘ 𝑔 ) ∈ ℝ )
203 23 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ∫2 ‘ 𝐻 ) ∈ ℝ )
204 200 202 203 leaddsub2d ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ( ( ∫1 ‘ 𝑓 ) + ( ∫1 ‘ 𝑔 ) ) ≤ ( ∫2 ‘ 𝐻 ) ↔ ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ) )
205 199 204 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) )
206 205 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) → ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) )
207 206 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑔 ∘r ≤ 𝐺 → ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ) )
208 207 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐺 → ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ) )
209 93 7 fmptd ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
210 209 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
211 24 26 resubcld ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ∈ ℝ )
212 211 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ∈ ℝ* )
213 itg2leub ⊢ ( ( 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ∈ ℝ* ) → ( ( ∫2 ‘ 𝐺 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐺 → ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ) ) )
214 210 212 213 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ( ∫2 ‘ 𝐺 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐺 → ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ) ) )
215 208 214 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ∫2 ‘ 𝐺 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) )
216 21 24 26 215 lesubd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ∫1 ‘ 𝑓 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) )
217 216 expr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ) )
218 217 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ) )
219 127 6 fmptd ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
220 23 10 resubcld ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ∈ ℝ )
221 220 rexrd ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ∈ ℝ* )
222 itg2leub ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ∈ ℝ* ) → ( ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ) ) )
223 219 221 222 syl2anc ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ) ) )
224 218 223 mpbird ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) )
225 leaddsub ⊢ ( ( ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ 𝐺 ) ∈ ℝ ∧ ( ∫2 ‘ 𝐻 ) ∈ ℝ ) → ( ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) ≤ ( ∫2 ‘ 𝐻 ) ↔ ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ) )
226 9 10 23 225 syl3anc ⊢ ( 𝜑 → ( ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) ≤ ( ∫2 ‘ 𝐻 ) ↔ ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ) )
227 224 226 mpbird ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) ≤ ( ∫2 ‘ 𝐻 ) )
228 17 19 20 227 xrletrid ⊢ ( 𝜑 → ( ∫2 ‘ 𝐻 ) = ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) )