Metamath Proof Explorer

Theorem ioombl1lem2

Description: Lemma for ioombl1 . (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses ioombl1.b ⊢ B = A +∞
ioombl1.a ⊢ φ → A ∈ ℝ
ioombl1.e ⊢ φ → E ⊆ ℝ
ioombl1.v ⊢ φ → vol * ⁡ E ∈ ℝ
ioombl1.c ⊢ φ → C ∈ ℝ +
ioombl1.s ⊢ S = seq 1 + abs ∘ − ∘ F
ioombl1.t ⊢ T = seq 1 + abs ∘ − ∘ G
ioombl1.u ⊢ U = seq 1 + abs ∘ − ∘ H
ioombl1.f1 ⊢ φ → F : ℕ ⟶ ≤ ∩ ℝ 2
ioombl1.f2 ⊢ φ → E ⊆ ⋃ ran ⁡ . ∘ F
ioombl1.f3 ⊢ φ → sup ran ⁡ S ℝ * < ≤ vol * ⁡ E + C
ioombl1.p ⊢ P = 1 st ⁡ F ⁡ n
ioombl1.q ⊢ Q = 2 nd ⁡ F ⁡ n
ioombl1.g ⊢ G = n ∈ ℕ ⟼ if if P ≤ A A P ≤ Q if P ≤ A A P Q Q
ioombl1.h ⊢ H = n ∈ ℕ ⟼ P if if P ≤ A A P ≤ Q if P ≤ A A P Q
Assertion ioombl1lem2 ⊢ φ → sup ran ⁡ S ℝ * < ∈ ℝ

Proof

Step Hyp Ref Expression
1 ioombl1.b ⊢ B = A +∞
2 ioombl1.a ⊢ φ → A ∈ ℝ
3 ioombl1.e ⊢ φ → E ⊆ ℝ
4 ioombl1.v ⊢ φ → vol * ⁡ E ∈ ℝ
5 ioombl1.c ⊢ φ → C ∈ ℝ +
6 ioombl1.s ⊢ S = seq 1 + abs ∘ − ∘ F
7 ioombl1.t ⊢ T = seq 1 + abs ∘ − ∘ G
8 ioombl1.u ⊢ U = seq 1 + abs ∘ − ∘ H
9 ioombl1.f1 ⊢ φ → F : ℕ ⟶ ≤ ∩ ℝ 2
10 ioombl1.f2 ⊢ φ → E ⊆ ⋃ ran ⁡ . ∘ F
11 ioombl1.f3 ⊢ φ → sup ran ⁡ S ℝ * < ≤ vol * ⁡ E + C
12 ioombl1.p ⊢ P = 1 st ⁡ F ⁡ n
13 ioombl1.q ⊢ Q = 2 nd ⁡ F ⁡ n
14 ioombl1.g ⊢ G = n ∈ ℕ ⟼ if if P ≤ A A P ≤ Q if P ≤ A A P Q Q
15 ioombl1.h ⊢ H = n ∈ ℕ ⟼ P if if P ≤ A A P ≤ Q if P ≤ A A P Q
16 eqid ⊢ abs ∘ − ∘ F = abs ∘ − ∘ F
17 16 6 ovolsf ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 → S : ℕ ⟶ 0 +∞
18 9 17 syl ⊢ φ → S : ℕ ⟶ 0 +∞
19 18 frnd ⊢ φ → ran ⁡ S ⊆ 0 +∞
20 icossxr ⊢ 0 +∞ ⊆ ℝ *
21 19 20 sstrdi ⊢ φ → ran ⁡ S ⊆ ℝ *
22 supxrcl ⊢ ran ⁡ S ⊆ ℝ * → sup ran ⁡ S ℝ * < ∈ ℝ *
23 21 22 syl ⊢ φ → sup ran ⁡ S ℝ * < ∈ ℝ *
24 5 rpred ⊢ φ → C ∈ ℝ
25 4 24 readdcld ⊢ φ → vol * ⁡ E + C ∈ ℝ
26 mnfxr ⊢ −∞ ∈ ℝ *
27 26 a1i ⊢ φ → −∞ ∈ ℝ *
28 18 ffnd ⊢ φ → S Fn ℕ
29 1nn ⊢ 1 ∈ ℕ
30 fnfvelrn ⊢ S Fn ℕ ∧ 1 ∈ ℕ → S ⁡ 1 ∈ ran ⁡ S
31 28 29 30 sylancl ⊢ φ → S ⁡ 1 ∈ ran ⁡ S
32 21 31 sseldd ⊢ φ → S ⁡ 1 ∈ ℝ *
33 rge0ssre ⊢ 0 +∞ ⊆ ℝ
34 ffvelcdm ⊢ S : ℕ ⟶ 0 +∞ ∧ 1 ∈ ℕ → S ⁡ 1 ∈ 0 +∞
35 18 29 34 sylancl ⊢ φ → S ⁡ 1 ∈ 0 +∞
36 33 35 sselid ⊢ φ → S ⁡ 1 ∈ ℝ
37 36 mnfltd ⊢ φ → −∞ < S ⁡ 1
38 supxrub ⊢ ran ⁡ S ⊆ ℝ * ∧ S ⁡ 1 ∈ ran ⁡ S → S ⁡ 1 ≤ sup ran ⁡ S ℝ * <
39 21 31 38 syl2anc ⊢ φ → S ⁡ 1 ≤ sup ran ⁡ S ℝ * <
40 27 32 23 37 39 xrltletrd ⊢ φ → −∞ < sup ran ⁡ S ℝ * <
41 xrre ⊢ sup ran ⁡ S ℝ * < ∈ ℝ * ∧ vol * ⁡ E + C ∈ ℝ ∧ −∞ < sup ran ⁡ S ℝ * < ∧ sup ran ⁡ S ℝ * < ≤ vol * ⁡ E + C → sup ran ⁡ S ℝ * < ∈ ℝ
42 23 25 40 11 41 syl22anc ⊢ φ → sup ran ⁡ S ℝ * < ∈ ℝ