Step | Hyp | Ref
| Expression |
1 | | ovolsca.3 |
. . . 4
⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) |
2 | | ssrab2 3687 |
. . . 4
⊢ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴} ⊆ ℝ |
3 | 1, 2 | syl6eqss 3655 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
4 | | ovolcl 23246 |
. . 3
⊢ (𝐵 ⊆ ℝ →
(vol*‘𝐵) ∈
ℝ*) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝜑 → (vol*‘𝐵) ∈
ℝ*) |
6 | | ovolsca.7 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
7 | | ovolfcl 23235 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
8 | 6, 7 | sylan 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
9 | 8 | simp3d 1075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) |
10 | 8 | simp1d 1073 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ) |
11 | 8 | simp2d 1074 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ) |
12 | | ovolsca.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
13 | 12 | rpregt0d 11878 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 < 𝐶)) |
14 | 13 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶)) |
15 | | lediv1 10888 |
. . . . . . . . . . 11
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑛)) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → ((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)) ↔ ((1st
‘(𝐹‘𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) / 𝐶))) |
16 | 10, 11, 14, 15 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)) ↔ ((1st
‘(𝐹‘𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) / 𝐶))) |
17 | 9, 16 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) / 𝐶)) |
18 | | df-br 4654 |
. . . . . . . . 9
⊢
(((1st ‘(𝐹‘𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) / 𝐶) ↔ 〈((1st
‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ ≤ ) |
19 | 17, 18 | sylib 208 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ ≤ ) |
20 | 12 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈
ℝ+) |
21 | 10, 20 | rerpdivcld 11903 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) / 𝐶) ∈ ℝ) |
22 | 11, 20 | rerpdivcld 11903 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐹‘𝑛)) / 𝐶) ∈ ℝ) |
23 | | opelxpi 5148 |
. . . . . . . . 9
⊢
((((1st ‘(𝐹‘𝑛)) / 𝐶) ∈ ℝ ∧ ((2nd
‘(𝐹‘𝑛)) / 𝐶) ∈ ℝ) →
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ (ℝ ×
ℝ)) |
24 | 21, 22, 23 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ (ℝ ×
ℝ)) |
25 | 19, 24 | elind 3798 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
26 | | ovolsca.6 |
. . . . . . 7
⊢ 𝐺 = (𝑛 ∈ ℕ ↦
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) |
27 | 25, 26 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
28 | | eqid 2622 |
. . . . . . 7
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) |
29 | | eqid 2622 |
. . . . . . 7
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝐺)) = seq1( + , ((abs ∘ − )
∘ 𝐺)) |
30 | 28, 29 | ovolsf 23241 |
. . . . . 6
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘
𝐺)):ℕ⟶(0[,)+∞)) |
31 | 27, 30 | syl 17 |
. . . . 5
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐺)):ℕ⟶(0[,)+∞)) |
32 | | frn 6053 |
. . . . 5
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞) → ran
seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ (0[,)+∞)) |
33 | 31, 32 | syl 17 |
. . . 4
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ 𝐺)) ⊆ (0[,)+∞)) |
34 | | icossxr 12258 |
. . . 4
⊢
(0[,)+∞) ⊆ ℝ* |
35 | 33, 34 | syl6ss 3615 |
. . 3
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ 𝐺)) ⊆
ℝ*) |
36 | | supxrcl 12145 |
. . 3
⊢ (ran
seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* →
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈
ℝ*) |
37 | 35, 36 | syl 17 |
. 2
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ∈
ℝ*) |
38 | | ovolsca.4 |
. . . . 5
⊢ (𝜑 → (vol*‘𝐴) ∈
ℝ) |
39 | 38, 12 | rerpdivcld 11903 |
. . . 4
⊢ (𝜑 → ((vol*‘𝐴) / 𝐶) ∈ ℝ) |
40 | | ovolsca.9 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
41 | 40 | rpred 11872 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ ℝ) |
42 | 39, 41 | readdcld 10069 |
. . 3
⊢ (𝜑 → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ) |
43 | 42 | rexrd 10089 |
. 2
⊢ (𝜑 → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈
ℝ*) |
44 | 1 | eleq2d 2687 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})) |
45 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐶 · 𝑥) = (𝐶 · 𝑦)) |
46 | 45 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝐶 · 𝑥) ∈ 𝐴 ↔ (𝐶 · 𝑦) ∈ 𝐴)) |
47 | 46 | elrab 3363 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴} ↔ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) |
48 | 44, 47 | syl6bb 276 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴))) |
49 | | simprr 796 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → (𝐶 · 𝑦) ∈ 𝐴) |
50 | | ovolsca.8 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ∪ ran
((,) ∘ 𝐹)) |
51 | | ovolsca.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
52 | | ovolfioo 23236 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))) |
53 | 51, 6, 52 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))) |
54 | 50, 53 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))) |
55 | 54 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))) |
56 | | breq2 4657 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐶 · 𝑦) → ((1st ‘(𝐹‘𝑛)) < 𝑥 ↔ (1st ‘(𝐹‘𝑛)) < (𝐶 · 𝑦))) |
57 | | breq1 4656 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐶 · 𝑦) → (𝑥 < (2nd ‘(𝐹‘𝑛)) ↔ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)))) |
58 | 56, 57 | anbi12d 747 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐶 · 𝑦) → (((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) ↔ ((1st ‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛))))) |
59 | 58 | rexbidv 3052 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐶 · 𝑦) → (∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛))))) |
60 | 59 | rspcv 3305 |
. . . . . . . . 9
⊢ ((𝐶 · 𝑦) ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛))))) |
61 | 49, 55, 60 | sylc 65 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)))) |
62 | | opex 4932 |
. . . . . . . . . . . . . . . 16
⊢
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ V |
63 | 26 | fvmpt2 6291 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ ∧
〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉 ∈ V) → (𝐺‘𝑛) = 〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) |
64 | 62, 63 | mpan2 707 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = 〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) |
65 | 64 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(1st ‘(𝐺‘𝑛)) = (1st
‘〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉)) |
66 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝐹‘𝑛)) / 𝐶) ∈ V |
67 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(𝐹‘𝑛)) / 𝐶) ∈ V |
68 | 66, 67 | op1st 7176 |
. . . . . . . . . . . . . 14
⊢
(1st ‘〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) = ((1st ‘(𝐹‘𝑛)) / 𝐶) |
69 | 65, 68 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(1st ‘(𝐺‘𝑛)) = ((1st ‘(𝐹‘𝑛)) / 𝐶)) |
70 | 69 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘𝑛)) = ((1st
‘(𝐹‘𝑛)) / 𝐶)) |
71 | 70 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐺‘𝑛)) < 𝑦 ↔ ((1st ‘(𝐹‘𝑛)) / 𝐶) < 𝑦)) |
72 | 10 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ) |
73 | | simplrl 800 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑦 ∈ ℝ) |
74 | 14 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶)) |
75 | | ltdivmul 10898 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (((1st
‘(𝐹‘𝑛)) / 𝐶) < 𝑦 ↔ (1st ‘(𝐹‘𝑛)) < (𝐶 · 𝑦))) |
76 | 72, 73, 74, 75 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st
‘(𝐹‘𝑛)) / 𝐶) < 𝑦 ↔ (1st ‘(𝐹‘𝑛)) < (𝐶 · 𝑦))) |
77 | 71, 76 | bitr2d 269 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ↔ (1st ‘(𝐺‘𝑛)) < 𝑦)) |
78 | 11 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ) |
79 | | ltmuldiv2 10897 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹‘𝑛)) / 𝐶))) |
80 | 73, 78, 74, 79 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹‘𝑛)) / 𝐶))) |
81 | 64 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(2nd ‘(𝐺‘𝑛)) = (2nd
‘〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉)) |
82 | 66, 67 | op2nd 7177 |
. . . . . . . . . . . . . 14
⊢
(2nd ‘〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) = ((2nd ‘(𝐹‘𝑛)) / 𝐶) |
83 | 81, 82 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(2nd ‘(𝐺‘𝑛)) = ((2nd ‘(𝐹‘𝑛)) / 𝐶)) |
84 | 83 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐺‘𝑛)) = ((2nd
‘(𝐹‘𝑛)) / 𝐶)) |
85 | 84 | breq2d 4665 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑦 < (2nd ‘(𝐺‘𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹‘𝑛)) / 𝐶))) |
86 | 80, 85 | bitr4d 271 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛)) ↔ 𝑦 < (2nd ‘(𝐺‘𝑛)))) |
87 | 77, 86 | anbi12d 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛))) ↔ ((1st ‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
88 | 87 | rexbidva 3049 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → (∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹‘𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
89 | 61, 88 | mpbid 222 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛)))) |
90 | 89 | ex 450 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴) → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
91 | 48, 90 | sylbid 230 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐵 → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
92 | 91 | ralrimiv 2965 |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛)))) |
93 | | ovolfioo 23236 |
. . . . 5
⊢ ((𝐵 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
94 | 3, 27, 93 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
95 | 92, 94 | mpbird 247 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ ∪ ran
((,) ∘ 𝐺)) |
96 | 29 | ovollb 23247 |
. . 3
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐵 ⊆ ∪ ran
((,) ∘ 𝐺)) →
(vol*‘𝐵) ≤ sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, <
)) |
97 | 27, 95, 96 | syl2anc 693 |
. 2
⊢ (𝜑 → (vol*‘𝐵) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, <
)) |
98 | | fzfid 12772 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin) |
99 | 12 | rpcnd 11874 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) |
100 | 99 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ) |
101 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝜑) |
102 | | elfznn 12370 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ) |
103 | 11, 10 | resubcld 10458 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) ∈
ℝ) |
104 | 101, 102,
103 | syl2an 494 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ∈ ℝ) |
105 | 104 | recnd 10068 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ∈ ℂ) |
106 | 12 | rpne0d 11877 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ≠ 0) |
107 | 106 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ≠ 0) |
108 | 98, 100, 105, 107 | fsumdivc 14518 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) = Σ𝑛 ∈ (1...𝑘)(((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶)) |
109 | 83, 69 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛))) = (((2nd ‘(𝐹‘𝑛)) / 𝐶) − ((1st ‘(𝐹‘𝑛)) / 𝐶))) |
110 | 109 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐺‘𝑛)) − (1st
‘(𝐺‘𝑛))) = (((2nd
‘(𝐹‘𝑛)) / 𝐶) − ((1st ‘(𝐹‘𝑛)) / 𝐶))) |
111 | 28 | ovolfsval 23239 |
. . . . . . . . . . 11
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛)))) |
112 | 27, 111 | sylan 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛)))) |
113 | 11 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℂ) |
114 | 10 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℂ) |
115 | 12 | rpcnne0d 11881 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) |
116 | 115 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) |
117 | | divsubdir 10721 |
. . . . . . . . . . 11
⊢
(((2nd ‘(𝐹‘𝑛)) ∈ ℂ ∧ (1st
‘(𝐹‘𝑛)) ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) →
(((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) = (((2nd ‘(𝐹‘𝑛)) / 𝐶) − ((1st ‘(𝐹‘𝑛)) / 𝐶))) |
118 | 113, 114,
116, 117 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) / 𝐶) = (((2nd ‘(𝐹‘𝑛)) / 𝐶) − ((1st ‘(𝐹‘𝑛)) / 𝐶))) |
119 | 110, 112,
118 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = (((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶)) |
120 | 101, 102,
119 | syl2an 494 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((abs ∘ − ) ∘
𝐺)‘𝑛) = (((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶)) |
121 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
122 | | nnuz 11723 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
123 | 121, 122 | syl6eleq 2711 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
124 | 103, 20 | rerpdivcld 11903 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) / 𝐶) ∈ ℝ) |
125 | 124 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) / 𝐶) ∈ ℂ) |
126 | 101, 102,
125 | syl2an 494 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) ∈ ℂ) |
127 | 120, 123,
126 | fsumser 14461 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)(((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘)) |
128 | 108, 127 | eqtrd 2656 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘)) |
129 | | ovolsca.10 |
. . . . . . . . . . 11
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑅))) |
130 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) |
131 | | ovolsca.5 |
. . . . . . . . . . . . . . . 16
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
132 | 130, 131 | ovolsf 23241 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
133 | 6, 132 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞)) |
134 | | frn 6053 |
. . . . . . . . . . . . . 14
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ ran 𝑆 ⊆
(0[,)+∞)) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞)) |
136 | 135, 34 | syl6ss 3615 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
137 | 12, 40 | rpmulcld 11888 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶 · 𝑅) ∈
ℝ+) |
138 | 137 | rpred 11872 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶 · 𝑅) ∈ ℝ) |
139 | 38, 138 | readdcld 10069 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈ ℝ) |
140 | 139 | rexrd 10089 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈
ℝ*) |
141 | | supxrleub 12156 |
. . . . . . . . . . . 12
⊢ ((ran
𝑆 ⊆
ℝ* ∧ ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈ ℝ*) →
(sup(ran 𝑆,
ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) |
142 | 136, 140,
141 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) |
143 | 129, 142 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))) |
144 | | ffn 6045 |
. . . . . . . . . . . 12
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ 𝑆 Fn
ℕ) |
145 | 133, 144 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 Fn ℕ) |
146 | | breq1 4656 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑆‘𝑘) → (𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) |
147 | 146 | ralrn 6362 |
. . . . . . . . . . 11
⊢ (𝑆 Fn ℕ →
(∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) |
148 | 145, 147 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))) |
149 | 143, 148 | mpbid 222 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))) |
150 | 149 | r19.21bi 2932 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))) |
151 | 6 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
152 | 130 | ovolfsval 23239 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) |
153 | 151, 102,
152 | syl2an 494 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((abs ∘ − ) ∘
𝐹)‘𝑛) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) |
154 | 153, 123,
105 | fsumser 14461 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘)) |
155 | 131 | fveq1i 6192 |
. . . . . . . . 9
⊢ (𝑆‘𝑘) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘) |
156 | 154, 155 | syl6eqr 2674 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) = (𝑆‘𝑘)) |
157 | 39 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝜑 → ((vol*‘𝐴) / 𝐶) ∈ ℂ) |
158 | 40 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ ℂ) |
159 | 99, 157, 158 | adddid 10064 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((𝐶 · ((vol*‘𝐴) / 𝐶)) + (𝐶 · 𝑅))) |
160 | 38 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝜑 → (vol*‘𝐴) ∈
ℂ) |
161 | 160, 99, 106 | divcan2d 10803 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 · ((vol*‘𝐴) / 𝐶)) = (vol*‘𝐴)) |
162 | 161 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 · ((vol*‘𝐴) / 𝐶)) + (𝐶 · 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅))) |
163 | 159, 162 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅))) |
164 | 163 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅))) |
165 | 150, 156,
164 | 3brtr4d 4685 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅))) |
166 | 98, 104 | fsumrecl 14465 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ∈ ℝ) |
167 | 42 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ) |
168 | 13 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶)) |
169 | | ledivmul 10899 |
. . . . . . . 8
⊢
((Σ𝑛 ∈
(1...𝑘)((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛))) ∈ ℝ ∧
(((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)))) |
170 | 166, 167,
168, 169 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)))) |
171 | 165, 170 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) |
172 | 128, 171 | eqbrtrrd 4677 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) |
173 | 172 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) |
174 | | ffn 6045 |
. . . . . 6
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞) →
seq1( + , ((abs ∘ − ) ∘ 𝐺)) Fn ℕ) |
175 | 31, 174 | syl 17 |
. . . . 5
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐺)) Fn
ℕ) |
176 | | breq1 4656 |
. . . . . 6
⊢ (𝑦 = (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑘) → (𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) |
177 | 176 | ralrn 6362 |
. . . . 5
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝐺)) Fn ℕ → (∀𝑦 ∈ ran seq1( + , ((abs
∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) |
178 | 175, 177 | syl 17 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ ran seq1( + , ((abs
∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) |
179 | 173, 178 | mpbird 247 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ ran seq1( + , ((abs ∘ − )
∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) |
180 | | supxrleub 12156 |
. . . 4
⊢ ((ran
seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* ∧
(((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ*) →
(sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ≤
(((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑦 ∈ ran seq1( + , ((abs ∘ − )
∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) |
181 | 35, 43, 180 | syl2anc 693 |
. . 3
⊢ (𝜑 → (sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ≤
(((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑦 ∈ ran seq1( + , ((abs ∘ − )
∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))) |
182 | 179, 181 | mpbird 247 |
. 2
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ≤
(((vol*‘𝐴) / 𝐶) + 𝑅)) |
183 | 5, 37, 43, 97, 182 | xrletrd 11993 |
1
⊢ (𝜑 → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) |