Metamath Proof Explorer

Theorem ioombl1lem4

Description: Lemma for ioombl1 . (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Hypotheses ioombl1.b ⊢ 𝐵 = ( 𝐴 (,) +∞ )
ioombl1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ioombl1.e ⊢ ( 𝜑 → 𝐸 ⊆ ℝ )
ioombl1.v ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
ioombl1.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
ioombl1.s ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
ioombl1.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
ioombl1.u ⊢ 𝑈 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) )
ioombl1.f1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
ioombl1.f2 ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐹 ) )
ioombl1.f3 ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
ioombl1.p ⊢ 𝑃 = ( 1st ‘ ( 𝐹 ‘ 𝑛 ) )
ioombl1.q ⊢ 𝑄 = ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) )
ioombl1.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ )
ioombl1.h ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ )
Assertion ioombl1lem4 ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ioombl1.b ⊢ 𝐵 = ( 𝐴 (,) +∞ )
2 ioombl1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 ioombl1.e ⊢ ( 𝜑 → 𝐸 ⊆ ℝ )
4 ioombl1.v ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
5 ioombl1.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
6 ioombl1.s ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
7 ioombl1.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
8 ioombl1.u ⊢ 𝑈 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) )
9 ioombl1.f1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
10 ioombl1.f2 ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐹 ) )
11 ioombl1.f3 ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
12 ioombl1.p ⊢ 𝑃 = ( 1st ‘ ( 𝐹 ‘ 𝑛 ) )
13 ioombl1.q ⊢ 𝑄 = ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) )
14 ioombl1.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ )
15 ioombl1.h ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ )
16 inss1 ⊢ ( 𝐸 ∩ 𝐵 ) ⊆ 𝐸
17 ovolsscl ⊢ ( ( ( 𝐸 ∩ 𝐵 ) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) ∈ ℝ )
18 16 3 4 17 mp3an2i ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) ∈ ℝ )
19 difss ⊢ ( 𝐸 ∖ 𝐵 ) ⊆ 𝐸
20 ovolsscl ⊢ ( ( ( 𝐸 ∖ 𝐵 ) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ∈ ℝ )
21 19 3 4 20 mp3an2i ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ∈ ℝ )
22 18 21 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ) ∈ ℝ )
23 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 ioombl1lem2 ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ )
24 5 rpred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
25 4 24 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ 𝐸 ) + 𝐶 ) ∈ ℝ )
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 ioombl1lem1 ⊢ ( 𝜑 → ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) )
27 26 simpld ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
28 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐺 ) = ( ( abs ∘ − ) ∘ 𝐺 )
29 28 7 ovolsf ⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
30 27 29 syl ⊢ ( 𝜑 → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
31 30 frnd ⊢ ( 𝜑 → ran 𝑇 ⊆ ( 0 [,) +∞ ) )
32 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
33 31 32 sstrdi ⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ )
34 1nn ⊢ 1 ∈ ℕ
35 30 fdmd ⊢ ( 𝜑 → dom 𝑇 = ℕ )
36 34 35 eleqtrrid ⊢ ( 𝜑 → 1 ∈ dom 𝑇 )
37 36 ne0d ⊢ ( 𝜑 → dom 𝑇 ≠ ∅ )
38 dm0rn0 ⊢ ( dom 𝑇 = ∅ ↔ ran 𝑇 = ∅ )
39 38 necon3bii ⊢ ( dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅ )
40 37 39 sylib ⊢ ( 𝜑 → ran 𝑇 ≠ ∅ )
41 30 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) )
42 32 41 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 ‘ 𝑗 ) ∈ ℝ )
43 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 )
44 43 6 ovolsf ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
45 9 44 syl ⊢ ( 𝜑 → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
46 45 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑆 ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) )
47 32 46 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
48 23 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ )
49 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
50 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
51 49 50 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
52 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝜑 )
53 elfznn ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 𝑛 ∈ ℕ )
54 28 ovolfsf ⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐺 ) : ℕ ⟶ ( 0 [,) +∞ ) )
55 27 54 syl ⊢ ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐺 ) : ℕ ⟶ ( 0 [,) +∞ ) )
56 55 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) )
57 32 56 sseldi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ℝ )
58 52 53 57 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ℝ )
59 43 ovolfsf ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) )
60 9 59 syl ⊢ ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) )
61 60 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) )
62 elrege0 ⊢ ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ) )
63 61 62 sylib ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ) )
64 63 simpld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ℝ )
65 52 53 64 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ℝ )
66 26 simprd ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
67 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐻 ) = ( ( abs ∘ − ) ∘ 𝐻 )
68 67 ovolfsf ⊢ ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐻 ) : ℕ ⟶ ( 0 [,) +∞ ) )
69 66 68 syl ⊢ ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐻 ) : ℕ ⟶ ( 0 [,) +∞ ) )
70 69 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) )
71 elrege0 ⊢ ( ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) )
72 70 71 sylib ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) )
73 72 simprd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) )
74 72 simpld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ℝ )
75 57 74 addge01d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ↔ ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ≤ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) ) )
76 73 75 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ≤ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) )
77 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 ioombl1lem3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) = ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) )
78 76 77 breqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) )
79 52 53 78 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) )
80 51 58 65 79 serle ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑗 ) ≤ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑗 ) )
81 7 fveq1i ⊢ ( 𝑇 ‘ 𝑗 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑗 )
82 6 fveq1i ⊢ ( 𝑆 ‘ 𝑗 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑗 )
83 80 81 82 3brtr4g ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 ‘ 𝑗 ) ≤ ( 𝑆 ‘ 𝑗 ) )
84 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
85 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) )
86 63 simprd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) )
87 45 frnd ⊢ ( 𝜑 → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
88 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
89 87 88 sstrdi ⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ* )
90 89 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ran 𝑆 ⊆ ℝ* )
91 45 ffnd ⊢ ( 𝜑 → 𝑆 Fn ℕ )
92 fnfvelrn ⊢ ( ( 𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ∈ ran 𝑆 )
93 91 92 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ∈ ran 𝑆 )
94 supxrub ⊢ ( ( ran 𝑆 ⊆ ℝ* ∧ ( 𝑆 ‘ 𝑘 ) ∈ ran 𝑆 ) → ( 𝑆 ‘ 𝑘 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
95 90 93 94 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
96 95 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
97 brralrspcev ⊢ ( ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ∧ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 )
98 23 96 97 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 )
99 50 6 84 85 64 86 98 isumsup2 ⊢ ( 𝜑 → 𝑆 ⇝ sup ( ran 𝑆 , ℝ , < ) )
100 87 32 sstrdi ⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ )
101 45 fdmd ⊢ ( 𝜑 → dom 𝑆 = ℕ )
102 34 101 eleqtrrid ⊢ ( 𝜑 → 1 ∈ dom 𝑆 )
103 102 ne0d ⊢ ( 𝜑 → dom 𝑆 ≠ ∅ )
104 dm0rn0 ⊢ ( dom 𝑆 = ∅ ↔ ran 𝑆 = ∅ )
105 104 necon3bii ⊢ ( dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅ )
106 103 105 sylib ⊢ ( 𝜑 → ran 𝑆 ≠ ∅ )
107 breq1 ⊢ ( 𝑧 = ( 𝑆 ‘ 𝑘 ) → ( 𝑧 ≤ 𝑥 ↔ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) )
108 107 ralrn ⊢ ( 𝑆 Fn ℕ → ( ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) )
109 91 108 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) )
110 109 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑥 ) )
111 98 110 mpbird ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 )
112 supxrre ⊢ ( ( ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ) → sup ( ran 𝑆 , ℝ* , < ) = sup ( ran 𝑆 , ℝ , < ) )
113 100 106 111 112 syl3anc ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) = sup ( ran 𝑆 , ℝ , < ) )
114 99 113 breqtrrd ⊢ ( 𝜑 → 𝑆 ⇝ sup ( ran 𝑆 , ℝ* , < ) )
115 114 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑆 ⇝ sup ( ran 𝑆 , ℝ* , < ) )
116 6 115 eqbrtrrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ⇝ sup ( ran 𝑆 , ℝ* , < ) )
117 64 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) ∈ ℝ )
118 86 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) )
119 50 49 116 117 118 climserle ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
120 82 119 eqbrtrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑆 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
121 42 47 48 83 120 letrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
122 121 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
123 brralrspcev ⊢ ( ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ∧ ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ 𝑥 )
124 23 122 123 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ 𝑥 )
125 30 ffnd ⊢ ( 𝜑 → 𝑇 Fn ℕ )
126 breq1 ⊢ ( 𝑧 = ( 𝑇 ‘ 𝑗 ) → ( 𝑧 ≤ 𝑥 ↔ ( 𝑇 ‘ 𝑗 ) ≤ 𝑥 ) )
127 126 ralrn ⊢ ( 𝑇 Fn ℕ → ( ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ 𝑥 ) )
128 125 127 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ 𝑥 ) )
129 128 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝑇 ‘ 𝑗 ) ≤ 𝑥 ) )
130 124 129 mpbird ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 )
131 33 40 130 suprcld ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ , < ) ∈ ℝ )
132 67 8 ovolsf ⊢ ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) )
133 66 132 syl ⊢ ( 𝜑 → 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) )
134 133 frnd ⊢ ( 𝜑 → ran 𝑈 ⊆ ( 0 [,) +∞ ) )
135 134 32 sstrdi ⊢ ( 𝜑 → ran 𝑈 ⊆ ℝ )
136 133 fdmd ⊢ ( 𝜑 → dom 𝑈 = ℕ )
137 34 136 eleqtrrid ⊢ ( 𝜑 → 1 ∈ dom 𝑈 )
138 137 ne0d ⊢ ( 𝜑 → dom 𝑈 ≠ ∅ )
139 dm0rn0 ⊢ ( dom 𝑈 = ∅ ↔ ran 𝑈 = ∅ )
140 139 necon3bii ⊢ ( dom 𝑈 ≠ ∅ ↔ ran 𝑈 ≠ ∅ )
141 138 140 sylib ⊢ ( 𝜑 → ran 𝑈 ≠ ∅ )
142 133 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑈 ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) )
143 32 142 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑈 ‘ 𝑗 ) ∈ ℝ )
144 52 53 74 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ℝ )
145 elrege0 ⊢ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ) )
146 56 145 sylib ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ) )
147 146 simprd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) )
148 74 57 addge02d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ↔ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ≤ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) ) )
149 147 148 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ≤ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) )
150 149 77 breqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) )
151 52 53 150 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) )
152 51 144 65 151 serle ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 𝑗 ) ≤ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑗 ) )
153 8 fveq1i ⊢ ( 𝑈 ‘ 𝑗 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 𝑗 )
154 152 153 82 3brtr4g ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑈 ‘ 𝑗 ) ≤ ( 𝑆 ‘ 𝑗 ) )
155 143 47 48 154 120 letrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑈 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
156 155 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
157 brralrspcev ⊢ ( ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ∧ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ 𝑥 )
158 23 156 157 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ 𝑥 )
159 133 ffnd ⊢ ( 𝜑 → 𝑈 Fn ℕ )
160 breq1 ⊢ ( 𝑧 = ( 𝑈 ‘ 𝑗 ) → ( 𝑧 ≤ 𝑥 ↔ ( 𝑈 ‘ 𝑗 ) ≤ 𝑥 ) )
161 160 ralrn ⊢ ( 𝑈 Fn ℕ → ( ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ 𝑥 ) )
162 159 161 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ 𝑥 ) )
163 162 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝑈 ‘ 𝑗 ) ≤ 𝑥 ) )
164 158 163 mpbird ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 )
165 135 141 164 suprcld ⊢ ( 𝜑 → sup ( ran 𝑈 , ℝ , < ) ∈ ℝ )
166 ssralv ⊢ ( ( 𝐸 ∩ 𝐵 ) ⊆ 𝐸 → ( ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
167 16 166 ax-mp ⊢ ( ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
168 12 breq1i ⊢ ( 𝑃 < 𝑥 ↔ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 )
169 ovolfcl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
170 9 169 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
171 170 simp1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
172 12 171 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑃 ∈ ℝ )
173 172 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑃 ∈ ℝ )
174 16 3 sstrid ⊢ ( 𝜑 → ( 𝐸 ∩ 𝐵 ) ⊆ ℝ )
175 174 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) → 𝑥 ∈ ℝ )
176 175 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ ℝ )
177 ltle ⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑃 < 𝑥 → 𝑃 ≤ 𝑥 ) )
178 173 176 177 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 < 𝑥 → 𝑃 ≤ 𝑥 ) )
179 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
180 opex ⊢ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ∈ V
181 14 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ∈ V ) → ( 𝐺 ‘ 𝑛 ) = ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ )
182 179 180 181 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) = ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ )
183 182 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 1st ‘ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ) )
184 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℝ )
185 184 172 ifcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∈ ℝ )
186 170 simp2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
187 13 186 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑄 ∈ ℝ )
188 185 187 ifcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ )
189 op1stg ⊢ ( ( if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ∧ 𝑄 ∈ ℝ ) → ( 1st ‘ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
190 188 187 189 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
191 183 190 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
192 191 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
193 188 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ )
194 185 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∈ ℝ )
195 174 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → ( 𝐸 ∩ 𝐵 ) ⊆ ℝ )
196 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) )
197 195 196 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
198 187 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝑄 ∈ ℝ )
199 min1 ⊢ ( ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∈ ℝ ∧ 𝑄 ∈ ℝ ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) )
200 194 198 199 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) )
201 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝐴 ∈ ℝ )
202 elinel2 ⊢ ( 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) → 𝑥 ∈ 𝐵 )
203 202 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝑥 ∈ 𝐵 )
204 2 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
205 pnfxr ⊢ +∞ ∈ ℝ*
206 elioo2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞ ) ) )
207 204 205 206 sylancl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞ ) ) )
208 1 eleq2i ⊢ ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( 𝐴 (,) +∞ ) )
209 ltpnf ⊢ ( 𝑥 ∈ ℝ → 𝑥 < +∞ )
210 209 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) → 𝑥 < +∞ )
211 210 pm4.71i ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ∧ 𝑥 < +∞ ) )
212 df-3an ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞ ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ∧ 𝑥 < +∞ ) )
213 211 212 bitr4i ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞ ) )
214 207 208 213 3bitr4g ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ) )
215 simpr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) → 𝐴 < 𝑥 )
216 214 215 syl6bi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝐴 < 𝑥 ) )
217 216 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → ( 𝑥 ∈ 𝐵 → 𝐴 < 𝑥 ) )
218 203 217 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝐴 < 𝑥 )
219 201 197 218 ltled ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝐴 ≤ 𝑥 )
220 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → 𝑃 ≤ 𝑥 )
221 breq1 ⊢ ( 𝐴 = if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) → ( 𝐴 ≤ 𝑥 ↔ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑥 ) )
222 breq1 ⊢ ( 𝑃 = if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) → ( 𝑃 ≤ 𝑥 ↔ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑥 ) )
223 221 222 ifboth ⊢ ( ( 𝐴 ≤ 𝑥 ∧ 𝑃 ≤ 𝑥 ) → if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑥 )
224 219 220 223 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑥 )
225 193 194 197 200 224 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ≤ 𝑥 )
226 192 225 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 )
227 226 expr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 ≤ 𝑥 → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ) )
228 178 227 syld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 < 𝑥 → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ) )
229 168 228 syl5bir ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ) )
230 13 breq2i ⊢ ( 𝑥 < 𝑄 ↔ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) )
231 187 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑄 ∈ ℝ )
232 ltle ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑄 ∈ ℝ ) → ( 𝑥 < 𝑄 → 𝑥 ≤ 𝑄 ) )
233 176 231 232 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < 𝑄 → 𝑥 ≤ 𝑄 ) )
234 230 233 syl5bir ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ≤ 𝑄 ) )
235 182 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 2nd ‘ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ) )
236 op2ndg ⊢ ( ( if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ∧ 𝑄 ∈ ℝ ) → ( 2nd ‘ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ) = 𝑄 )
237 188 187 236 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ) = 𝑄 )
238 235 237 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) = 𝑄 )
239 238 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) = 𝑄 )
240 239 breq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ 𝑥 ≤ 𝑄 ) )
241 234 240 sylibrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
242 229 241 anim12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
243 242 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ) → ( ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
244 243 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
245 167 244 syl5 ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
246 ovolfioo ⊢ ( ( 𝐸 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
247 3 9 246 syl2anc ⊢ ( 𝜑 → ( 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
248 ovolficc ⊢ ( ( ( 𝐸 ∩ 𝐵 ) ⊆ ℝ ∧ 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( ( 𝐸 ∩ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ↔ ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
249 174 27 248 syl2anc ⊢ ( 𝜑 → ( ( 𝐸 ∩ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ↔ ∀ 𝑥 ∈ ( 𝐸 ∩ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
250 245 247 249 3imtr4d ⊢ ( 𝜑 → ( 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐹 ) → ( 𝐸 ∩ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ) )
251 10 250 mpd ⊢ ( 𝜑 → ( 𝐸 ∩ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) )
252 7 ovollb2 ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( 𝐸 ∩ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ) → ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
253 27 251 252 syl2anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
254 supxrre ⊢ ( ( ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ) → sup ( ran 𝑇 , ℝ* , < ) = sup ( ran 𝑇 , ℝ , < ) )
255 33 40 130 254 syl3anc ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) = sup ( ran 𝑇 , ℝ , < ) )
256 253 255 breqtrd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) ≤ sup ( ran 𝑇 , ℝ , < ) )
257 ssralv ⊢ ( ( 𝐸 ∖ 𝐵 ) ⊆ 𝐸 → ( ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
258 19 257 ax-mp ⊢ ( ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
259 172 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑃 ∈ ℝ )
260 19 3 sstrid ⊢ ( 𝜑 → ( 𝐸 ∖ 𝐵 ) ⊆ ℝ )
261 260 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) → 𝑥 ∈ ℝ )
262 261 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ ℝ )
263 259 262 177 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 < 𝑥 → 𝑃 ≤ 𝑥 ) )
264 168 263 syl5bir ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 → 𝑃 ≤ 𝑥 ) )
265 opex ⊢ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ∈ V
266 15 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ∈ V ) → ( 𝐻 ‘ 𝑛 ) = ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ )
267 179 265 266 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐻 ‘ 𝑛 ) = ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ )
268 267 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) = ( 1st ‘ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ) )
269 op1stg ⊢ ( ( 𝑃 ∈ ℝ ∧ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ) → ( 1st ‘ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ) = 𝑃 )
270 172 188 269 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ) = 𝑃 )
271 268 270 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) = 𝑃 )
272 271 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) = 𝑃 )
273 272 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ↔ 𝑃 ≤ 𝑥 ) )
274 264 273 sylibrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 → ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ) )
275 187 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑄 ∈ ℝ )
276 262 275 232 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < 𝑄 → 𝑥 ≤ 𝑄 ) )
277 260 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ( 𝐸 ∖ 𝐵 ) ⊆ ℝ )
278 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) )
279 277 278 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ∈ ℝ )
280 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝐴 ∈ ℝ )
281 172 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑃 ∈ ℝ )
282 280 281 ifcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∈ ℝ )
283 eldifn ⊢ ( 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) → ¬ 𝑥 ∈ 𝐵 )
284 283 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ¬ 𝑥 ∈ 𝐵 )
285 279 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ( 𝐴 < 𝑥 ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ) )
286 214 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ) ) )
287 285 286 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ( 𝐴 < 𝑥 ↔ 𝑥 ∈ 𝐵 ) )
288 284 287 mtbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ¬ 𝐴 < 𝑥 )
289 279 280 288 nltled ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ≤ 𝐴 )
290 max2 ⊢ ( ( 𝑃 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → 𝐴 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) )
291 281 280 290 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝐴 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) )
292 279 280 282 289 291 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) )
293 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ≤ 𝑄 )
294 breq2 ⊢ ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) → ( 𝑥 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ↔ 𝑥 ≤ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) )
295 breq2 ⊢ ( 𝑄 = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) → ( 𝑥 ≤ 𝑄 ↔ 𝑥 ≤ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) )
296 294 295 ifboth ⊢ ( ( 𝑥 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∧ 𝑥 ≤ 𝑄 ) → 𝑥 ≤ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
297 292 293 296 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ≤ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
298 267 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) = ( 2nd ‘ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ) )
299 op2ndg ⊢ ( ( 𝑃 ∈ ℝ ∧ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ) → ( 2nd ‘ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
300 172 188 299 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
301 298 300 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
302 301 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
303 297 302 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄 ) ) → 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) )
304 303 expr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ≤ 𝑄 → 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) )
305 276 304 syld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < 𝑄 → 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) )
306 230 305 syl5bir ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) )
307 274 306 anim12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) )
308 307 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ) → ( ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) )
309 308 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) )
310 258 309 syl5 ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐸 ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) )
311 ovolficc ⊢ ( ( ( 𝐸 ∖ 𝐵 ) ⊆ ℝ ∧ 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( ( 𝐸 ∖ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐻 ) ↔ ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) )
312 260 66 311 syl2anc ⊢ ( 𝜑 → ( ( 𝐸 ∖ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐻 ) ↔ ∀ 𝑥 ∈ ( 𝐸 ∖ 𝐵 ) ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) )
313 310 247 312 3imtr4d ⊢ ( 𝜑 → ( 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐹 ) → ( 𝐸 ∖ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐻 ) ) )
314 10 313 mpd ⊢ ( 𝜑 → ( 𝐸 ∖ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐻 ) )
315 8 ovollb2 ⊢ ( ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( 𝐸 ∖ 𝐵 ) ⊆ ∪ ran ( [,] ∘ 𝐻 ) ) → ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ≤ sup ( ran 𝑈 , ℝ* , < ) )
316 66 314 315 syl2anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ≤ sup ( ran 𝑈 , ℝ* , < ) )
317 supxrre ⊢ ( ( ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ) → sup ( ran 𝑈 , ℝ* , < ) = sup ( ran 𝑈 , ℝ , < ) )
318 135 141 164 317 syl3anc ⊢ ( 𝜑 → sup ( ran 𝑈 , ℝ* , < ) = sup ( ran 𝑈 , ℝ , < ) )
319 316 318 breqtrd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ≤ sup ( ran 𝑈 , ℝ , < ) )
320 18 21 131 165 256 319 le2addd ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ) ≤ ( sup ( ran 𝑇 , ℝ , < ) + sup ( ran 𝑈 , ℝ , < ) ) )
321 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) )
322 50 7 84 321 57 147 124 isumsup2 ⊢ ( 𝜑 → 𝑇 ⇝ sup ( ran 𝑇 , ℝ , < ) )
323 seqex ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ∈ V
324 6 323 eqeltri ⊢ 𝑆 ∈ V
325 324 a1i ⊢ ( 𝜑 → 𝑆 ∈ V )
326 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) = ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) )
327 50 8 84 326 74 73 158 isumsup2 ⊢ ( 𝜑 → 𝑈 ⇝ sup ( ran 𝑈 , ℝ , < ) )
328 42 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 ‘ 𝑗 ) ∈ ℂ )
329 143 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑈 ‘ 𝑗 ) ∈ ℂ )
330 57 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ℂ )
331 52 53 330 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) ∈ ℂ )
332 74 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ℂ )
333 52 53 332 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ∈ ℂ )
334 77 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) )
335 52 53 334 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) )
336 51 331 333 335 seradd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑗 ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑗 ) + ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 𝑗 ) ) )
337 81 153 oveq12i ⊢ ( ( 𝑇 ‘ 𝑗 ) + ( 𝑈 ‘ 𝑗 ) ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑗 ) + ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 𝑗 ) )
338 336 82 337 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑆 ‘ 𝑗 ) = ( ( 𝑇 ‘ 𝑗 ) + ( 𝑈 ‘ 𝑗 ) ) )
339 50 84 322 325 327 328 329 338 climadd ⊢ ( 𝜑 → 𝑆 ⇝ ( sup ( ran 𝑇 , ℝ , < ) + sup ( ran 𝑈 , ℝ , < ) ) )
340 climuni ⊢ ( ( 𝑆 ⇝ ( sup ( ran 𝑇 , ℝ , < ) + sup ( ran 𝑈 , ℝ , < ) ) ∧ 𝑆 ⇝ sup ( ran 𝑆 , ℝ* , < ) ) → ( sup ( ran 𝑇 , ℝ , < ) + sup ( ran 𝑈 , ℝ , < ) ) = sup ( ran 𝑆 , ℝ* , < ) )
341 339 114 340 syl2anc ⊢ ( 𝜑 → ( sup ( ran 𝑇 , ℝ , < ) + sup ( ran 𝑈 , ℝ , < ) ) = sup ( ran 𝑆 , ℝ* , < ) )
342 320 341 breqtrd ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
343 22 23 25 342 11 letrd ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐵 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐵 ) ) ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )