Metamath Proof Explorer

Theorem ioombl1lem3

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 ioombl1lem3 ⊢ φ ∧ n ∈ ℕ → abs ∘ − ∘ G ⁡ n + abs ∘ − ∘ H ⁡ n = abs ∘ − ∘ F ⁡ n

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 ovolfcl ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → 1 st ⁡ F ⁡ n ∈ ℝ ∧ 2 nd ⁡ F ⁡ n ∈ ℝ ∧ 1 st ⁡ F ⁡ n ≤ 2 nd ⁡ F ⁡ n
17 9 16 sylan ⊢ φ ∧ n ∈ ℕ → 1 st ⁡ F ⁡ n ∈ ℝ ∧ 2 nd ⁡ F ⁡ n ∈ ℝ ∧ 1 st ⁡ F ⁡ n ≤ 2 nd ⁡ F ⁡ n
18 17 simp2d ⊢ φ ∧ n ∈ ℕ → 2 nd ⁡ F ⁡ n ∈ ℝ
19 13 18 eqeltrid ⊢ φ ∧ n ∈ ℕ → Q ∈ ℝ
20 19 recnd ⊢ φ ∧ n ∈ ℕ → Q ∈ ℂ
21 2 adantr ⊢ φ ∧ n ∈ ℕ → A ∈ ℝ
22 17 simp1d ⊢ φ ∧ n ∈ ℕ → 1 st ⁡ F ⁡ n ∈ ℝ
23 12 22 eqeltrid ⊢ φ ∧ n ∈ ℕ → P ∈ ℝ
24 21 23 ifcld ⊢ φ ∧ n ∈ ℕ → if P ≤ A A P ∈ ℝ
25 24 19 ifcld ⊢ φ ∧ n ∈ ℕ → if if P ≤ A A P ≤ Q if P ≤ A A P Q ∈ ℝ
26 25 recnd ⊢ φ ∧ n ∈ ℕ → if if P ≤ A A P ≤ Q if P ≤ A A P Q ∈ ℂ
27 23 recnd ⊢ φ ∧ n ∈ ℕ → P ∈ ℂ
28 20 26 27 npncand ⊢ φ ∧ n ∈ ℕ → Q − if if P ≤ A A P ≤ Q if P ≤ A A P Q + if if P ≤ A A P ≤ Q if P ≤ A A P Q - P = Q − P
29 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 ioombl1lem1 ⊢ φ → G : ℕ ⟶ ≤ ∩ ℝ 2 ∧ H : ℕ ⟶ ≤ ∩ ℝ 2
30 29 simpld ⊢ φ → G : ℕ ⟶ ≤ ∩ ℝ 2
31 eqid ⊢ abs ∘ − ∘ G = abs ∘ − ∘ G
32 31 ovolfsval ⊢ G : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → abs ∘ − ∘ G ⁡ n = 2 nd ⁡ G ⁡ n − 1 st ⁡ G ⁡ n
33 30 32 sylan ⊢ φ ∧ n ∈ ℕ → abs ∘ − ∘ G ⁡ n = 2 nd ⁡ G ⁡ n − 1 st ⁡ G ⁡ n
34 simpr ⊢ φ ∧ n ∈ ℕ → n ∈ ℕ
35 opex ⊢ if if P ≤ A A P ≤ Q if P ≤ A A P Q Q ∈ V
36 14 fvmpt2 ⊢ n ∈ ℕ ∧ if if P ≤ A A P ≤ Q if P ≤ A A P Q Q ∈ V → G ⁡ n = if if P ≤ A A P ≤ Q if P ≤ A A P Q Q
37 34 35 36 sylancl ⊢ φ ∧ n ∈ ℕ → G ⁡ n = if if P ≤ A A P ≤ Q if P ≤ A A P Q Q
38 37 fveq2d ⊢ φ ∧ n ∈ ℕ → 2 nd ⁡ G ⁡ n = 2 nd ⁡ if if P ≤ A A P ≤ Q if P ≤ A A P Q Q
39 op2ndg ⊢ if if P ≤ A A P ≤ Q if P ≤ A A P Q ∈ ℝ ∧ Q ∈ ℝ → 2 nd ⁡ if if P ≤ A A P ≤ Q if P ≤ A A P Q Q = Q
40 25 19 39 syl2anc ⊢ φ ∧ n ∈ ℕ → 2 nd ⁡ if if P ≤ A A P ≤ Q if P ≤ A A P Q Q = Q
41 38 40 eqtrd ⊢ φ ∧ n ∈ ℕ → 2 nd ⁡ G ⁡ n = Q
42 37 fveq2d ⊢ φ ∧ n ∈ ℕ → 1 st ⁡ G ⁡ n = 1 st ⁡ if if P ≤ A A P ≤ Q if P ≤ A A P Q Q
43 op1stg ⊢ if if P ≤ A A P ≤ Q if P ≤ A A P Q ∈ ℝ ∧ Q ∈ ℝ → 1 st ⁡ 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
44 25 19 43 syl2anc ⊢ φ ∧ n ∈ ℕ → 1 st ⁡ 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
45 42 44 eqtrd ⊢ φ ∧ n ∈ ℕ → 1 st ⁡ G ⁡ n = if if P ≤ A A P ≤ Q if P ≤ A A P Q
46 41 45 oveq12d ⊢ φ ∧ n ∈ ℕ → 2 nd ⁡ G ⁡ n − 1 st ⁡ G ⁡ n = Q − if if P ≤ A A P ≤ Q if P ≤ A A P Q
47 33 46 eqtrd ⊢ φ ∧ n ∈ ℕ → abs ∘ − ∘ G ⁡ n = Q − if if P ≤ A A P ≤ Q if P ≤ A A P Q
48 29 simprd ⊢ φ → H : ℕ ⟶ ≤ ∩ ℝ 2
49 eqid ⊢ abs ∘ − ∘ H = abs ∘ − ∘ H
50 49 ovolfsval ⊢ H : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → abs ∘ − ∘ H ⁡ n = 2 nd ⁡ H ⁡ n − 1 st ⁡ H ⁡ n
51 48 50 sylan ⊢ φ ∧ n ∈ ℕ → abs ∘ − ∘ H ⁡ n = 2 nd ⁡ H ⁡ n − 1 st ⁡ H ⁡ n
52 opex ⊢ P if if P ≤ A A P ≤ Q if P ≤ A A P Q ∈ V
53 15 fvmpt2 ⊢ n ∈ ℕ ∧ P if if P ≤ A A P ≤ Q if P ≤ A A P Q ∈ V → H ⁡ n = P if if P ≤ A A P ≤ Q if P ≤ A A P Q
54 34 52 53 sylancl ⊢ φ ∧ n ∈ ℕ → H ⁡ n = P if if P ≤ A A P ≤ Q if P ≤ A A P Q
55 54 fveq2d ⊢ φ ∧ n ∈ ℕ → 2 nd ⁡ H ⁡ n = 2 nd ⁡ P if if P ≤ A A P ≤ Q if P ≤ A A P Q
56 op2ndg ⊢ P ∈ ℝ ∧ if if P ≤ A A P ≤ Q if P ≤ A A P Q ∈ ℝ → 2 nd ⁡ P if if P ≤ A A P ≤ Q if P ≤ A A P Q = if if P ≤ A A P ≤ Q if P ≤ A A P Q
57 23 25 56 syl2anc ⊢ φ ∧ n ∈ ℕ → 2 nd ⁡ P if if P ≤ A A P ≤ Q if P ≤ A A P Q = if if P ≤ A A P ≤ Q if P ≤ A A P Q
58 55 57 eqtrd ⊢ φ ∧ n ∈ ℕ → 2 nd ⁡ H ⁡ n = if if P ≤ A A P ≤ Q if P ≤ A A P Q
59 54 fveq2d ⊢ φ ∧ n ∈ ℕ → 1 st ⁡ H ⁡ n = 1 st ⁡ P if if P ≤ A A P ≤ Q if P ≤ A A P Q
60 op1stg ⊢ P ∈ ℝ ∧ if if P ≤ A A P ≤ Q if P ≤ A A P Q ∈ ℝ → 1 st ⁡ P if if P ≤ A A P ≤ Q if P ≤ A A P Q = P
61 23 25 60 syl2anc ⊢ φ ∧ n ∈ ℕ → 1 st ⁡ P if if P ≤ A A P ≤ Q if P ≤ A A P Q = P
62 59 61 eqtrd ⊢ φ ∧ n ∈ ℕ → 1 st ⁡ H ⁡ n = P
63 58 62 oveq12d ⊢ φ ∧ n ∈ ℕ → 2 nd ⁡ H ⁡ n − 1 st ⁡ H ⁡ n = if if P ≤ A A P ≤ Q if P ≤ A A P Q − P
64 51 63 eqtrd ⊢ φ ∧ n ∈ ℕ → abs ∘ − ∘ H ⁡ n = if if P ≤ A A P ≤ Q if P ≤ A A P Q − P
65 47 64 oveq12d ⊢ φ ∧ n ∈ ℕ → abs ∘ − ∘ G ⁡ n + abs ∘ − ∘ H ⁡ n = Q − if if P ≤ A A P ≤ Q if P ≤ A A P Q + if if P ≤ A A P ≤ Q if P ≤ A A P Q - P
66 eqid ⊢ abs ∘ − ∘ F = abs ∘ − ∘ F
67 66 ovolfsval ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ n ∈ ℕ → abs ∘ − ∘ F ⁡ n = 2 nd ⁡ F ⁡ n − 1 st ⁡ F ⁡ n
68 9 67 sylan ⊢ φ ∧ n ∈ ℕ → abs ∘ − ∘ F ⁡ n = 2 nd ⁡ F ⁡ n − 1 st ⁡ F ⁡ n
69 13 12 oveq12i ⊢ Q − P = 2 nd ⁡ F ⁡ n − 1 st ⁡ F ⁡ n
70 68 69 eqtr4di ⊢ φ ∧ n ∈ ℕ → abs ∘ − ∘ F ⁡ n = Q − P
71 28 65 70 3eqtr4d ⊢ φ ∧ n ∈ ℕ → abs ∘ − ∘ G ⁡ n + abs ∘ − ∘ H ⁡ n = abs ∘ − ∘ F ⁡ n