Metamath Proof Explorer

Theorem ovolunlem1

Description: Lemma for ovolun . (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Hypotheses ovolun.a ⊢ ( 𝜑 → ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) )
ovolun.b ⊢ ( 𝜑 → ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) )
ovolun.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
ovolun.s ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
ovolun.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
ovolun.u ⊢ 𝑈 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) )
ovolun.f1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) )
ovolun.f2 ⊢ ( 𝜑 → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) )
ovolun.f3 ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) )
ovolun.g1 ⊢ ( 𝜑 → 𝐺 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) )
ovolun.g2 ⊢ ( 𝜑 → 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
ovolun.g3 ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) )
ovolun.h ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ if ( ( 𝑛 / 2 ) ∈ ℕ , ( 𝐺 ‘ ( 𝑛 / 2 ) ) , ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) )
Assertion ovolunlem1 ( 𝜑 → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ovolun.a ⊢ ( 𝜑 → ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) )
2 ovolun.b ⊢ ( 𝜑 → ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) )
3 ovolun.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
4 ovolun.s ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
5 ovolun.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
6 ovolun.u ⊢ 𝑈 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) )
7 ovolun.f1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) )
8 ovolun.f2 ⊢ ( 𝜑 → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) )
9 ovolun.f3 ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) )
10 ovolun.g1 ⊢ ( 𝜑 → 𝐺 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) )
11 ovolun.g2 ⊢ ( 𝜑 → 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
12 ovolun.g3 ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) )
13 ovolun.h ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ if ( ( 𝑛 / 2 ) ∈ ℕ , ( 𝐺 ‘ ( 𝑛 / 2 ) ) , ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) )
14 1 simpld ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
15 2 simpld ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
16 14 15 unssd ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ ℝ )
17 elovolmlem ⊢ ( 𝐺 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
18 10 17 sylib ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
20 19 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 / 2 ) ∈ ℕ ) → ( 𝐺 ‘ ( 𝑛 / 2 ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
21 nneo ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑛 + 1 ) / 2 ) ∈ ℕ ) )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑛 + 1 ) / 2 ) ∈ ℕ ) )
23 22 con2bid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑛 + 1 ) / 2 ) ∈ ℕ ↔ ¬ ( 𝑛 / 2 ) ∈ ℕ ) )
24 23 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 𝑛 / 2 ) ∈ ℕ ) → ( ( 𝑛 + 1 ) / 2 ) ∈ ℕ )
25 elovolmlem ⊢ ( 𝐹 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
26 7 25 sylib ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
28 27 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑛 + 1 ) / 2 ) ∈ ℕ ) → ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
29 24 28 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 𝑛 / 2 ) ∈ ℕ ) → ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
30 20 29 ifclda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( ( 𝑛 / 2 ) ∈ ℕ , ( 𝐺 ‘ ( 𝑛 / 2 ) ) , ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
31 30 13 fmptd ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
32 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐻 ) = ( ( abs ∘ − ) ∘ 𝐻 )
33 32 6 ovolsf ⊢ ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) )
34 31 33 syl ⊢ ( 𝜑 → 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) )
35 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
36 fss ⊢ ( ( 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝑈 : ℕ ⟶ ℝ )
37 34 35 36 sylancl ⊢ ( 𝜑 → 𝑈 : ℕ ⟶ ℝ )
38 37 frnd ⊢ ( 𝜑 → ran 𝑈 ⊆ ℝ )
39 1nn ⊢ 1 ∈ ℕ
40 1z ⊢ 1 ∈ ℤ
41 seqfn ⊢ ( 1 ∈ ℤ → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) Fn ( ℤ≥ ‘ 1 ) )
42 40 41 mp1i ⊢ ( 𝜑 → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) Fn ( ℤ≥ ‘ 1 ) )
43 6 fneq1i ⊢ ( 𝑈 Fn ℕ ↔ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) Fn ℕ )
44 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
45 44 fneq2i ⊢ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) Fn ℕ ↔ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) Fn ( ℤ≥ ‘ 1 ) )
46 43 45 bitri ⊢ ( 𝑈 Fn ℕ ↔ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) Fn ( ℤ≥ ‘ 1 ) )
47 42 46 sylibr ⊢ ( 𝜑 → 𝑈 Fn ℕ )
48 47 fndmd ⊢ ( 𝜑 → dom 𝑈 = ℕ )
49 39 48 eleqtrrid ⊢ ( 𝜑 → 1 ∈ dom 𝑈 )
50 49 ne0d ⊢ ( 𝜑 → dom 𝑈 ≠ ∅ )
51 dm0rn0 ⊢ ( dom 𝑈 = ∅ ↔ ran 𝑈 = ∅ )
52 51 necon3bii ⊢ ( dom 𝑈 ≠ ∅ ↔ ran 𝑈 ≠ ∅ )
53 50 52 sylib ⊢ ( 𝜑 → ran 𝑈 ≠ ∅ )
54 1 simprd ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) ∈ ℝ )
55 2 simprd ⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) ∈ ℝ )
56 54 55 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ )
57 3 rpred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
58 56 57 readdcld ⊢ ( 𝜑 → ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ∈ ℝ )
59 1 2 3 4 5 6 7 8 9 10 11 12 13 ovolunlem1a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ 𝑘 ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) )
60 59 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑈 ‘ 𝑘 ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) )
61 breq1 ⊢ ( 𝑧 = ( 𝑈 ‘ 𝑘 ) → ( 𝑧 ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ↔ ( 𝑈 ‘ 𝑘 ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ) )
62 61 ralrn ⊢ ( 𝑈 Fn ℕ → ( ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ↔ ∀ 𝑘 ∈ ℕ ( 𝑈 ‘ 𝑘 ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ) )
63 47 62 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ↔ ∀ 𝑘 ∈ ℕ ( 𝑈 ‘ 𝑘 ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ) )
64 60 63 mpbird ⊢ ( 𝜑 → ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) )
65 brralrspcev ⊢ ( ( ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ∈ ℝ ∧ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑘 )
66 58 64 65 syl2anc ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑘 )
67 ressxr ⊢ ℝ ⊆ ℝ*
68 38 67 sstrdi ⊢ ( 𝜑 → ran 𝑈 ⊆ ℝ* )
69 supxrbnd2 ⊢ ( ran 𝑈 ⊆ ℝ* → ( ∃ 𝑘 ∈ ℝ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑘 ↔ sup ( ran 𝑈 , ℝ* , < ) < +∞ ) )
70 68 69 syl ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℝ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑘 ↔ sup ( ran 𝑈 , ℝ* , < ) < +∞ ) )
71 66 70 mpbid ⊢ ( 𝜑 → sup ( ran 𝑈 , ℝ* , < ) < +∞ )
72 supxrbnd ⊢ ( ( ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ sup ( ran 𝑈 , ℝ* , < ) < +∞ ) → sup ( ran 𝑈 , ℝ* , < ) ∈ ℝ )
73 38 53 71 72 syl3anc ⊢ ( 𝜑 → sup ( ran 𝑈 , ℝ* , < ) ∈ ℝ )
74 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
75 74 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℂ )
76 1cnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 1 ∈ ℂ )
77 75 2timesd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2 · 𝑚 ) = ( 𝑚 + 𝑚 ) )
78 77 oveq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 2 · 𝑚 ) − 1 ) = ( ( 𝑚 + 𝑚 ) − 1 ) )
79 75 75 76 78 assraddsubd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 2 · 𝑚 ) − 1 ) = ( 𝑚 + ( 𝑚 − 1 ) ) )
80 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
81 nnm1nn0 ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 − 1 ) ∈ ℕ0 )
82 nnnn0addcl ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑚 − 1 ) ∈ ℕ0 ) → ( 𝑚 + ( 𝑚 − 1 ) ) ∈ ℕ )
83 80 81 82 syl2anc2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + ( 𝑚 − 1 ) ) ∈ ℕ )
84 79 83 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 2 · 𝑚 ) − 1 ) ∈ ℕ )
85 oveq1 ⊢ ( 𝑛 = ( ( 2 · 𝑚 ) − 1 ) → ( 𝑛 / 2 ) = ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) )
86 85 eleq1d ⊢ ( 𝑛 = ( ( 2 · 𝑚 ) − 1 ) → ( ( 𝑛 / 2 ) ∈ ℕ ↔ ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ∈ ℕ ) )
87 85 fveq2d ⊢ ( 𝑛 = ( ( 2 · 𝑚 ) − 1 ) → ( 𝐺 ‘ ( 𝑛 / 2 ) ) = ( 𝐺 ‘ ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ) )
88 oveq1 ⊢ ( 𝑛 = ( ( 2 · 𝑚 ) − 1 ) → ( 𝑛 + 1 ) = ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) )
89 88 fvoveq1d ⊢ ( 𝑛 = ( ( 2 · 𝑚 ) − 1 ) → ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) = ( 𝐹 ‘ ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) ) )
90 86 87 89 ifbieq12d ⊢ ( 𝑛 = ( ( 2 · 𝑚 ) − 1 ) → if ( ( 𝑛 / 2 ) ∈ ℕ , ( 𝐺 ‘ ( 𝑛 / 2 ) ) , ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) = if ( ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) ) ) )
91 fvex ⊢ ( 𝐺 ‘ ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ) ∈ V
92 fvex ⊢ ( 𝐹 ‘ ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) ) ∈ V
93 91 92 ifex ⊢ if ( ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) ) ) ∈ V
94 90 13 93 fvmpt ⊢ ( ( ( 2 · 𝑚 ) − 1 ) ∈ ℕ → ( 𝐻 ‘ ( ( 2 · 𝑚 ) − 1 ) ) = if ( ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) ) ) )
95 84 94 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ ( ( 2 · 𝑚 ) − 1 ) ) = if ( ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) ) ) )
96 2nn ⊢ 2 ∈ ℕ
97 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( 2 · 𝑚 ) ∈ ℕ )
98 96 80 97 sylancr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2 · 𝑚 ) ∈ ℕ )
99 98 nncnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2 · 𝑚 ) ∈ ℂ )
100 ax-1cn ⊢ 1 ∈ ℂ
101 npcan ⊢ ( ( ( 2 · 𝑚 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) = ( 2 · 𝑚 ) )
102 99 100 101 sylancl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) = ( 2 · 𝑚 ) )
103 102 oveq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) = ( ( 2 · 𝑚 ) / 2 ) )
104 2cn ⊢ 2 ∈ ℂ
105 2ne0 ⊢ 2 ≠ 0
106 divcan3 ⊢ ( ( 𝑚 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · 𝑚 ) / 2 ) = 𝑚 )
107 104 105 106 mp3an23 ⊢ ( 𝑚 ∈ ℂ → ( ( 2 · 𝑚 ) / 2 ) = 𝑚 )
108 75 107 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 2 · 𝑚 ) / 2 ) = 𝑚 )
109 103 108 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) = 𝑚 )
110 109 80 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) ∈ ℕ )
111 nneo ⊢ ( ( ( 2 · 𝑚 ) − 1 ) ∈ ℕ → ( ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ∈ ℕ ↔ ¬ ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) ∈ ℕ ) )
112 84 111 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ∈ ℕ ↔ ¬ ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) ∈ ℕ ) )
113 112 con2bid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) ∈ ℕ ↔ ¬ ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ∈ ℕ ) )
114 110 113 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ¬ ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ∈ ℕ )
115 114 iffalsed ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → if ( ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( ( 2 · 𝑚 ) − 1 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) ) ) = ( 𝐹 ‘ ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) ) )
116 109 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ ( ( ( ( 2 · 𝑚 ) − 1 ) + 1 ) / 2 ) ) = ( 𝐹 ‘ 𝑚 ) )
117 95 115 116 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ ( ( 2 · 𝑚 ) − 1 ) ) = ( 𝐹 ‘ 𝑚 ) )
118 fveqeq2 ⊢ ( 𝑘 = ( ( 2 · 𝑚 ) − 1 ) → ( ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) ↔ ( 𝐻 ‘ ( ( 2 · 𝑚 ) − 1 ) ) = ( 𝐹 ‘ 𝑚 ) ) )
119 118 rspcev ⊢ ( ( ( ( 2 · 𝑚 ) − 1 ) ∈ ℕ ∧ ( 𝐻 ‘ ( ( 2 · 𝑚 ) − 1 ) ) = ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑘 ∈ ℕ ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
120 84 117 119 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∃ 𝑘 ∈ ℕ ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
121 fveq2 ⊢ ( ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) → ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) )
122 121 breq1d ⊢ ( ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) → ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ↔ ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) )
123 fveq2 ⊢ ( ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) → ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) )
124 123 breq2d ⊢ ( ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) → ( 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ↔ 𝑧 < ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
125 122 124 anbi12d ⊢ ( ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) → ( ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ↔ ( ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
126 125 biimprcd ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ( ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) → ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
127 126 reximdv ⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ( ∃ 𝑘 ∈ ℕ ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) → ∃ 𝑘 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
128 120 127 syl5com ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ∃ 𝑘 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
129 128 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ∃ 𝑘 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
130 129 ralimdv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑘 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
131 ovolfioo ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
132 14 26 131 syl2anc ⊢ ( 𝜑 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
133 ovolfioo ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐻 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑘 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
134 14 31 133 syl2anc ⊢ ( 𝜑 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐻 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑘 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
135 130 132 134 3imtr4d ⊢ ( 𝜑 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐻 ) ) )
136 8 135 mpd ⊢ ( 𝜑 → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐻 ) )
137 oveq1 ⊢ ( 𝑛 = ( 2 · 𝑚 ) → ( 𝑛 / 2 ) = ( ( 2 · 𝑚 ) / 2 ) )
138 137 eleq1d ⊢ ( 𝑛 = ( 2 · 𝑚 ) → ( ( 𝑛 / 2 ) ∈ ℕ ↔ ( ( 2 · 𝑚 ) / 2 ) ∈ ℕ ) )
139 137 fveq2d ⊢ ( 𝑛 = ( 2 · 𝑚 ) → ( 𝐺 ‘ ( 𝑛 / 2 ) ) = ( 𝐺 ‘ ( ( 2 · 𝑚 ) / 2 ) ) )
140 oveq1 ⊢ ( 𝑛 = ( 2 · 𝑚 ) → ( 𝑛 + 1 ) = ( ( 2 · 𝑚 ) + 1 ) )
141 140 fvoveq1d ⊢ ( 𝑛 = ( 2 · 𝑚 ) → ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) = ( 𝐹 ‘ ( ( ( 2 · 𝑚 ) + 1 ) / 2 ) ) )
142 138 139 141 ifbieq12d ⊢ ( 𝑛 = ( 2 · 𝑚 ) → if ( ( 𝑛 / 2 ) ∈ ℕ , ( 𝐺 ‘ ( 𝑛 / 2 ) ) , ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) = if ( ( ( 2 · 𝑚 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( 2 · 𝑚 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( 2 · 𝑚 ) + 1 ) / 2 ) ) ) )
143 fvex ⊢ ( 𝐺 ‘ ( ( 2 · 𝑚 ) / 2 ) ) ∈ V
144 fvex ⊢ ( 𝐹 ‘ ( ( ( 2 · 𝑚 ) + 1 ) / 2 ) ) ∈ V
145 143 144 ifex ⊢ if ( ( ( 2 · 𝑚 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( 2 · 𝑚 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( 2 · 𝑚 ) + 1 ) / 2 ) ) ) ∈ V
146 142 13 145 fvmpt ⊢ ( ( 2 · 𝑚 ) ∈ ℕ → ( 𝐻 ‘ ( 2 · 𝑚 ) ) = if ( ( ( 2 · 𝑚 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( 2 · 𝑚 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( 2 · 𝑚 ) + 1 ) / 2 ) ) ) )
147 98 146 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ ( 2 · 𝑚 ) ) = if ( ( ( 2 · 𝑚 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( 2 · 𝑚 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( 2 · 𝑚 ) + 1 ) / 2 ) ) ) )
148 108 80 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 2 · 𝑚 ) / 2 ) ∈ ℕ )
149 148 iftrued ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → if ( ( ( 2 · 𝑚 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( 2 · 𝑚 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( 2 · 𝑚 ) + 1 ) / 2 ) ) ) = ( 𝐺 ‘ ( ( 2 · 𝑚 ) / 2 ) ) )
150 108 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐺 ‘ ( ( 2 · 𝑚 ) / 2 ) ) = ( 𝐺 ‘ 𝑚 ) )
151 147 149 150 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ ( 2 · 𝑚 ) ) = ( 𝐺 ‘ 𝑚 ) )
152 fveqeq2 ⊢ ( 𝑘 = ( 2 · 𝑚 ) → ( ( 𝐻 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑚 ) ↔ ( 𝐻 ‘ ( 2 · 𝑚 ) ) = ( 𝐺 ‘ 𝑚 ) ) )
153 152 rspcev ⊢ ( ( ( 2 · 𝑚 ) ∈ ℕ ∧ ( 𝐻 ‘ ( 2 · 𝑚 ) ) = ( 𝐺 ‘ 𝑚 ) ) → ∃ 𝑘 ∈ ℕ ( 𝐻 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑚 ) )
154 98 151 153 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∃ 𝑘 ∈ ℕ ( 𝐻 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑚 ) )
155 fveq2 ⊢ ( ( 𝐻 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑚 ) → ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 1st ‘ ( 𝐺 ‘ 𝑚 ) ) )
156 155 breq1d ⊢ ( ( 𝐻 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑚 ) → ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ↔ ( 1st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ) )
157 fveq2 ⊢ ( ( 𝐻 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑚 ) → ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) = ( 2nd ‘ ( 𝐺 ‘ 𝑚 ) ) )
158 157 breq2d ⊢ ( ( 𝐻 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑚 ) → ( 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ↔ 𝑧 < ( 2nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) )
159 156 158 anbi12d ⊢ ( ( 𝐻 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑚 ) → ( ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ↔ ( ( 1st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) )
160 159 biimprcd ⊢ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) → ( ( 𝐻 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑚 ) → ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
161 160 reximdv ⊢ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) → ( ∃ 𝑘 ∈ ℕ ( 𝐻 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑚 ) → ∃ 𝑘 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
162 154 161 syl5com ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( 1st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) → ∃ 𝑘 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
163 162 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) → ∃ 𝑘 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
164 163 ralimdv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 ∃ 𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) → ∀ 𝑧 ∈ 𝐵 ∃ 𝑘 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
165 ovolfioo ⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ↔ ∀ 𝑧 ∈ 𝐵 ∃ 𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) )
166 15 18 165 syl2anc ⊢ ( 𝜑 → ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ↔ ∀ 𝑧 ∈ 𝐵 ∃ 𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) )
167 ovolfioo ⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐻 ) ↔ ∀ 𝑧 ∈ 𝐵 ∃ 𝑘 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
168 15 31 167 syl2anc ⊢ ( 𝜑 → ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐻 ) ↔ ∀ 𝑧 ∈ 𝐵 ∃ 𝑘 ∈ ℕ ( ( 1st ‘ ( 𝐻 ‘ 𝑘 ) ) < 𝑧 ∧ 𝑧 < ( 2nd ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
169 164 166 168 3imtr4d ⊢ ( 𝜑 → ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐺 ) → 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐻 ) ) )
170 11 169 mpd ⊢ ( 𝜑 → 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐻 ) )
171 136 170 unssd ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝐻 ) )
172 6 ovollb ⊢ ( ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝐻 ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ sup ( ran 𝑈 , ℝ* , < ) )
173 31 171 172 syl2anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ sup ( ran 𝑈 , ℝ* , < ) )
174 ovollecl ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ℝ ∧ sup ( ran 𝑈 , ℝ* , < ) ∈ ℝ ∧ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ sup ( ran 𝑈 , ℝ* , < ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ℝ )
175 16 73 173 174 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ℝ )
176 58 rexrd ⊢ ( 𝜑 → ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ∈ ℝ* )
177 supxrleub ⊢ ( ( ran 𝑈 ⊆ ℝ* ∧ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ∈ ℝ* ) → ( sup ( ran 𝑈 , ℝ* , < ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ↔ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ) )
178 68 176 177 syl2anc ⊢ ( 𝜑 → ( sup ( ran 𝑈 , ℝ* , < ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ↔ ∀ 𝑧 ∈ ran 𝑈 𝑧 ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ) )
179 64 178 mpbird ⊢ ( 𝜑 → sup ( ran 𝑈 , ℝ* , < ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) )
180 175 73 58 173 179 letrd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) )