Metamath Proof Explorer

Theorem ioombl1lem1

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 ioombl1lem1 ( 𝜑 → ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) )

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 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℝ )
17 ovolfcl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
18 9 17 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
19 18 simp1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
20 12 19 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑃 ∈ ℝ )
21 16 20 ifcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∈ ℝ )
22 18 simp2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
23 13 22 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑄 ∈ ℝ )
24 min2 ⊢ ( ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∈ ℝ ∧ 𝑄 ∈ ℝ ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ≤ 𝑄 )
25 21 23 24 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ≤ 𝑄 )
26 df-br ⊢ ( if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ≤ 𝑄 ↔ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ∈ ≤ )
27 25 26 sylib ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ∈ ≤ )
28 21 23 ifcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ )
29 28 23 opelxpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ∈ ( ℝ × ℝ ) )
30 27 29 elind ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
31 30 14 fmptd ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
32 max1 ⊢ ( ( 𝑃 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → 𝑃 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) )
33 20 16 32 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑃 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) )
34 18 simp3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) )
35 34 12 13 3brtr4g ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑃 ≤ 𝑄 )
36 breq2 ⊢ ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) → ( 𝑃 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ↔ 𝑃 ≤ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) )
37 breq2 ⊢ ( 𝑄 = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) → ( 𝑃 ≤ 𝑄 ↔ 𝑃 ≤ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) )
38 36 37 ifboth ⊢ ( ( 𝑃 ≤ if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∧ 𝑃 ≤ 𝑄 ) → 𝑃 ≤ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
39 33 35 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑃 ≤ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
40 df-br ⊢ ( 𝑃 ≤ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ↔ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ∈ ≤ )
41 39 40 sylib ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ∈ ≤ )
42 20 28 opelxpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ∈ ( ℝ × ℝ ) )
43 41 42 elind ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
44 43 15 fmptd ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
45 31 44 jca ⊢ ( 𝜑 → ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) )