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

Metamath Proof Explorer

Theorem ioombl1lem2

Description: Lemma for ioombl1 . (Contributed by Mario Carneiro, 18-Aug-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 ioombl1lem2 ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ )

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 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 )
17 16 6 ovolsf ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
18 9 17 syl ⊢ ( 𝜑 → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
19 18 frnd ⊢ ( 𝜑 → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
20 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
21 19 20 sstrdi ⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ* )
22 supxrcl ⊢ ( ran 𝑆 ⊆ ℝ* → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* )
23 21 22 syl ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* )
24 5 rpred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
25 4 24 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ 𝐸 ) + 𝐶 ) ∈ ℝ )
26 mnfxr ⊢ -∞ ∈ ℝ*
27 26 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
28 18 ffnd ⊢ ( 𝜑 → 𝑆 Fn ℕ )
29 1nn ⊢ 1 ∈ ℕ
30 fnfvelrn ⊢ ( ( 𝑆 Fn ℕ ∧ 1 ∈ ℕ ) → ( 𝑆 ‘ 1 ) ∈ ran 𝑆 )
31 28 29 30 sylancl ⊢ ( 𝜑 → ( 𝑆 ‘ 1 ) ∈ ran 𝑆 )
32 21 31 sseldd ⊢ ( 𝜑 → ( 𝑆 ‘ 1 ) ∈ ℝ* )
33 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
34 ffvelcdm ⊢ ( ( 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) ∧ 1 ∈ ℕ ) → ( 𝑆 ‘ 1 ) ∈ ( 0 [,) +∞ ) )
35 18 29 34 sylancl ⊢ ( 𝜑 → ( 𝑆 ‘ 1 ) ∈ ( 0 [,) +∞ ) )
36 33 35 sselid ⊢ ( 𝜑 → ( 𝑆 ‘ 1 ) ∈ ℝ )
37 36 mnfltd ⊢ ( 𝜑 → -∞ < ( 𝑆 ‘ 1 ) )
38 supxrub ⊢ ( ( ran 𝑆 ⊆ ℝ* ∧ ( 𝑆 ‘ 1 ) ∈ ran 𝑆 ) → ( 𝑆 ‘ 1 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
39 21 31 38 syl2anc ⊢ ( 𝜑 → ( 𝑆 ‘ 1 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
40 27 32 23 37 39 xrltletrd ⊢ ( 𝜑 → -∞ < sup ( ran 𝑆 , ℝ* , < ) )
41 xrre ⊢ ( ( ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* ∧ ( ( vol* ‘ 𝐸 ) + 𝐶 ) ∈ ℝ ) ∧ ( -∞ < sup ( ran 𝑆 , ℝ* , < ) ∧ sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) ) ) → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ )
42 23 25 40 11 41 syl22anc ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ )