Metamath Proof Explorer

Theorem ioombl1lem1

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 ioombl1lem1 ⊢ φ → G : ℕ ⟶ ≤ ∩ ℝ 2 ∧ H : ℕ ⟶ ≤ ∩ ℝ 2

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 2 adantr ⊢ φ ∧ n ∈ ℕ → A ∈ ℝ
17 ovolfcl ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → 1 st ⁡ F ⁡ n ∈ ℝ ∧ 2 nd ⁡ F ⁡ n ∈ ℝ ∧ 1 st ⁡ F ⁡ n ≤ 2 nd ⁡ F ⁡ n
18 9 17 sylan ⊢ φ ∧ n ∈ ℕ → 1 st ⁡ F ⁡ n ∈ ℝ ∧ 2 nd ⁡ F ⁡ n ∈ ℝ ∧ 1 st ⁡ F ⁡ n ≤ 2 nd ⁡ F ⁡ n
19 18 simp1d ⊢ φ ∧ n ∈ ℕ → 1 st ⁡ F ⁡ n ∈ ℝ
20 12 19 eqeltrid ⊢ φ ∧ n ∈ ℕ → P ∈ ℝ
21 16 20 ifcld ⊢ φ ∧ n ∈ ℕ → if P ≤ A A P ∈ ℝ
22 18 simp2d ⊢ φ ∧ n ∈ ℕ → 2 nd ⁡ F ⁡ n ∈ ℝ
23 13 22 eqeltrid ⊢ φ ∧ n ∈ ℕ → Q ∈ ℝ
24 min2 ⊢ if P ≤ A A P ∈ ℝ ∧ Q ∈ ℝ → if if P ≤ A A P ≤ Q if P ≤ A A P Q ≤ Q
25 21 23 24 syl2anc ⊢ φ ∧ n ∈ ℕ → if if P ≤ A A P ≤ Q if P ≤ A A P Q ≤ Q
26 df-br ⊢ if if P ≤ A A P ≤ Q if P ≤ A A P Q ≤ Q ↔ if if P ≤ A A P ≤ Q if P ≤ A A P Q Q ∈ ≤
27 25 26 sylib ⊢ φ ∧ n ∈ ℕ → if if P ≤ A A P ≤ Q if P ≤ A A P Q Q ∈ ≤
28 21 23 ifcld ⊢ φ ∧ n ∈ ℕ → if if P ≤ A A P ≤ Q if P ≤ A A P Q ∈ ℝ
29 28 23 opelxpd ⊢ φ ∧ n ∈ ℕ → if if P ≤ A A P ≤ Q if P ≤ A A P Q Q ∈ ℝ 2
30 27 29 elind ⊢ φ ∧ n ∈ ℕ → if if P ≤ A A P ≤ Q if P ≤ A A P Q Q ∈ ≤ ∩ ℝ 2
31 30 14 fmptd ⊢ φ → G : ℕ ⟶ ≤ ∩ ℝ 2
32 max1 ⊢ P ∈ ℝ ∧ A ∈ ℝ → P ≤ if P ≤ A A P
33 20 16 32 syl2anc ⊢ φ ∧ n ∈ ℕ → P ≤ if P ≤ A A P
34 18 simp3d ⊢ φ ∧ n ∈ ℕ → 1 st ⁡ F ⁡ n ≤ 2 nd ⁡ F ⁡ n
35 34 12 13 3brtr4g ⊢ φ ∧ n ∈ ℕ → P ≤ Q
36 breq2 ⊢ if P ≤ A A P = if if P ≤ A A P ≤ Q if P ≤ A A P Q → P ≤ if P ≤ A A P ↔ P ≤ if if P ≤ A A P ≤ Q if P ≤ A A P Q
37 breq2 ⊢ Q = if if P ≤ A A P ≤ Q if P ≤ A A P Q → P ≤ Q ↔ P ≤ if if P ≤ A A P ≤ Q if P ≤ A A P Q
38 36 37 ifboth ⊢ P ≤ if P ≤ A A P ∧ P ≤ Q → P ≤ if if P ≤ A A P ≤ Q if P ≤ A A P Q
39 33 35 38 syl2anc ⊢ φ ∧ n ∈ ℕ → P ≤ if if P ≤ A A P ≤ Q if P ≤ A A P Q
40 df-br ⊢ P ≤ if if P ≤ A A P ≤ Q if P ≤ A A P Q ↔ P if if P ≤ A A P ≤ Q if P ≤ A A P Q ∈ ≤
41 39 40 sylib ⊢ φ ∧ n ∈ ℕ → P if if P ≤ A A P ≤ Q if P ≤ A A P Q ∈ ≤
42 20 28 opelxpd ⊢ φ ∧ n ∈ ℕ → P if if P ≤ A A P ≤ Q if P ≤ A A P Q ∈ ℝ 2
43 41 42 elind ⊢ φ ∧ n ∈ ℕ → P if if P ≤ A A P ≤ Q if P ≤ A A P Q ∈ ≤ ∩ ℝ 2
44 43 15 fmptd ⊢ φ → H : ℕ ⟶ ≤ ∩ ℝ 2
45 31 44 jca ⊢ φ → G : ℕ ⟶ ≤ ∩ ℝ 2 ∧ H : ℕ ⟶ ≤ ∩ ℝ 2