Step | Hyp | Ref
| Expression |
1 | | mnfxr 10895 |
. . . . . 6
⊢ -∞
∈ ℝ* |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝜑 → -∞ ∈
ℝ*) |
3 | | nnuz 12482 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
4 | | 1zzd 12213 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
5 | | ovoliun.v |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈
ℝ) |
6 | | ovoliun.g |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) |
7 | 5, 6 | fmptd 6936 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ℕ⟶ℝ) |
8 | 7 | ffvelrnda 6909 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) |
9 | 3, 4, 8 | serfre 13610 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
10 | | ovoliun.t |
. . . . . . . . 9
⊢ 𝑇 = seq1( + , 𝐺) |
11 | 10 | feq1i 6541 |
. . . . . . . 8
⊢ (𝑇:ℕ⟶ℝ ↔
seq1( + , 𝐺):ℕ⟶ℝ) |
12 | 9, 11 | sylibr 237 |
. . . . . . 7
⊢ (𝜑 → 𝑇:ℕ⟶ℝ) |
13 | | 1nn 11846 |
. . . . . . 7
⊢ 1 ∈
ℕ |
14 | | ffvelrn 6907 |
. . . . . . 7
⊢ ((𝑇:ℕ⟶ℝ ∧ 1
∈ ℕ) → (𝑇‘1) ∈ ℝ) |
15 | 12, 13, 14 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → (𝑇‘1) ∈ ℝ) |
16 | 15 | rexrd 10888 |
. . . . 5
⊢ (𝜑 → (𝑇‘1) ∈
ℝ*) |
17 | 12 | frnd 6558 |
. . . . . . 7
⊢ (𝜑 → ran 𝑇 ⊆ ℝ) |
18 | | ressxr 10882 |
. . . . . . 7
⊢ ℝ
⊆ ℝ* |
19 | 17, 18 | sstrdi 3918 |
. . . . . 6
⊢ (𝜑 → ran 𝑇 ⊆
ℝ*) |
20 | | supxrcl 12910 |
. . . . . 6
⊢ (ran
𝑇 ⊆
ℝ* → sup(ran 𝑇, ℝ*, < ) ∈
ℝ*) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ*) |
22 | 15 | mnfltd 12721 |
. . . . 5
⊢ (𝜑 → -∞ < (𝑇‘1)) |
23 | 12 | ffnd 6551 |
. . . . . . 7
⊢ (𝜑 → 𝑇 Fn ℕ) |
24 | | fnfvelrn 6906 |
. . . . . . 7
⊢ ((𝑇 Fn ℕ ∧ 1 ∈
ℕ) → (𝑇‘1)
∈ ran 𝑇) |
25 | 23, 13, 24 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → (𝑇‘1) ∈ ran 𝑇) |
26 | | supxrub 12919 |
. . . . . 6
⊢ ((ran
𝑇 ⊆
ℝ* ∧ (𝑇‘1) ∈ ran 𝑇) → (𝑇‘1) ≤ sup(ran 𝑇, ℝ*, <
)) |
27 | 19, 25, 26 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑇‘1) ≤ sup(ran 𝑇, ℝ*, <
)) |
28 | 2, 16, 21, 22, 27 | xrltletrd 12756 |
. . . 4
⊢ (𝜑 → -∞ < sup(ran
𝑇, ℝ*,
< )) |
29 | | xrrebnd 12763 |
. . . . 5
⊢ (sup(ran
𝑇, ℝ*,
< ) ∈ ℝ* → (sup(ran 𝑇, ℝ*, < ) ∈ ℝ
↔ (-∞ < sup(ran 𝑇, ℝ*, < ) ∧ sup(ran
𝑇, ℝ*,
< ) < +∞))) |
30 | 21, 29 | syl 17 |
. . . 4
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) ∈ ℝ
↔ (-∞ < sup(ran 𝑇, ℝ*, < ) ∧ sup(ran
𝑇, ℝ*,
< ) < +∞))) |
31 | 28, 30 | mpbirand 707 |
. . 3
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) ∈ ℝ
↔ sup(ran 𝑇,
ℝ*, < ) < +∞)) |
32 | | nfcv 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑚𝐴 |
33 | | nfcsb1v 3841 |
. . . . . . . . 9
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
34 | | csbeq1a 3830 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
35 | 32, 33, 34 | cbviun 4950 |
. . . . . . . 8
⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑚 ∈ ℕ
⦋𝑚 / 𝑛⦌𝐴 |
36 | 35 | fveq2i 6725 |
. . . . . . 7
⊢
(vol*‘∪ 𝑛 ∈ ℕ 𝐴) = (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) |
37 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑚(vol*‘𝐴) |
38 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛vol* |
39 | 38, 33 | nffv 6732 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(vol*‘⦋𝑚 / 𝑛⦌𝐴) |
40 | 34 | fveq2d 6726 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (vol*‘𝐴) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
41 | 37, 39, 40 | cbvmpt 5161 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦
(vol*‘𝐴)) = (𝑚 ∈ ℕ ↦
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
42 | 6, 41 | eqtri 2765 |
. . . . . . . 8
⊢ 𝐺 = (𝑚 ∈ ℕ ↦
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
43 | | ovoliun.a |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) |
44 | 43 | ralrimiva 3105 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ 𝐴 ⊆ ℝ) |
45 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚 𝐴 ⊆
ℝ |
46 | | nfcv 2904 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛ℝ |
47 | 33, 46 | nfss 3897 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ |
48 | 34 | sseq1d 3937 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → (𝐴 ⊆ ℝ ↔ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ)) |
49 | 45, 47, 48 | cbvralw 3354 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ 𝐴 ⊆ ℝ
↔ ∀𝑚 ∈
ℕ ⦋𝑚 /
𝑛⦌𝐴 ⊆
ℝ) |
50 | 44, 49 | sylib 221 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
51 | 50 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) → ∀𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
52 | 51 | r19.21bi 3130 |
. . . . . . . 8
⊢ ((((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ 𝑚 ∈ ℕ) → ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
53 | 5 | ralrimiva 3105 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ (vol*‘𝐴) ∈ ℝ) |
54 | 37 | nfel1 2920 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚(vol*‘𝐴) ∈ ℝ |
55 | 39 | nfel1 2920 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ |
56 | 40 | eleq1d 2822 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((vol*‘𝐴) ∈ ℝ ↔
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ)) |
57 | 54, 55, 56 | cbvralw 3354 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ (vol*‘𝐴)
∈ ℝ ↔ ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
58 | 53, 57 | sylib 221 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
59 | 58 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) → ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
60 | 59 | r19.21bi 3130 |
. . . . . . . 8
⊢ ((((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ 𝑚 ∈ ℕ) →
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
61 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
62 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℝ+) |
63 | 10, 42, 52, 60, 61, 62 | ovoliunlem3 24406 |
. . . . . . 7
⊢ (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) → (vol*‘∪
𝑚 ∈ ℕ
⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝑥)) |
64 | 36, 63 | eqbrtrid 5093 |
. . . . . 6
⊢ (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) → (vol*‘∪
𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) +
𝑥)) |
65 | 64 | ralrimiva 3105 |
. . . . 5
⊢ ((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) → ∀𝑥
∈ ℝ+ (vol*‘∪
𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) +
𝑥)) |
66 | | iunss 4959 |
. . . . . . . 8
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ ↔ ∀𝑛 ∈ ℕ 𝐴 ⊆
ℝ) |
67 | 44, 66 | sylibr 237 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ) |
68 | | ovolcl 24380 |
. . . . . . 7
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
69 | 67, 68 | syl 17 |
. . . . . 6
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
70 | | xralrple 12800 |
. . . . . 6
⊢
(((vol*‘∪ 𝑛 ∈ ℕ 𝐴) ∈ ℝ* ∧ sup(ran
𝑇, ℝ*,
< ) ∈ ℝ) → ((vol*‘∪
𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ) ↔
∀𝑥 ∈
ℝ+ (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) +
𝑥))) |
71 | 69, 70 | sylan 583 |
. . . . 5
⊢ ((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) → ((vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ) ↔
∀𝑥 ∈
ℝ+ (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) +
𝑥))) |
72 | 65, 71 | mpbird 260 |
. . . 4
⊢ ((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
)) |
73 | 72 | ex 416 |
. . 3
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) ∈ ℝ
→ (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
))) |
74 | 31, 73 | sylbird 263 |
. 2
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) < +∞
→ (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
))) |
75 | | nltpnft 12759 |
. . . 4
⊢ (sup(ran
𝑇, ℝ*,
< ) ∈ ℝ* → (sup(ran 𝑇, ℝ*, < ) = +∞
↔ ¬ sup(ran 𝑇,
ℝ*, < ) < +∞)) |
76 | 21, 75 | syl 17 |
. . 3
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) = +∞
↔ ¬ sup(ran 𝑇,
ℝ*, < ) < +∞)) |
77 | | pnfge 12727 |
. . . . 5
⊢
((vol*‘∪ 𝑛 ∈ ℕ 𝐴) ∈ ℝ* →
(vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ +∞) |
78 | 69, 77 | syl 17 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ +∞) |
79 | | breq2 5062 |
. . . 4
⊢ (sup(ran
𝑇, ℝ*,
< ) = +∞ → ((vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ) ↔
(vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ +∞)) |
80 | 78, 79 | syl5ibrcom 250 |
. . 3
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) = +∞
→ (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
))) |
81 | 76, 80 | sylbird 263 |
. 2
⊢ (𝜑 → (¬ sup(ran 𝑇, ℝ*, < )
< +∞ → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
))) |
82 | 74, 81 | pm2.61d 182 |
1
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
)) |