This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uniioombllem1

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 25-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
uniioombl.a ⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
uniioombl.e ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
uniioombl.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
uniioombl.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.s ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
uniioombl.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
uniioombl.v ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
Assertion uniioombllem1 ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2 uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
3 uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4 uniioombl.a ⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
5 uniioombl.e ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
6 uniioombl.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
7 uniioombl.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
8 uniioombl.s ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
9 uniioombl.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
10 uniioombl.v ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
11 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐺 ) = ( ( abs ∘ − ) ∘ 𝐺 )
12 11 9 ovolsf ⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
13 7 12 syl ⊢ ( 𝜑 → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
14 13 frnd ⊢ ( 𝜑 → ran 𝑇 ⊆ ( 0 [,) +∞ ) )
15 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
16 14 15 sstrdi ⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ )
17 1nn ⊢ 1 ∈ ℕ
18 13 fdmd ⊢ ( 𝜑 → dom 𝑇 = ℕ )
19 17 18 eleqtrrid ⊢ ( 𝜑 → 1 ∈ dom 𝑇 )
20 19 ne0d ⊢ ( 𝜑 → dom 𝑇 ≠ ∅ )
21 dm0rn0 ⊢ ( dom 𝑇 = ∅ ↔ ran 𝑇 = ∅ )
22 21 necon3bii ⊢ ( dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅ )
23 20 22 sylib ⊢ ( 𝜑 → ran 𝑇 ≠ ∅ )
24 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
25 14 24 sstrdi ⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ* )
26 supxrcl ⊢ ( ran 𝑇 ⊆ ℝ* → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ* )
27 25 26 syl ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ* )
28 6 rpred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
29 5 28 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ 𝐸 ) + 𝐶 ) ∈ ℝ )
30 29 rexrd ⊢ ( 𝜑 → ( ( vol* ‘ 𝐸 ) + 𝐶 ) ∈ ℝ* )
31 pnfxr ⊢ +∞ ∈ ℝ*
32 31 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
33 29 ltpnfd ⊢ ( 𝜑 → ( ( vol* ‘ 𝐸 ) + 𝐶 ) < +∞ )
34 27 30 32 10 33 xrlelttrd ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) < +∞ )
35 supxrbnd ⊢ ( ( ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ sup ( ran 𝑇 , ℝ* , < ) < +∞ ) → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
36 16 23 34 35 syl3anc ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )