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 ffvelcdm ⊢ ( ( 𝑓 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
69 56 54 68 syl2an ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
70 ffvelcdm ⊢ ( ( 𝑔 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑔 ‘ 𝑥 ) ∈ ℝ )
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 ffvelcdm ⊢ ( ( 𝐻 : ℝ ⟶ ( 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 dffn5 ⊢ ( 𝑔 Fn ℝ ↔ 𝑔 = ( 𝑥 ∈ ℝ ↦ ( 𝑔 ‘ 𝑥 ) ) )
96 95 bilani ⊢ ( ( 𝜑 ∧ 𝑔 Fn ℝ ) → 𝑔 = ( 𝑥 ∈ ℝ ↦ ( 𝑔 ‘ 𝑥 ) ) )
97 7 a1i ⊢ ( ( 𝜑 ∧ 𝑔 Fn ℝ ) → 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) ) )
98 85 86 94 96 97 ofrfval2 ⊢ ( ( 𝜑 ∧ 𝑔 Fn ℝ ) → ( 𝑔 ∘r ≤ 𝐺 ↔ ∀ 𝑥 ∈ ℝ ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) ) )
99 60 98 syldan ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( 𝑔 ∘r ≤ 𝐺 ↔ ∀ 𝑥 ∈ ℝ ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) ) )
100 84 99 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ∀ 𝑥 ∈ ℝ ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
101 100 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
102 54 101 sylan2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
103 102 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
104 eldifn ⊢ ( 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) → ¬ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
105 104 adantl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ¬ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
106 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
107 105 106 sylnib ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
108 imnan ⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
109 107 108 sylibr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
110 109 imp ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 ∈ 𝐵 )
111 110 iffalsed ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) = 0 )
112 103 111 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ≤ 0 )
113 82 83 75 112 leadd2dd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + 0 ) )
114 75 recnd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℂ )
115 114 addridd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + 0 ) = ( 𝑓 ‘ 𝑥 ) )
116 113 115 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( 𝑓 ‘ 𝑥 ) )
117 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → 𝑓 ∘r ≤ 𝐹 )
118 61 a1i ⊢ ( ( 𝜑 ∧ 𝑓 Fn ℝ ) → ℝ ∈ V )
119 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑓 Fn ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) ∈ V )
120 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
121 120 4 sseqtrrid ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
122 121 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝑈 )
123 122 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝑈 )
124 123 11 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
125 12 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,] +∞ ) )
126 124 125 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
127 126 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 Fn ℝ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
128 dffn5 ⊢ ( 𝑓 Fn ℝ ↔ 𝑓 = ( 𝑥 ∈ ℝ ↦ ( 𝑓 ‘ 𝑥 ) ) )
129 128 bilani ⊢ ( ( 𝜑 ∧ 𝑓 Fn ℝ ) → 𝑓 = ( 𝑥 ∈ ℝ ↦ ( 𝑓 ‘ 𝑥 ) ) )
130 6 a1i ⊢ ( ( 𝜑 ∧ 𝑓 Fn ℝ ) → 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) )
131 118 119 127 129 130 ofrfval2 ⊢ ( ( 𝜑 ∧ 𝑓 Fn ℝ ) → ( 𝑓 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) )
132 57 131 syldan ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( 𝑓 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) )
133 117 132 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ∀ 𝑥 ∈ ℝ ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
134 133 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
135 54 134 sylan2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
136 135 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
137 121 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → 𝐴 ⊆ 𝑈 )
138 137 sselda ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝑈 )
139 138 iftrued ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) = 𝐶 )
140 simpr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
141 14 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) )
142 8 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) ∈ ( 0 [,] +∞ ) ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
143 140 141 142 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
144 54 143 sylan2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
145 144 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
146 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
147 146 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
148 139 145 147 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
149 136 148 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) )
150 74 76 81 116 149 xrletrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( 𝐻 ‘ 𝑥 ) )
151 73 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* )
152 71 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ ℝ )
153 152 rexrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ ℝ* )
154 80 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ ℝ* )
155 69 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
156 0red ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ℝ )
157 135 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) )
158 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 0 )
159 158 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 0 )
160 157 159 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ≤ 0 )
161 155 156 152 160 leadd1dd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( 0 + ( 𝑔 ‘ 𝑥 ) ) )
162 152 recnd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ ℂ )
163 162 addlidd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 0 + ( 𝑔 ‘ 𝑥 ) ) = ( 𝑔 ‘ 𝑥 ) )
164 161 163 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( 𝑔 ‘ 𝑥 ) )
165 102 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ≤ if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
166 144 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
167 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
168 167 eleq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑈 ↔ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ) )
169 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
170 biorf ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ) )
171 169 170 bitr4id ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ 𝐵 ) )
172 171 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ 𝐵 ) )
173 168 172 bitrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑈 ↔ 𝑥 ∈ 𝐵 ) )
174 173 ifbid ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) = if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
175 166 174 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ 𝐵 , 𝐶 , 0 ) )
176 165 175 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) )
177 151 153 154 164 176 xrletrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( 𝐻 ‘ 𝑥 ) )
178 150 177 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ≤ ( 𝐻 ‘ 𝑥 ) )
179 67 178 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) )
180 179 ex ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) ) )
181 53 180 ralrimi ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ∀ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) )
182 nfv ⊢ Ⅎ 𝑦 ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 )
183 nfcv ⊢ Ⅎ 𝑥 ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 )
184 nfcv ⊢ Ⅎ 𝑥 ≤
185 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑈 , 𝐶 , 0 ) )
186 8 185 nfcxfr ⊢ Ⅎ 𝑥 𝐻
187 nfcv ⊢ Ⅎ 𝑥 𝑦
188 186 187 nffv ⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑦 )
189 183 184 188 nfbr ⊢ Ⅎ 𝑥 ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 ) ≤ ( 𝐻 ‘ 𝑦 )
190 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) = ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 ) )
191 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑦 ) )
192 190 191 breq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) ↔ ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 ) ≤ ( 𝐻 ‘ 𝑦 ) ) )
193 182 189 192 cbvralw ⊢ ( ∀ 𝑥 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑥 ) ≤ ( 𝐻 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 ) ≤ ( 𝐻 ‘ 𝑦 ) )
194 181 193 sylib ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ∀ 𝑦 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 ) ≤ ( 𝐻 ‘ 𝑦 ) )
195 194 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) ∧ 𝑦 ∈ ( ℝ ∖ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑓 ∘f + 𝑔 ) ‘ 𝑦 ) ≤ ( 𝐻 ‘ 𝑦 ) )
196 30 31 36 37 195 itg2uba ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ∫1 ‘ ( 𝑓 ∘f + 𝑔 ) ) ≤ ( ∫2 ‘ 𝐻 ) )
197 29 196 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ( ∫1 ‘ 𝑓 ) + ( ∫1 ‘ 𝑔 ) ) ≤ ( ∫2 ‘ 𝐻 ) )
198 26 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ∫1 ‘ 𝑓 ) ∈ ℝ )
199 itg1cl ⊢ ( 𝑔 ∈ dom ∫1 → ( ∫1 ‘ 𝑔 ) ∈ ℝ )
200 28 199 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ∫1 ‘ 𝑔 ) ∈ ℝ )
201 23 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ∫2 ‘ 𝐻 ) ∈ ℝ )
202 198 200 201 leaddsub2d ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ( ( ∫1 ‘ 𝑓 ) + ( ∫1 ‘ 𝑔 ) ) ≤ ( ∫2 ‘ 𝐻 ) ↔ ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ) )
203 197 202 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) ) → ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) )
204 203 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺 ) ) → ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) )
205 204 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑔 ∘r ≤ 𝐺 → ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ) )
206 205 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐺 → ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ) )
207 93 7 fmptd ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
208 207 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
209 24 26 resubcld ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ∈ ℝ )
210 209 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ∈ ℝ* )
211 itg2leub ⊢ ( ( 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ∈ ℝ* ) → ( ( ∫2 ‘ 𝐺 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐺 → ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ) ) )
212 208 210 211 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ( ∫2 ‘ 𝐺 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐺 → ( ∫1 ‘ 𝑔 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) ) ) )
213 206 212 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ∫2 ‘ 𝐺 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫1 ‘ 𝑓 ) ) )
214 21 24 26 213 lesubd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ∫1 ‘ 𝑓 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) )
215 214 expr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ) )
216 215 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ) )
217 126 6 fmptd ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
218 23 10 resubcld ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ∈ ℝ )
219 218 rexrd ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ∈ ℝ* )
220 itg2leub ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ∈ ℝ* ) → ( ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ) ) )
221 217 219 220 syl2anc ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ) ) )
222 216 221 mpbird ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) )
223 leaddsub ⊢ ( ( ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ 𝐺 ) ∈ ℝ ∧ ( ∫2 ‘ 𝐻 ) ∈ ℝ ) → ( ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) ≤ ( ∫2 ‘ 𝐻 ) ↔ ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ) )
224 9 10 23 223 syl3anc ⊢ ( 𝜑 → ( ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) ≤ ( ∫2 ‘ 𝐻 ) ↔ ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ 𝐻 ) − ( ∫2 ‘ 𝐺 ) ) ) )
225 222 224 mpbird ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) ≤ ( ∫2 ‘ 𝐻 ) )
226 17 19 20 225 xrletrid ⊢ ( 𝜑 → ( ∫2 ‘ 𝐻 ) = ( ( ∫2 ‘ 𝐹 ) + ( ∫2 ‘ 𝐺 ) ) )