Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) →
𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) |
2 | | ovolficcss 23045 |
. . . . . . . 8
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐹) ⊆
ℝ) |
3 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) →
∪ ran ([,] ∘ 𝐹) ⊆ ℝ) |
4 | 1, 3 | sstrd 3578 |
. . . . . 6
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) →
𝐴 ⊆
ℝ) |
5 | | ovolcl 23053 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ →
(vol*‘𝐴) ∈
ℝ*) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) →
(vol*‘𝐴) ∈
ℝ*) |
7 | 6 | adantr 480 |
. . . 4
⊢ (((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) = +∞) → (vol*‘𝐴) ∈
ℝ*) |
8 | | pnfge 11840 |
. . . 4
⊢
((vol*‘𝐴)
∈ ℝ* → (vol*‘𝐴) ≤ +∞) |
9 | 7, 8 | syl 17 |
. . 3
⊢ (((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) = +∞) → (vol*‘𝐴) ≤ +∞) |
10 | | simpr 476 |
. . 3
⊢ (((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) = +∞) → sup(ran 𝑆, ℝ*, < ) =
+∞) |
11 | 9, 10 | breqtrrd 4611 |
. 2
⊢ (((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) = +∞) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, <
)) |
12 | | eqid 2610 |
. . . . . . . . 9
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) |
13 | | ovollb2.1 |
. . . . . . . . 9
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
14 | 12, 13 | ovolsf 23048 |
. . . . . . . 8
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) →
𝑆:ℕ⟶(0[,)+∞)) |
16 | | frn 5966 |
. . . . . . 7
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ ran 𝑆 ⊆
(0[,)+∞)) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) → ran
𝑆 ⊆
(0[,)+∞)) |
18 | | rge0ssre 12151 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℝ |
19 | 17, 18 | syl6ss 3580 |
. . . . 5
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) → ran
𝑆 ⊆
ℝ) |
20 | | 1nn 10908 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
21 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ dom 𝑆 =
ℕ) |
22 | 15, 21 | syl 17 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) → dom
𝑆 =
ℕ) |
23 | 20, 22 | syl5eleqr 2695 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) → 1
∈ dom 𝑆) |
24 | | ne0i 3880 |
. . . . . . 7
⊢ (1 ∈
dom 𝑆 → dom 𝑆 ≠ ∅) |
25 | 23, 24 | syl 17 |
. . . . . 6
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) → dom
𝑆 ≠
∅) |
26 | | dm0rn0 5263 |
. . . . . . 7
⊢ (dom
𝑆 = ∅ ↔ ran
𝑆 =
∅) |
27 | 26 | necon3bii 2834 |
. . . . . 6
⊢ (dom
𝑆 ≠ ∅ ↔ ran
𝑆 ≠
∅) |
28 | 25, 27 | sylib 207 |
. . . . 5
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) → ran
𝑆 ≠
∅) |
29 | | supxrre2 12033 |
. . . . 5
⊢ ((ran
𝑆 ⊆ ℝ ∧ ran
𝑆 ≠ ∅) →
(sup(ran 𝑆,
ℝ*, < ) ∈ ℝ ↔ sup(ran 𝑆, ℝ*, < ) ≠
+∞)) |
30 | 19, 28, 29 | syl2anc 691 |
. . . 4
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) →
(sup(ran 𝑆,
ℝ*, < ) ∈ ℝ ↔ sup(ran 𝑆, ℝ*, < ) ≠
+∞)) |
31 | 30 | biimpar 501 |
. . 3
⊢ (((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) ≠ +∞) → sup(ran 𝑆, ℝ*, < ) ∈
ℝ) |
32 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
33 | 32 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (1st ‘(𝐹‘𝑚)) = (1st ‘(𝐹‘𝑛))) |
34 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (2↑𝑚) = (2↑𝑛)) |
35 | 34 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((𝑥 / 2) / (2↑𝑚)) = ((𝑥 / 2) / (2↑𝑛))) |
36 | 33, 35 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((1st ‘(𝐹‘𝑚)) − ((𝑥 / 2) / (2↑𝑚))) = ((1st ‘(𝐹‘𝑛)) − ((𝑥 / 2) / (2↑𝑛)))) |
37 | 32 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (2nd ‘(𝐹‘𝑚)) = (2nd ‘(𝐹‘𝑛))) |
38 | 37, 35 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((2nd ‘(𝐹‘𝑚)) + ((𝑥 / 2) / (2↑𝑚))) = ((2nd ‘(𝐹‘𝑛)) + ((𝑥 / 2) / (2↑𝑛)))) |
39 | 36, 38 | opeq12d 4348 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → 〈((1st ‘(𝐹‘𝑚)) − ((𝑥 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝑥 / 2) / (2↑𝑚)))〉 = 〈((1st
‘(𝐹‘𝑛)) − ((𝑥 / 2) / (2↑𝑛))), ((2nd ‘(𝐹‘𝑛)) + ((𝑥 / 2) / (2↑𝑛)))〉) |
40 | 39 | cbvmptv 4678 |
. . . . . 6
⊢ (𝑚 ∈ ℕ ↦
〈((1st ‘(𝐹‘𝑚)) − ((𝑥 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝑥 / 2) / (2↑𝑚)))〉) = (𝑛 ∈ ℕ ↦
〈((1st ‘(𝐹‘𝑛)) − ((𝑥 / 2) / (2↑𝑛))), ((2nd ‘(𝐹‘𝑛)) + ((𝑥 / 2) / (2↑𝑛)))〉) |
41 | | eqid 2610 |
. . . . . 6
⊢ seq1( + ,
((abs ∘ − ) ∘ (𝑚 ∈ ℕ ↦
〈((1st ‘(𝐹‘𝑚)) − ((𝑥 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝑥 / 2) / (2↑𝑚)))〉))) = seq1( + , ((abs ∘
− ) ∘ (𝑚 ∈
ℕ ↦ 〈((1st ‘(𝐹‘𝑚)) − ((𝑥 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝑥 / 2) / (2↑𝑚)))〉))) |
42 | | simplll 794 |
. . . . . 6
⊢ ((((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) |
43 | | simpllr 795 |
. . . . . 6
⊢ ((((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) |
44 | | simpr 476 |
. . . . . 6
⊢ ((((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
45 | | simplr 788 |
. . . . . 6
⊢ ((((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → sup(ran
𝑆, ℝ*,
< ) ∈ ℝ) |
46 | 13, 40, 41, 42, 43, 44, 45 | ovollb2lem 23063 |
. . . . 5
⊢ ((((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) →
(vol*‘𝐴) ≤
(sup(ran 𝑆,
ℝ*, < ) + 𝑥)) |
47 | 46 | ralrimiva 2949 |
. . . 4
⊢ (((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) ∈ ℝ) → ∀𝑥 ∈ ℝ+ (vol*‘𝐴) ≤ (sup(ran 𝑆, ℝ*, < ) +
𝑥)) |
48 | | xralrple 11910 |
. . . . 5
⊢
(((vol*‘𝐴)
∈ ℝ* ∧ sup(ran 𝑆, ℝ*, < ) ∈
ℝ) → ((vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ) ↔
∀𝑥 ∈
ℝ+ (vol*‘𝐴) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝑥))) |
49 | 6, 48 | sylan 487 |
. . . 4
⊢ (((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) ∈ ℝ) → ((vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ) ↔
∀𝑥 ∈
ℝ+ (vol*‘𝐴) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝑥))) |
50 | 47, 49 | mpbird 246 |
. . 3
⊢ (((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) ∈ ℝ) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, <
)) |
51 | 31, 50 | syldan 486 |
. 2
⊢ (((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) ∧
sup(ran 𝑆,
ℝ*, < ) ≠ +∞) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, <
)) |
52 | 11, 51 | pm2.61dane 2869 |
1
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) →
(vol*‘𝐴) ≤ sup(ran
𝑆, ℝ*,
< )) |