Step | Hyp | Ref
| Expression |
1 | | nnuz 11723 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11408 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | ovoliun.v |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈
ℝ) |
4 | | ovoliun.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) |
5 | 3, 4 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:ℕ⟶ℝ) |
6 | 5 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) |
7 | 1, 2, 6 | serfre 12830 |
. . . . . . . . 9
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
8 | | ovoliun.t |
. . . . . . . . . 10
⊢ 𝑇 = seq1( + , 𝐺) |
9 | 8 | feq1i 6036 |
. . . . . . . . 9
⊢ (𝑇:ℕ⟶ℝ ↔
seq1( + , 𝐺):ℕ⟶ℝ) |
10 | 7, 9 | sylibr 224 |
. . . . . . . 8
⊢ (𝜑 → 𝑇:ℕ⟶ℝ) |
11 | | frn 6053 |
. . . . . . . 8
⊢ (𝑇:ℕ⟶ℝ →
ran 𝑇 ⊆
ℝ) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝑇 ⊆ ℝ) |
13 | | ressxr 10083 |
. . . . . . 7
⊢ ℝ
⊆ ℝ* |
14 | 12, 13 | syl6ss 3615 |
. . . . . 6
⊢ (𝜑 → ran 𝑇 ⊆
ℝ*) |
15 | | supxrcl 12145 |
. . . . . 6
⊢ (ran
𝑇 ⊆
ℝ* → sup(ran 𝑇, ℝ*, < ) ∈
ℝ*) |
16 | 14, 15 | syl 17 |
. . . . 5
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ*) |
17 | | xrrebnd 11999 |
. . . . 5
⊢ (sup(ran
𝑇, ℝ*,
< ) ∈ ℝ* → (sup(ran 𝑇, ℝ*, < ) ∈ ℝ
↔ (-∞ < sup(ran 𝑇, ℝ*, < ) ∧ sup(ran
𝑇, ℝ*,
< ) < +∞))) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) ∈ ℝ
↔ (-∞ < sup(ran 𝑇, ℝ*, < ) ∧ sup(ran
𝑇, ℝ*,
< ) < +∞))) |
19 | | mnfxr 10096 |
. . . . . . 7
⊢ -∞
∈ ℝ* |
20 | 19 | a1i 11 |
. . . . . 6
⊢ (𝜑 → -∞ ∈
ℝ*) |
21 | | 1nn 11031 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
22 | | ffvelrn 6357 |
. . . . . . . 8
⊢ ((𝑇:ℕ⟶ℝ ∧ 1
∈ ℕ) → (𝑇‘1) ∈ ℝ) |
23 | 10, 21, 22 | sylancl 694 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘1) ∈ ℝ) |
24 | 23 | rexrd 10089 |
. . . . . 6
⊢ (𝜑 → (𝑇‘1) ∈
ℝ*) |
25 | | mnflt 11957 |
. . . . . . 7
⊢ ((𝑇‘1) ∈ ℝ →
-∞ < (𝑇‘1)) |
26 | 23, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → -∞ < (𝑇‘1)) |
27 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝑇:ℕ⟶ℝ →
𝑇 Fn
ℕ) |
28 | 10, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 Fn ℕ) |
29 | | fnfvelrn 6356 |
. . . . . . . 8
⊢ ((𝑇 Fn ℕ ∧ 1 ∈
ℕ) → (𝑇‘1)
∈ ran 𝑇) |
30 | 28, 21, 29 | sylancl 694 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘1) ∈ ran 𝑇) |
31 | | supxrub 12154 |
. . . . . . 7
⊢ ((ran
𝑇 ⊆
ℝ* ∧ (𝑇‘1) ∈ ran 𝑇) → (𝑇‘1) ≤ sup(ran 𝑇, ℝ*, <
)) |
32 | 14, 30, 31 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝑇‘1) ≤ sup(ran 𝑇, ℝ*, <
)) |
33 | 20, 24, 16, 26, 32 | xrltletrd 11992 |
. . . . 5
⊢ (𝜑 → -∞ < sup(ran
𝑇, ℝ*,
< )) |
34 | 33 | biantrurd 529 |
. . . 4
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) < +∞
↔ (-∞ < sup(ran 𝑇, ℝ*, < ) ∧ sup(ran
𝑇, ℝ*,
< ) < +∞))) |
35 | 18, 34 | bitr4d 271 |
. . 3
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) ∈ ℝ
↔ sup(ran 𝑇,
ℝ*, < ) < +∞)) |
36 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑚𝐴 |
37 | | nfcsb1v 3549 |
. . . . . . . . 9
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
38 | | csbeq1a 3542 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
39 | 36, 37, 38 | cbviun 4557 |
. . . . . . . 8
⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑚 ∈ ℕ
⦋𝑚 / 𝑛⦌𝐴 |
40 | 39 | fveq2i 6194 |
. . . . . . 7
⊢
(vol*‘∪ 𝑛 ∈ ℕ 𝐴) = (vol*‘∪ 𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴) |
41 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑚(vol*‘𝐴) |
42 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛vol* |
43 | 42, 37 | nffv 6198 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(vol*‘⦋𝑚 / 𝑛⦌𝐴) |
44 | 38 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (vol*‘𝐴) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
45 | 41, 43, 44 | cbvmpt 4749 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦
(vol*‘𝐴)) = (𝑚 ∈ ℕ ↦
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
46 | 4, 45 | eqtri 2644 |
. . . . . . . 8
⊢ 𝐺 = (𝑚 ∈ ℕ ↦
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
47 | | ovoliun.a |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) |
48 | 47 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ 𝐴 ⊆ ℝ) |
49 | | nfv 1843 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚 𝐴 ⊆
ℝ |
50 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛ℝ |
51 | 37, 50 | nfss 3596 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ |
52 | 38 | sseq1d 3632 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → (𝐴 ⊆ ℝ ↔ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ)) |
53 | 49, 51, 52 | cbvral 3167 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ 𝐴 ⊆ ℝ
↔ ∀𝑚 ∈
ℕ ⦋𝑚 /
𝑛⦌𝐴 ⊆
ℝ) |
54 | 48, 53 | sylib 208 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
55 | 54 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) → ∀𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
56 | 55 | r19.21bi 2932 |
. . . . . . . 8
⊢ ((((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ 𝑚 ∈ ℕ) → ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
57 | 3 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ (vol*‘𝐴) ∈ ℝ) |
58 | 41 | nfel1 2779 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚(vol*‘𝐴) ∈ ℝ |
59 | 43 | nfel1 2779 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ |
60 | 44 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((vol*‘𝐴) ∈ ℝ ↔
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ)) |
61 | 58, 59, 60 | cbvral 3167 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ (vol*‘𝐴)
∈ ℝ ↔ ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
62 | 57, 61 | sylib 208 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
63 | 62 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) → ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
64 | 63 | r19.21bi 2932 |
. . . . . . . 8
⊢ ((((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) ∧ 𝑚 ∈ ℕ) →
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
65 | | simplr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
66 | | simpr 477 |
. . . . . . . 8
⊢ (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) → 𝑥 ∈ ℝ+) |
67 | 8, 46, 56, 64, 65, 66 | ovoliunlem3 23272 |
. . . . . . 7
⊢ (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) → (vol*‘∪
𝑚 ∈ ℕ
⦋𝑚 / 𝑛⦌𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝑥)) |
68 | 40, 67 | syl5eqbr 4688 |
. . . . . 6
⊢ (((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) ∧ 𝑥 ∈
ℝ+) → (vol*‘∪
𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) +
𝑥)) |
69 | 68 | ralrimiva 2966 |
. . . . 5
⊢ ((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) → ∀𝑥
∈ ℝ+ (vol*‘∪
𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) +
𝑥)) |
70 | | iunss 4561 |
. . . . . . . 8
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ ↔ ∀𝑛 ∈ ℕ 𝐴 ⊆
ℝ) |
71 | 48, 70 | sylibr 224 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ) |
72 | | ovolcl 23246 |
. . . . . . 7
⊢ (∪ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
73 | 71, 72 | syl 17 |
. . . . . 6
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ∈
ℝ*) |
74 | | xralrple 12036 |
. . . . . 6
⊢
(((vol*‘∪ 𝑛 ∈ ℕ 𝐴) ∈ ℝ* ∧ sup(ran
𝑇, ℝ*,
< ) ∈ ℝ) → ((vol*‘∪
𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ) ↔
∀𝑥 ∈
ℝ+ (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) +
𝑥))) |
75 | 73, 74 | sylan 488 |
. . . . 5
⊢ ((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) → ((vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ) ↔
∀𝑥 ∈
ℝ+ (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) +
𝑥))) |
76 | 69, 75 | mpbird 247 |
. . . 4
⊢ ((𝜑 ∧ sup(ran 𝑇, ℝ*, < ) ∈
ℝ) → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
)) |
77 | 76 | ex 450 |
. . 3
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) ∈ ℝ
→ (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
))) |
78 | 35, 77 | sylbird 250 |
. 2
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) < +∞
→ (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
))) |
79 | | nltpnft 11995 |
. . . 4
⊢ (sup(ran
𝑇, ℝ*,
< ) ∈ ℝ* → (sup(ran 𝑇, ℝ*, < ) = +∞
↔ ¬ sup(ran 𝑇,
ℝ*, < ) < +∞)) |
80 | 16, 79 | syl 17 |
. . 3
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) = +∞
↔ ¬ sup(ran 𝑇,
ℝ*, < ) < +∞)) |
81 | | pnfge 11964 |
. . . . 5
⊢
((vol*‘∪ 𝑛 ∈ ℕ 𝐴) ∈ ℝ* →
(vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ +∞) |
82 | 73, 81 | syl 17 |
. . . 4
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ +∞) |
83 | | breq2 4657 |
. . . 4
⊢ (sup(ran
𝑇, ℝ*,
< ) = +∞ → ((vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ) ↔
(vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ +∞)) |
84 | 82, 83 | syl5ibrcom 237 |
. . 3
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) = +∞
→ (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
))) |
85 | 80, 84 | sylbird 250 |
. 2
⊢ (𝜑 → (¬ sup(ran 𝑇, ℝ*, < )
< +∞ → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
))) |
86 | 78, 85 | pm2.61d 170 |
1
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
)) |