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 𝑆 , ℝ* , < ) ∈ ℝ )