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 sselid ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑇𝑗 ) ∈ ℝ )
43 eqid ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 )
44 43 6 ovolsf ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
45 9 44 syl ( 𝜑𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
46 45 ffvelrnda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑆𝑗 ) ∈ ( 0 [,) +∞ ) )
47 32 46 sselid ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑆𝑗 ) ∈ ℝ )
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 sselid ( ( 𝜑𝑛 ∈ ℕ ) → ( ( ( 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 sselid ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑈𝑗 ) ∈ ℝ )
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* ‘ 𝐸 ) + 𝐶 ) )