| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ovolsca.3 | . . . 4
⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) | 
| 2 |  | ssrab2 4080 | . . . 4
⊢ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴} ⊆ ℝ | 
| 3 | 1, 2 | eqsstrdi 4028 | . . 3
⊢ (𝜑 → 𝐵 ⊆ ℝ) | 
| 4 |  | ovolcl 25513 | . . 3
⊢ (𝐵 ⊆ ℝ →
(vol*‘𝐵) ∈
ℝ*) | 
| 5 | 3, 4 | syl 17 | . 2
⊢ (𝜑 → (vol*‘𝐵) ∈
ℝ*) | 
| 6 |  | ovolsca.7 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 7 |  | ovolfcl 25501 | . . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) | 
| 8 | 6, 7 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) | 
| 9 | 8 | simp3d 1145 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) | 
| 10 | 8 | simp1d 1143 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ) | 
| 11 | 8 | simp2d 1144 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ) | 
| 12 |  | ovolsca.2 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈
ℝ+) | 
| 13 | 12 | rpregt0d 13083 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 < 𝐶)) | 
| 14 | 13 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶)) | 
| 15 |  | lediv1 12133 | . . . . . . . . . . 11
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑛)) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → ((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)) ↔ ((1st
‘(𝐹‘𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) / 𝐶))) | 
| 16 | 10, 11, 14, 15 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)) ↔ ((1st
‘(𝐹‘𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) / 𝐶))) | 
| 17 | 9, 16 | mpbid 232 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) / 𝐶)) | 
| 18 |  | df-br 5144 | . . . . . . . . 9
⊢
(((1st ‘(𝐹‘𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) / 𝐶) ↔ 〈((1st
‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ ≤ ) | 
| 19 | 17, 18 | sylib 218 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ ≤ ) | 
| 20 | 12 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈
ℝ+) | 
| 21 | 10, 20 | rerpdivcld 13108 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) / 𝐶) ∈ ℝ) | 
| 22 | 11, 20 | rerpdivcld 13108 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐹‘𝑛)) / 𝐶) ∈ ℝ) | 
| 23 | 21, 22 | opelxpd 5724 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ (ℝ ×
ℝ)) | 
| 24 | 19, 23 | elind 4200 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ ( ≤ ∩ (ℝ ×
ℝ))) | 
| 25 |  | ovolsca.6 | . . . . . . 7
⊢ 𝐺 = (𝑛 ∈ ℕ ↦
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) | 
| 26 | 24, 25 | fmptd 7134 | . . . . . 6
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 27 |  | eqid 2737 | . . . . . . 7
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) | 
| 28 |  | eqid 2737 | . . . . . . 7
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝐺)) = seq1( + , ((abs ∘ − )
∘ 𝐺)) | 
| 29 | 27, 28 | ovolsf 25507 | . . . . . 6
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘
𝐺)):ℕ⟶(0[,)+∞)) | 
| 30 | 26, 29 | syl 17 | . . . . 5
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐺)):ℕ⟶(0[,)+∞)) | 
| 31 | 30 | frnd 6744 | . . . 4
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ 𝐺)) ⊆ (0[,)+∞)) | 
| 32 |  | icossxr 13472 | . . . 4
⊢
(0[,)+∞) ⊆ ℝ* | 
| 33 | 31, 32 | sstrdi 3996 | . . 3
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ 𝐺)) ⊆
ℝ*) | 
| 34 |  | supxrcl 13357 | . . 3
⊢ (ran
seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* →
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈
ℝ*) | 
| 35 | 33, 34 | syl 17 | . 2
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ∈
ℝ*) | 
| 36 |  | ovolsca.4 | . . . . 5
⊢ (𝜑 → (vol*‘𝐴) ∈
ℝ) | 
| 37 | 36, 12 | rerpdivcld 13108 | . . . 4
⊢ (𝜑 → ((vol*‘𝐴) / 𝐶) ∈ ℝ) | 
| 38 |  | ovolsca.9 | . . . . 5
⊢ (𝜑 → 𝑅 ∈
ℝ+) | 
| 39 | 38 | rpred 13077 | . . . 4
⊢ (𝜑 → 𝑅 ∈ ℝ) | 
| 40 | 37, 39 | readdcld 11290 | . . 3
⊢ (𝜑 → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ) | 
| 41 | 40 | rexrd 11311 | . 2
⊢ (𝜑 → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈
ℝ*) | 
| 42 | 1 | eleq2d 2827 | . . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})) | 
| 43 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐶 · 𝑥) = (𝐶 · 𝑦)) | 
| 44 | 43 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝐶 · 𝑥) ∈ 𝐴 ↔ (𝐶 · 𝑦) ∈ 𝐴)) | 
| 45 | 44 | elrab 3692 | . . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴} ↔ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) | 
| 46 | 42, 45 | bitrdi 287 | . . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴))) | 
| 47 |  | breq2 5147 | . . . . . . . . . . 11
⊢ (𝑥 = (𝐶 · 𝑦) → ((1st ‘(𝐹‘𝑛)) < 𝑥 ↔ (1st ‘(𝐹‘𝑛)) < (𝐶 · 𝑦))) | 
| 48 |  | breq1 5146 | . . . . . . . . . . 11
⊢ (𝑥 = (𝐶 · 𝑦) → (𝑥 < (2nd ‘(𝐹‘𝑛)) ↔ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)))) | 
| 49 | 47, 48 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑥 = (𝐶 · 𝑦) → (((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) ↔ ((1st ‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛))))) | 
| 50 | 49 | rexbidv 3179 | . . . . . . . . 9
⊢ (𝑥 = (𝐶 · 𝑦) → (∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛))))) | 
| 51 |  | ovolsca.8 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ∪ ran
((,) ∘ 𝐹)) | 
| 52 |  | ovolsca.1 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ ℝ) | 
| 53 |  | ovolfioo 25502 | . . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))) | 
| 54 | 52, 6, 53 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))) | 
| 55 | 51, 54 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))) | 
| 56 | 55 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))) | 
| 57 |  | simprr 773 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → (𝐶 · 𝑦) ∈ 𝐴) | 
| 58 | 50, 56, 57 | rspcdva 3623 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)))) | 
| 59 |  | opex 5469 | . . . . . . . . . . . . . . . 16
⊢
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ V | 
| 60 | 25 | fvmpt2 7027 | . . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ ∧
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ V) → (𝐺‘𝑛) = 〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) | 
| 61 | 59, 60 | mpan2 691 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = 〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) | 
| 62 | 61 | fveq2d 6910 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(1st ‘(𝐺‘𝑛)) = (1st
‘〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉)) | 
| 63 |  | ovex 7464 | . . . . . . . . . . . . . . 15
⊢
((1st ‘(𝐹‘𝑛)) / 𝐶) ∈ V | 
| 64 |  | ovex 7464 | . . . . . . . . . . . . . . 15
⊢
((2nd ‘(𝐹‘𝑛)) / 𝐶) ∈ V | 
| 65 | 63, 64 | op1st 8022 | . . . . . . . . . . . . . 14
⊢
(1st ‘〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) = ((1st ‘(𝐹‘𝑛)) / 𝐶) | 
| 66 | 62, 65 | eqtrdi 2793 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(1st ‘(𝐺‘𝑛)) = ((1st ‘(𝐹‘𝑛)) / 𝐶)) | 
| 67 | 66 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘𝑛)) = ((1st
‘(𝐹‘𝑛)) / 𝐶)) | 
| 68 | 67 | breq1d 5153 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐺‘𝑛)) < 𝑦 ↔ ((1st ‘(𝐹‘𝑛)) / 𝐶) < 𝑦)) | 
| 69 | 10 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ) | 
| 70 |  | simplrl 777 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑦 ∈ ℝ) | 
| 71 | 14 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶)) | 
| 72 |  | ltdivmul 12143 | . . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (((1st
‘(𝐹‘𝑛)) / 𝐶) < 𝑦 ↔ (1st ‘(𝐹‘𝑛)) < (𝐶 · 𝑦))) | 
| 73 | 69, 70, 71, 72 | syl3anc 1373 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st
‘(𝐹‘𝑛)) / 𝐶) < 𝑦 ↔ (1st ‘(𝐹‘𝑛)) < (𝐶 · 𝑦))) | 
| 74 | 68, 73 | bitr2d 280 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ↔ (1st ‘(𝐺‘𝑛)) < 𝑦)) | 
| 75 | 11 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ) | 
| 76 |  | ltmuldiv2 12142 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹‘𝑛)) / 𝐶))) | 
| 77 | 70, 75, 71, 76 | syl3anc 1373 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹‘𝑛)) / 𝐶))) | 
| 78 | 61 | fveq2d 6910 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(2nd ‘(𝐺‘𝑛)) = (2nd
‘〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉)) | 
| 79 | 63, 64 | op2nd 8023 | . . . . . . . . . . . . . 14
⊢
(2nd ‘〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) = ((2nd ‘(𝐹‘𝑛)) / 𝐶) | 
| 80 | 78, 79 | eqtrdi 2793 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(2nd ‘(𝐺‘𝑛)) = ((2nd ‘(𝐹‘𝑛)) / 𝐶)) | 
| 81 | 80 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐺‘𝑛)) = ((2nd
‘(𝐹‘𝑛)) / 𝐶)) | 
| 82 | 81 | breq2d 5155 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑦 < (2nd ‘(𝐺‘𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹‘𝑛)) / 𝐶))) | 
| 83 | 77, 82 | bitr4d 282 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)) ↔ 𝑦 < (2nd ‘(𝐺‘𝑛)))) | 
| 84 | 74, 83 | anbi12d 632 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛))) ↔ ((1st ‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) | 
| 85 | 84 | rexbidva 3177 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → (∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) | 
| 86 | 58, 85 | mpbid 232 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛)))) | 
| 87 | 86 | ex 412 | . . . . . 6
⊢ (𝜑 → ((𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴) → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) | 
| 88 | 46, 87 | sylbid 240 | . . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐵 → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) | 
| 89 | 88 | ralrimiv 3145 | . . . 4
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛)))) | 
| 90 |  | ovolfioo 25502 | . . . . 5
⊢ ((𝐵 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) | 
| 91 | 3, 26, 90 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) | 
| 92 | 89, 91 | mpbird 257 | . . 3
⊢ (𝜑 → 𝐵 ⊆ ∪ ran
((,) ∘ 𝐺)) | 
| 93 | 28 | ovollb 25514 | . . 3
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐵 ⊆ ∪ ran
((,) ∘ 𝐺)) →
(vol*‘𝐵) ≤ sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, <
)) | 
| 94 | 26, 92, 93 | syl2anc 584 | . 2
⊢ (𝜑 → (vol*‘𝐵) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, <
)) | 
| 95 |  | fzfid 14014 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin) | 
| 96 | 12 | rpcnd 13079 | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 97 | 96 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ) | 
| 98 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝜑) | 
| 99 |  | elfznn 13593 | . . . . . . . . . 10
⊢ (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ) | 
| 100 | 11, 10 | resubcld 11691 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) ∈
ℝ) | 
| 101 | 98, 99, 100 | syl2an 596 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ∈ ℝ) | 
| 102 | 101 | recnd 11289 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ∈ ℂ) | 
| 103 | 12 | rpne0d 13082 | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ≠ 0) | 
| 104 | 103 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ≠ 0) | 
| 105 | 95, 97, 102, 104 | fsumdivc 15822 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) = Σ𝑛 ∈ (1...𝑘)(((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶)) | 
| 106 | 80, 66 | oveq12d 7449 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛))) = (((2nd ‘(𝐹‘𝑛)) / 𝐶) − ((1st ‘(𝐹‘𝑛)) / 𝐶))) | 
| 107 | 106 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐺‘𝑛)) − (1st
‘(𝐺‘𝑛))) = (((2nd
‘(𝐹‘𝑛)) / 𝐶) − ((1st ‘(𝐹‘𝑛)) / 𝐶))) | 
| 108 | 27 | ovolfsval 25505 | . . . . . . . . . . 11
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛)))) | 
| 109 | 26, 108 | sylan 580 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛)))) | 
| 110 | 11 | recnd 11289 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℂ) | 
| 111 | 10 | recnd 11289 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℂ) | 
| 112 | 12 | rpcnne0d 13086 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) | 
| 113 | 112 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) | 
| 114 |  | divsubdir 11961 | . . . . . . . . . . 11
⊢
(((2nd ‘(𝐹‘𝑛)) ∈ ℂ ∧ (1st
‘(𝐹‘𝑛)) ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) →
(((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) = (((2nd ‘(𝐹‘𝑛)) / 𝐶) − ((1st ‘(𝐹‘𝑛)) / 𝐶))) | 
| 115 | 110, 111,
113, 114 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) / 𝐶) = (((2nd ‘(𝐹‘𝑛)) / 𝐶) − ((1st ‘(𝐹‘𝑛)) / 𝐶))) | 
| 116 | 107, 109,
115 | 3eqtr4d 2787 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = (((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶)) | 
| 117 | 98, 99, 116 | syl2an 596 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((abs ∘ − ) ∘
𝐺)‘𝑛) = (((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶)) | 
| 118 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) | 
| 119 |  | nnuz 12921 | . . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) | 
| 120 | 118, 119 | eleqtrdi 2851 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) | 
| 121 | 100, 20 | rerpdivcld 13108 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) / 𝐶) ∈ ℝ) | 
| 122 | 121 | recnd 11289 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) / 𝐶) ∈ ℂ) | 
| 123 | 98, 99, 122 | syl2an 596 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) ∈ ℂ) | 
| 124 | 117, 120,
123 | fsumser 15766 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)(((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘)) | 
| 125 | 105, 124 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘)) | 
| 126 |  | ovolsca.10 | . . . . . . . . . . 11
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑅))) | 
| 127 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) | 
| 128 |  | ovolsca.5 | . . . . . . . . . . . . . . . 16
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) | 
| 129 | 127, 128 | ovolsf 25507 | . . . . . . . . . . . . . . 15
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) | 
| 130 | 6, 129 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞)) | 
| 131 | 130 | frnd 6744 | . . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞)) | 
| 132 | 131, 32 | sstrdi 3996 | . . . . . . . . . . . 12
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) | 
| 133 | 12, 38 | rpmulcld 13093 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶 · 𝑅) ∈
ℝ+) | 
| 134 | 133 | rpred 13077 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶 · 𝑅) ∈ ℝ) | 
| 135 | 36, 134 | readdcld 11290 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈ ℝ) | 
| 136 | 135 | rexrd 11311 | . . . . . . . . . . . 12
⊢ (𝜑 → ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈
ℝ*) | 
| 137 |  | supxrleub 13368 | . . . . . . . . . . . 12
⊢ ((ran
𝑆 ⊆
ℝ* ∧ ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈ ℝ*) →
(sup(ran 𝑆,
ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) | 
| 138 | 132, 136,
137 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) | 
| 139 | 126, 138 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))) | 
| 140 | 130 | ffnd 6737 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑆 Fn ℕ) | 
| 141 |  | breq1 5146 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝑆‘𝑘) → (𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) | 
| 142 | 141 | ralrn 7108 | . . . . . . . . . . 11
⊢ (𝑆 Fn ℕ →
(∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) | 
| 143 | 140, 142 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) | 
| 144 | 139, 143 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))) | 
| 145 | 144 | r19.21bi 3251 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))) | 
| 146 | 6 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 147 | 127 | ovolfsval 25505 | . . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) | 
| 148 | 146, 99, 147 | syl2an 596 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((abs ∘ − ) ∘
𝐹)‘𝑛) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) | 
| 149 | 148, 120,
102 | fsumser 15766 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘)) | 
| 150 | 128 | fveq1i 6907 | . . . . . . . . 9
⊢ (𝑆‘𝑘) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘) | 
| 151 | 149, 150 | eqtr4di 2795 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) = (𝑆‘𝑘)) | 
| 152 | 37 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → ((vol*‘𝐴) / 𝐶) ∈ ℂ) | 
| 153 | 38 | rpcnd 13079 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ ℂ) | 
| 154 | 96, 152, 153 | adddid 11285 | . . . . . . . . . 10
⊢ (𝜑 → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((𝐶 · ((vol*‘𝐴) / 𝐶)) + (𝐶 · 𝑅))) | 
| 155 | 36 | recnd 11289 | . . . . . . . . . . . 12
⊢ (𝜑 → (vol*‘𝐴) ∈
ℂ) | 
| 156 | 155, 96, 103 | divcan2d 12045 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐶 · ((vol*‘𝐴) / 𝐶)) = (vol*‘𝐴)) | 
| 157 | 156 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐶 · ((vol*‘𝐴) / 𝐶)) + (𝐶 · 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅))) | 
| 158 | 154, 157 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝜑 → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅))) | 
| 159 | 158 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅))) | 
| 160 | 145, 151,
159 | 3brtr4d 5175 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅))) | 
| 161 | 95, 101 | fsumrecl 15770 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ∈ ℝ) | 
| 162 | 40 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ) | 
| 163 | 13 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶)) | 
| 164 |  | ledivmul 12144 | . . . . . . . 8
⊢
((Σ𝑛 ∈
(1...𝑘)((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) ∈ ℝ ∧
(((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)))) | 
| 165 | 161, 162,
163, 164 | syl3anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)))) | 
| 166 | 160, 165 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) | 
| 167 | 125, 166 | eqbrtrrd 5167 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) | 
| 168 | 167 | ralrimiva 3146 | . . . 4
⊢ (𝜑 → ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) | 
| 169 | 30 | ffnd 6737 | . . . . 5
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐺)) Fn
ℕ) | 
| 170 |  | breq1 5146 | . . . . . 6
⊢ (𝑦 = (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑘) → (𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) | 
| 171 | 170 | ralrn 7108 | . . . . 5
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝐺)) Fn ℕ → (∀𝑦 ∈ ran seq1( + , ((abs
∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) | 
| 172 | 169, 171 | syl 17 | . . . 4
⊢ (𝜑 → (∀𝑦 ∈ ran seq1( + , ((abs
∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) | 
| 173 | 168, 172 | mpbird 257 | . . 3
⊢ (𝜑 → ∀𝑦 ∈ ran seq1( + , ((abs ∘ − )
∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) | 
| 174 |  | supxrleub 13368 | . . . 4
⊢ ((ran
seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* ∧
(((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ*) →
(sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ≤
(((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑦 ∈ ran seq1( + , ((abs ∘ − )
∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) | 
| 175 | 33, 41, 174 | syl2anc 584 | . . 3
⊢ (𝜑 → (sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ≤
(((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑦 ∈ ran seq1( + , ((abs ∘ − )
∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) | 
| 176 | 173, 175 | mpbird 257 | . 2
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ≤
(((vol*‘𝐴) / 𝐶) + 𝑅)) | 
| 177 | 5, 35, 41, 94, 176 | xrletrd 13204 | 1
⊢ (𝜑 → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) |