Step | Hyp | Ref
| Expression |
1 | | ovolsca.3 |
. . . 4
⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) |
2 | | ssrab2 3912 |
. . . 4
⊢ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴} ⊆ ℝ |
3 | 1, 2 | syl6eqss 3880 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
4 | | ovolcl 23644 |
. . 3
⊢ (𝐵 ⊆ ℝ →
(vol*‘𝐵) ∈
ℝ*) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝜑 → (vol*‘𝐵) ∈
ℝ*) |
6 | | ovolsca.7 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
7 | | ovolfcl 23632 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
8 | 6, 7 | sylan 575 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
9 | 8 | simp3d 1178 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) |
10 | 8 | simp1d 1176 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ) |
11 | 8 | simp2d 1177 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ) |
12 | | ovolsca.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
13 | 12 | rpregt0d 12162 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 < 𝐶)) |
14 | 13 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶)) |
15 | | lediv1 11218 |
. . . . . . . . . . 11
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑛)) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → ((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)) ↔ ((1st
‘(𝐹‘𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) / 𝐶))) |
16 | 10, 11, 14, 15 | syl3anc 1494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)) ↔ ((1st
‘(𝐹‘𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) / 𝐶))) |
17 | 9, 16 | mpbid 224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) / 𝐶)) |
18 | | df-br 4874 |
. . . . . . . . 9
⊢
(((1st ‘(𝐹‘𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) / 𝐶) ↔ 〈((1st
‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ ≤ ) |
19 | 17, 18 | sylib 210 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ ≤ ) |
20 | 12 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈
ℝ+) |
21 | 10, 20 | rerpdivcld 12187 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) / 𝐶) ∈ ℝ) |
22 | 11, 20 | rerpdivcld 12187 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐹‘𝑛)) / 𝐶) ∈ ℝ) |
23 | | opelxpi 5379 |
. . . . . . . . 9
⊢
((((1st ‘(𝐹‘𝑛)) / 𝐶) ∈ ℝ ∧ ((2nd
‘(𝐹‘𝑛)) / 𝐶) ∈ ℝ) →
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ (ℝ ×
ℝ)) |
24 | 21, 22, 23 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ (ℝ ×
ℝ)) |
25 | 19, 24 | elind 4025 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
26 | | ovolsca.6 |
. . . . . . 7
⊢ 𝐺 = (𝑛 ∈ ℕ ↦
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) |
27 | 25, 26 | fmptd 6633 |
. . . . . 6
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
28 | | eqid 2825 |
. . . . . . 7
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) |
29 | | eqid 2825 |
. . . . . . 7
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝐺)) = seq1( + , ((abs ∘ − )
∘ 𝐺)) |
30 | 28, 29 | ovolsf 23638 |
. . . . . 6
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘
𝐺)):ℕ⟶(0[,)+∞)) |
31 | 27, 30 | syl 17 |
. . . . 5
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐺)):ℕ⟶(0[,)+∞)) |
32 | 31 | frnd 6285 |
. . . 4
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ 𝐺)) ⊆ (0[,)+∞)) |
33 | | icossxr 12546 |
. . . 4
⊢
(0[,)+∞) ⊆ ℝ* |
34 | 32, 33 | syl6ss 3839 |
. . 3
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ 𝐺)) ⊆
ℝ*) |
35 | | supxrcl 12433 |
. . 3
⊢ (ran
seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* →
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈
ℝ*) |
36 | 34, 35 | syl 17 |
. 2
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ∈
ℝ*) |
37 | | ovolsca.4 |
. . . . 5
⊢ (𝜑 → (vol*‘𝐴) ∈
ℝ) |
38 | 37, 12 | rerpdivcld 12187 |
. . . 4
⊢ (𝜑 → ((vol*‘𝐴) / 𝐶) ∈ ℝ) |
39 | | ovolsca.9 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
40 | 39 | rpred 12156 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ ℝ) |
41 | 38, 40 | readdcld 10386 |
. . 3
⊢ (𝜑 → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ) |
42 | 41 | rexrd 10406 |
. 2
⊢ (𝜑 → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈
ℝ*) |
43 | 1 | eleq2d 2892 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})) |
44 | | oveq2 6913 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐶 · 𝑥) = (𝐶 · 𝑦)) |
45 | 44 | eleq1d 2891 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝐶 · 𝑥) ∈ 𝐴 ↔ (𝐶 · 𝑦) ∈ 𝐴)) |
46 | 45 | elrab 3585 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴} ↔ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) |
47 | 43, 46 | syl6bb 279 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴))) |
48 | | breq2 4877 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐶 · 𝑦) → ((1st ‘(𝐹‘𝑛)) < 𝑥 ↔ (1st ‘(𝐹‘𝑛)) < (𝐶 · 𝑦))) |
49 | | breq1 4876 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐶 · 𝑦) → (𝑥 < (2nd ‘(𝐹‘𝑛)) ↔ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)))) |
50 | 48, 49 | anbi12d 624 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐶 · 𝑦) → (((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) ↔ ((1st ‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛))))) |
51 | 50 | rexbidv 3262 |
. . . . . . . . 9
⊢ (𝑥 = (𝐶 · 𝑦) → (∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛))))) |
52 | | ovolsca.8 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ∪ ran
((,) ∘ 𝐹)) |
53 | | ovolsca.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
54 | | ovolfioo 23633 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))) |
55 | 53, 6, 54 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))) |
56 | 52, 55 | mpbid 224 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))) |
57 | 56 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))) |
58 | | simprr 789 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → (𝐶 · 𝑦) ∈ 𝐴) |
59 | 51, 57, 58 | rspcdva 3532 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)))) |
60 | | opex 5153 |
. . . . . . . . . . . . . . . 16
⊢
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ V |
61 | 26 | fvmpt2 6538 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ ∧
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ V) → (𝐺‘𝑛) = 〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) |
62 | 60, 61 | mpan2 682 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = 〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) |
63 | 62 | fveq2d 6437 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(1st ‘(𝐺‘𝑛)) = (1st
‘〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉)) |
64 | | ovex 6937 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝐹‘𝑛)) / 𝐶) ∈ V |
65 | | ovex 6937 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(𝐹‘𝑛)) / 𝐶) ∈ V |
66 | 64, 65 | op1st 7436 |
. . . . . . . . . . . . . 14
⊢
(1st ‘〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) = ((1st ‘(𝐹‘𝑛)) / 𝐶) |
67 | 63, 66 | syl6eq 2877 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(1st ‘(𝐺‘𝑛)) = ((1st ‘(𝐹‘𝑛)) / 𝐶)) |
68 | 67 | adantl 475 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘𝑛)) = ((1st
‘(𝐹‘𝑛)) / 𝐶)) |
69 | 68 | breq1d 4883 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐺‘𝑛)) < 𝑦 ↔ ((1st ‘(𝐹‘𝑛)) / 𝐶) < 𝑦)) |
70 | 10 | adantlr 706 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ) |
71 | | simplrl 795 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑦 ∈ ℝ) |
72 | 14 | adantlr 706 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶)) |
73 | | ltdivmul 11228 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (((1st
‘(𝐹‘𝑛)) / 𝐶) < 𝑦 ↔ (1st ‘(𝐹‘𝑛)) < (𝐶 · 𝑦))) |
74 | 70, 71, 72, 73 | syl3anc 1494 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st
‘(𝐹‘𝑛)) / 𝐶) < 𝑦 ↔ (1st ‘(𝐹‘𝑛)) < (𝐶 · 𝑦))) |
75 | 69, 74 | bitr2d 272 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ↔ (1st ‘(𝐺‘𝑛)) < 𝑦)) |
76 | 11 | adantlr 706 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ) |
77 | | ltmuldiv2 11227 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹‘𝑛)) / 𝐶))) |
78 | 71, 76, 72, 77 | syl3anc 1494 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹‘𝑛)) / 𝐶))) |
79 | 62 | fveq2d 6437 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(2nd ‘(𝐺‘𝑛)) = (2nd
‘〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉)) |
80 | 64, 65 | op2nd 7437 |
. . . . . . . . . . . . . 14
⊢
(2nd ‘〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) = ((2nd ‘(𝐹‘𝑛)) / 𝐶) |
81 | 79, 80 | syl6eq 2877 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(2nd ‘(𝐺‘𝑛)) = ((2nd ‘(𝐹‘𝑛)) / 𝐶)) |
82 | 81 | adantl 475 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐺‘𝑛)) = ((2nd
‘(𝐹‘𝑛)) / 𝐶)) |
83 | 82 | breq2d 4885 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑦 < (2nd ‘(𝐺‘𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹‘𝑛)) / 𝐶))) |
84 | 78, 83 | bitr4d 274 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)) ↔ 𝑦 < (2nd ‘(𝐺‘𝑛)))) |
85 | 75, 84 | anbi12d 624 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛))) ↔ ((1st ‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
86 | 85 | rexbidva 3259 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → (∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
87 | 59, 86 | mpbid 224 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛)))) |
88 | 87 | ex 403 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴) → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
89 | 47, 88 | sylbid 232 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐵 → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
90 | 89 | ralrimiv 3174 |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛)))) |
91 | | ovolfioo 23633 |
. . . . 5
⊢ ((𝐵 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
92 | 3, 27, 91 | syl2anc 579 |
. . . 4
⊢ (𝜑 → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
93 | 90, 92 | mpbird 249 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ ∪ ran
((,) ∘ 𝐺)) |
94 | 29 | ovollb 23645 |
. . 3
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐵 ⊆ ∪ ran
((,) ∘ 𝐺)) →
(vol*‘𝐵) ≤ sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, <
)) |
95 | 27, 93, 94 | syl2anc 579 |
. 2
⊢ (𝜑 → (vol*‘𝐵) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, <
)) |
96 | | fzfid 13067 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin) |
97 | 12 | rpcnd 12158 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) |
98 | 97 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ) |
99 | | simpl 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝜑) |
100 | | elfznn 12663 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ) |
101 | 11, 10 | resubcld 10782 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) ∈
ℝ) |
102 | 99, 100, 101 | syl2an 589 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ∈ ℝ) |
103 | 102 | recnd 10385 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ∈ ℂ) |
104 | 12 | rpne0d 12161 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ≠ 0) |
105 | 104 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ≠ 0) |
106 | 96, 98, 103, 105 | fsumdivc 14892 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) = Σ𝑛 ∈ (1...𝑘)(((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶)) |
107 | 81, 67 | oveq12d 6923 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛))) = (((2nd ‘(𝐹‘𝑛)) / 𝐶) − ((1st ‘(𝐹‘𝑛)) / 𝐶))) |
108 | 107 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐺‘𝑛)) − (1st
‘(𝐺‘𝑛))) = (((2nd
‘(𝐹‘𝑛)) / 𝐶) − ((1st ‘(𝐹‘𝑛)) / 𝐶))) |
109 | 28 | ovolfsval 23636 |
. . . . . . . . . . 11
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛)))) |
110 | 27, 109 | sylan 575 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛)))) |
111 | 11 | recnd 10385 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℂ) |
112 | 10 | recnd 10385 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℂ) |
113 | 12 | rpcnne0d 12165 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) |
114 | 113 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) |
115 | | divsubdir 11046 |
. . . . . . . . . . 11
⊢
(((2nd ‘(𝐹‘𝑛)) ∈ ℂ ∧ (1st
‘(𝐹‘𝑛)) ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) →
(((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) = (((2nd ‘(𝐹‘𝑛)) / 𝐶) − ((1st ‘(𝐹‘𝑛)) / 𝐶))) |
116 | 111, 112,
114, 115 | syl3anc 1494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) / 𝐶) = (((2nd ‘(𝐹‘𝑛)) / 𝐶) − ((1st ‘(𝐹‘𝑛)) / 𝐶))) |
117 | 108, 110,
116 | 3eqtr4d 2871 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = (((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶)) |
118 | 99, 100, 117 | syl2an 589 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((abs ∘ − ) ∘
𝐺)‘𝑛) = (((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶)) |
119 | | simpr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
120 | | nnuz 12005 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
121 | 119, 120 | syl6eleq 2916 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
122 | 101, 20 | rerpdivcld 12187 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) / 𝐶) ∈ ℝ) |
123 | 122 | recnd 10385 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) / 𝐶) ∈ ℂ) |
124 | 99, 100, 123 | syl2an 589 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) ∈ ℂ) |
125 | 118, 121,
124 | fsumser 14838 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)(((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘)) |
126 | 106, 125 | eqtrd 2861 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘)) |
127 | | ovolsca.10 |
. . . . . . . . . . 11
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑅))) |
128 | | eqid 2825 |
. . . . . . . . . . . . . . . 16
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) |
129 | | ovolsca.5 |
. . . . . . . . . . . . . . . 16
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
130 | 128, 129 | ovolsf 23638 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
131 | 6, 130 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞)) |
132 | 131 | frnd 6285 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞)) |
133 | 132, 33 | syl6ss 3839 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
134 | 12, 39 | rpmulcld 12172 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶 · 𝑅) ∈
ℝ+) |
135 | 134 | rpred 12156 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶 · 𝑅) ∈ ℝ) |
136 | 37, 135 | readdcld 10386 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈ ℝ) |
137 | 136 | rexrd 10406 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈
ℝ*) |
138 | | supxrleub 12444 |
. . . . . . . . . . . 12
⊢ ((ran
𝑆 ⊆
ℝ* ∧ ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈ ℝ*) →
(sup(ran 𝑆,
ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) |
139 | 133, 137,
138 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) |
140 | 127, 139 | mpbid 224 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))) |
141 | 131 | ffnd 6279 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 Fn ℕ) |
142 | | breq1 4876 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑆‘𝑘) → (𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) |
143 | 142 | ralrn 6611 |
. . . . . . . . . . 11
⊢ (𝑆 Fn ℕ →
(∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) |
144 | 141, 143 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) |
145 | 140, 144 | mpbid 224 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))) |
146 | 145 | r19.21bi 3141 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))) |
147 | 6 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
148 | 128 | ovolfsval 23636 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) |
149 | 147, 100,
148 | syl2an 589 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((abs ∘ − ) ∘
𝐹)‘𝑛) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) |
150 | 149, 121,
103 | fsumser 14838 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘)) |
151 | 129 | fveq1i 6434 |
. . . . . . . . 9
⊢ (𝑆‘𝑘) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘) |
152 | 150, 151 | syl6eqr 2879 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) = (𝑆‘𝑘)) |
153 | 38 | recnd 10385 |
. . . . . . . . . . 11
⊢ (𝜑 → ((vol*‘𝐴) / 𝐶) ∈ ℂ) |
154 | 39 | rpcnd 12158 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ ℂ) |
155 | 97, 153, 154 | adddid 10381 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((𝐶 · ((vol*‘𝐴) / 𝐶)) + (𝐶 · 𝑅))) |
156 | 37 | recnd 10385 |
. . . . . . . . . . . 12
⊢ (𝜑 → (vol*‘𝐴) ∈
ℂ) |
157 | 156, 97, 104 | divcan2d 11129 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 · ((vol*‘𝐴) / 𝐶)) = (vol*‘𝐴)) |
158 | 157 | oveq1d 6920 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 · ((vol*‘𝐴) / 𝐶)) + (𝐶 · 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅))) |
159 | 155, 158 | eqtrd 2861 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅))) |
160 | 159 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅))) |
161 | 146, 152,
160 | 3brtr4d 4905 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅))) |
162 | 96, 102 | fsumrecl 14842 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ∈ ℝ) |
163 | 41 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ) |
164 | 13 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶)) |
165 | | ledivmul 11229 |
. . . . . . . 8
⊢
((Σ𝑛 ∈
(1...𝑘)((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) ∈ ℝ ∧
(((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)))) |
166 | 162, 163,
164, 165 | syl3anc 1494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)))) |
167 | 161, 166 | mpbird 249 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) |
168 | 126, 167 | eqbrtrrd 4897 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) |
169 | 168 | ralrimiva 3175 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) |
170 | 31 | ffnd 6279 |
. . . . 5
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐺)) Fn
ℕ) |
171 | | breq1 4876 |
. . . . . 6
⊢ (𝑦 = (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑘) → (𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) |
172 | 171 | ralrn 6611 |
. . . . 5
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝐺)) Fn ℕ → (∀𝑦 ∈ ran seq1( + , ((abs
∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) |
173 | 170, 172 | syl 17 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ ran seq1( + , ((abs
∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) |
174 | 169, 173 | mpbird 249 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ ran seq1( + , ((abs ∘ − )
∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) |
175 | | supxrleub 12444 |
. . . 4
⊢ ((ran
seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* ∧
(((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ*) →
(sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ≤
(((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑦 ∈ ran seq1( + , ((abs ∘ − )
∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) |
176 | 34, 42, 175 | syl2anc 579 |
. . 3
⊢ (𝜑 → (sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ≤
(((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑦 ∈ ran seq1( + , ((abs ∘ − )
∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) |
177 | 174, 176 | mpbird 249 |
. 2
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ≤
(((vol*‘𝐴) / 𝐶) + 𝑅)) |
178 | 5, 36, 42, 95, 177 | xrletrd 12281 |
1
⊢ (𝜑 → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) |