Proof of Theorem ioombl1lem3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ioombl1.q | . . . . 5
⊢ 𝑄 = (2nd ‘(𝐹‘𝑛)) | 
| 2 |  | ioombl1.f1 | . . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 3 |  | ovolfcl 25501 | . . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) | 
| 4 | 2, 3 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) | 
| 5 | 4 | simp2d 1144 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ) | 
| 6 | 1, 5 | eqeltrid 2845 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ) | 
| 7 | 6 | recnd 11289 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℂ) | 
| 8 |  | ioombl1.a | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 9 | 8 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ) | 
| 10 |  | ioombl1.p | . . . . . . 7
⊢ 𝑃 = (1st ‘(𝐹‘𝑛)) | 
| 11 | 4 | simp1d 1143 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ) | 
| 12 | 10, 11 | eqeltrid 2845 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ) | 
| 13 | 9, 12 | ifcld 4572 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ) | 
| 14 | 13, 6 | ifcld 4572 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) | 
| 15 | 14 | recnd 11289 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℂ) | 
| 16 | 12 | recnd 11289 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℂ) | 
| 17 | 7, 15, 16 | npncand 11644 | . 2
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑄 − if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)) + (if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) − 𝑃)) = (𝑄 − 𝑃)) | 
| 18 |  | ioombl1.b | . . . . . . 7
⊢ 𝐵 = (𝐴(,)+∞) | 
| 19 |  | ioombl1.e | . . . . . . 7
⊢ (𝜑 → 𝐸 ⊆ ℝ) | 
| 20 |  | ioombl1.v | . . . . . . 7
⊢ (𝜑 → (vol*‘𝐸) ∈
ℝ) | 
| 21 |  | ioombl1.c | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈
ℝ+) | 
| 22 |  | ioombl1.s | . . . . . . 7
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) | 
| 23 |  | ioombl1.t | . . . . . . 7
⊢ 𝑇 = seq1( + , ((abs ∘
− ) ∘ 𝐺)) | 
| 24 |  | ioombl1.u | . . . . . . 7
⊢ 𝑈 = seq1( + , ((abs ∘
− ) ∘ 𝐻)) | 
| 25 |  | ioombl1.f2 | . . . . . . 7
⊢ (𝜑 → 𝐸 ⊆ ∪ ran
((,) ∘ 𝐹)) | 
| 26 |  | ioombl1.f3 | . . . . . . 7
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐸) + 𝐶)) | 
| 27 |  | ioombl1.g | . . . . . . 7
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉) | 
| 28 |  | ioombl1.h | . . . . . . 7
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ 〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉) | 
| 29 | 18, 8, 19, 20, 21, 22, 23, 24, 2, 25, 26, 10, 1, 27, 28 | ioombl1lem1 25593 | . . . . . 6
⊢ (𝜑 → (𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ)))) | 
| 30 | 29 | simpld 494 | . . . . 5
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 31 |  | eqid 2737 | . . . . . 6
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) | 
| 32 | 31 | ovolfsval 25505 | . . . . 5
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛)))) | 
| 33 | 30, 32 | sylan 580 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛)))) | 
| 34 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) | 
| 35 |  | opex 5469 | . . . . . . . 8
⊢
〈if(if(𝑃 ≤
𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉 ∈ V | 
| 36 | 27 | fvmpt2 7027 | . . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧
〈if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉 ∈ V) → (𝐺‘𝑛) = 〈if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉) | 
| 37 | 34, 35, 36 | sylancl 586 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = 〈if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉) | 
| 38 | 37 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐺‘𝑛)) = (2nd
‘〈if(if(𝑃 ≤
𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉)) | 
| 39 |  | op2ndg 8027 | . . . . . . 7
⊢
((if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (2nd
‘〈if(if(𝑃 ≤
𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉) = 𝑄) | 
| 40 | 14, 6, 39 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘〈if(if(𝑃 ≤
𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉) = 𝑄) | 
| 41 | 38, 40 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐺‘𝑛)) = 𝑄) | 
| 42 | 37 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘𝑛)) = (1st
‘〈if(if(𝑃 ≤
𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉)) | 
| 43 |  | op1stg 8026 | . . . . . . 7
⊢
((if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (1st
‘〈if(if(𝑃 ≤
𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)) | 
| 44 | 14, 6, 43 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘〈if(if(𝑃 ≤
𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄〉) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)) | 
| 45 | 42, 44 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)) | 
| 46 | 41, 45 | oveq12d 7449 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐺‘𝑛)) − (1st
‘(𝐺‘𝑛))) = (𝑄 − if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))) | 
| 47 | 33, 46 | eqtrd 2777 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = (𝑄 − if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))) | 
| 48 | 29 | simprd 495 | . . . . 5
⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 49 |  | eqid 2737 | . . . . . 6
⊢ ((abs
∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻) | 
| 50 | 49 | ovolfsval 25505 | . . . . 5
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘𝑛) = ((2nd ‘(𝐻‘𝑛)) − (1st ‘(𝐻‘𝑛)))) | 
| 51 | 48, 50 | sylan 580 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘𝑛) = ((2nd ‘(𝐻‘𝑛)) − (1st ‘(𝐻‘𝑛)))) | 
| 52 |  | opex 5469 | . . . . . . . 8
⊢
〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉 ∈ V | 
| 53 | 28 | fvmpt2 7027 | . . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧
〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉 ∈ V) → (𝐻‘𝑛) = 〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉) | 
| 54 | 34, 52, 53 | sylancl 586 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐻‘𝑛) = 〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉) | 
| 55 | 54 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐻‘𝑛)) = (2nd
‘〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉)) | 
| 56 |  | op2ndg 8027 | . . . . . . 7
⊢ ((𝑃 ∈ ℝ ∧
if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (2nd
‘〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)) | 
| 57 | 12, 14, 56 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)) | 
| 58 | 55, 57 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐻‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)) | 
| 59 | 54 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐻‘𝑛)) = (1st
‘〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉)) | 
| 60 |  | op1stg 8026 | . . . . . . 7
⊢ ((𝑃 ∈ ℝ ∧
if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (1st
‘〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉) = 𝑃) | 
| 61 | 12, 14, 60 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘〈𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)〉) = 𝑃) | 
| 62 | 59, 61 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐻‘𝑛)) = 𝑃) | 
| 63 | 58, 62 | oveq12d 7449 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐻‘𝑛)) − (1st
‘(𝐻‘𝑛))) = (if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) − 𝑃)) | 
| 64 | 51, 63 | eqtrd 2777 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘𝑛) = (if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) − 𝑃)) | 
| 65 | 47, 64 | oveq12d 7449 | . 2
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘
− ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)) = ((𝑄 − if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)) + (if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) − 𝑃))) | 
| 66 |  | eqid 2737 | . . . . 5
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) | 
| 67 | 66 | ovolfsval 25505 | . . . 4
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) | 
| 68 | 2, 67 | sylan 580 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) | 
| 69 | 1, 10 | oveq12i 7443 | . . 3
⊢ (𝑄 − 𝑃) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) | 
| 70 | 68, 69 | eqtr4di 2795 | . 2
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑛) = (𝑄 − 𝑃)) | 
| 71 | 17, 65, 70 | 3eqtr4d 2787 | 1
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘
− ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)) = (((abs ∘ − ) ∘ 𝐹)‘𝑛)) |