Step | Hyp | Ref
| Expression |
1 | | ovoliun.t |
. . 3
⊢ 𝑇 = seq1( + , 𝐺) |
2 | | ovoliun.g |
. . 3
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) |
3 | | ovoliun.a |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) |
4 | | ovoliun.v |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈
ℝ) |
5 | 1, 2, 3, 4 | ovoliun 23080 |
. 2
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
)) |
6 | | nnuz 11599 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
7 | | 1zzd 11285 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℤ) |
8 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ V |
9 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚(vol*‘𝐴) |
10 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛vol* |
11 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
12 | 10, 11 | nffv 6110 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(vol*‘⦋𝑚 / 𝑛⦌𝐴) |
13 | | csbeq1a 3508 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
14 | 13 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (vol*‘𝐴) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
15 | 9, 12, 14 | cbvmpt 4677 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦
(vol*‘𝐴)) = (𝑚 ∈ ℕ ↦
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
16 | 2, 15 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑚 ∈ ℕ ↦
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
17 | 16 | fvmpt2 6200 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ V) → (𝐺‘𝑚) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
18 | 8, 17 | mpan2 703 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → (𝐺‘𝑚) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
19 | 18 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
20 | 4 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ (vol*‘𝐴) ∈ ℝ) |
21 | 9 | nfel1 2765 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚(vol*‘𝐴) ∈ ℝ |
22 | 12 | nfel1 2765 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ |
23 | 14 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((vol*‘𝐴) ∈ ℝ ↔
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ)) |
24 | 21, 22, 23 | cbvral 3143 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ (vol*‘𝐴)
∈ ℝ ↔ ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
25 | 20, 24 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
26 | 25 | r19.21bi 2916 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
27 | 19, 26 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) ∈ ℝ) |
28 | 6, 7, 27 | serfre 12692 |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
29 | 1 | feq1i 5949 |
. . . . . . 7
⊢ (𝑇:ℕ⟶ℝ ↔
seq1( + , 𝐺):ℕ⟶ℝ) |
30 | 28, 29 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → 𝑇:ℕ⟶ℝ) |
31 | | frn 5966 |
. . . . . 6
⊢ (𝑇:ℕ⟶ℝ →
ran 𝑇 ⊆
ℝ) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝑇 ⊆ ℝ) |
33 | | 1nn 10908 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
34 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝑇:ℕ⟶ℝ →
dom 𝑇 =
ℕ) |
35 | 30, 34 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → dom 𝑇 = ℕ) |
36 | 33, 35 | syl5eleqr 2695 |
. . . . . . 7
⊢ (𝜑 → 1 ∈ dom 𝑇) |
37 | | ne0i 3880 |
. . . . . . 7
⊢ (1 ∈
dom 𝑇 → dom 𝑇 ≠ ∅) |
38 | 36, 37 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝑇 ≠ ∅) |
39 | | dm0rn0 5263 |
. . . . . . 7
⊢ (dom
𝑇 = ∅ ↔ ran
𝑇 =
∅) |
40 | 39 | necon3bii 2834 |
. . . . . 6
⊢ (dom
𝑇 ≠ ∅ ↔ ran
𝑇 ≠
∅) |
41 | 38, 40 | sylib 207 |
. . . . 5
⊢ (𝜑 → ran 𝑇 ≠ ∅) |
42 | | ovoliun2.t |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ dom ⇝ ) |
43 | 1, 42 | syl5eqelr 2693 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐺) ∈ dom ⇝
) |
44 | 6, 7, 19, 26, 43 | isumrecl 14338 |
. . . . . . 7
⊢ (𝜑 → Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
45 | | elfznn 12241 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (1...𝑘) → 𝑚 ∈ ℕ) |
46 | 45 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → 𝑚 ∈ ℕ) |
47 | 46, 18 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (𝐺‘𝑚) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
48 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
49 | 48, 6 | syl6eleq 2698 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
50 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝜑) |
51 | 50, 45, 26 | syl2an 493 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
52 | 51 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℂ) |
53 | 47, 49, 52 | fsumser 14308 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(vol*‘⦋𝑚 / 𝑛⦌𝐴) = (seq1( + , 𝐺)‘𝑘)) |
54 | 1 | fveq1i 6104 |
. . . . . . . . . 10
⊢ (𝑇‘𝑘) = (seq1( + , 𝐺)‘𝑘) |
55 | 53, 54 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(vol*‘⦋𝑚 / 𝑛⦌𝐴) = (𝑇‘𝑘)) |
56 | | fzfid 12634 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...𝑘) ∈ Fin) |
57 | | elfznn 12241 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ) |
58 | 57 | ssriv 3572 |
. . . . . . . . . . . 12
⊢
(1...𝑘) ⊆
ℕ |
59 | 58 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...𝑘) ⊆ ℕ) |
60 | 3 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑛 ∈ ℕ 𝐴 ⊆ ℝ) |
61 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚 𝐴 ⊆
ℝ |
62 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛ℝ |
63 | 11, 62 | nfss 3561 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ |
64 | 13 | sseq1d 3595 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝐴 ⊆ ℝ ↔ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ)) |
65 | 61, 63, 64 | cbvral 3143 |
. . . . . . . . . . . . . 14
⊢
(∀𝑛 ∈
ℕ 𝐴 ⊆ ℝ
↔ ∀𝑚 ∈
ℕ ⦋𝑚 /
𝑛⦌𝐴 ⊆
ℝ) |
66 | 60, 65 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
67 | 66 | r19.21bi 2916 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
68 | | ovolge0 23056 |
. . . . . . . . . . . 12
⊢
(⦋𝑚 /
𝑛⦌𝐴 ⊆ ℝ → 0 ≤
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0 ≤
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
70 | 6, 7, 56, 59, 19, 26, 69, 43 | isumless 14416 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑚 ∈ (1...𝑘)(vol*‘⦋𝑚 / 𝑛⦌𝐴) ≤ Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
71 | 70 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(vol*‘⦋𝑚 / 𝑛⦌𝐴) ≤ Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
72 | 55, 71 | eqbrtrrd 4607 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ≤ Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
73 | 72 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
74 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑥 = Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) → ((𝑇‘𝑘) ≤ 𝑥 ↔ (𝑇‘𝑘) ≤ Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴))) |
75 | 74 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑥 = Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) → (∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴))) |
76 | 75 | rspcev 3282 |
. . . . . . 7
⊢
((Σ𝑚 ∈
ℕ (vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ 𝑥) |
77 | 44, 73, 76 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ 𝑥) |
78 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑇:ℕ⟶ℝ →
𝑇 Fn
ℕ) |
79 | 30, 78 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 Fn ℕ) |
80 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑧 = (𝑇‘𝑘) → (𝑧 ≤ 𝑥 ↔ (𝑇‘𝑘) ≤ 𝑥)) |
81 | 80 | ralrn 6270 |
. . . . . . . 8
⊢ (𝑇 Fn ℕ →
(∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ 𝑥)) |
82 | 79, 81 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ 𝑥)) |
83 | 82 | rexbidv 3034 |
. . . . . 6
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ 𝑥)) |
84 | 77, 83 | mpbird 246 |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥) |
85 | | supxrre 12029 |
. . . . 5
⊢ ((ran
𝑇 ⊆ ℝ ∧ ran
𝑇 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥) → sup(ran 𝑇, ℝ*, < ) = sup(ran
𝑇, ℝ, <
)) |
86 | 32, 41, 84, 85 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) = sup(ran
𝑇, ℝ, <
)) |
87 | 6, 1, 7, 19, 26, 69, 77 | isumsup 14418 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) = sup(ran 𝑇, ℝ, < )) |
88 | 86, 87 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) = Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
89 | 9, 12, 14 | cbvsumi 14275 |
. . 3
⊢
Σ𝑛 ∈
ℕ (vol*‘𝐴) =
Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) |
90 | 88, 89 | syl6eqr 2662 |
. 2
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) = Σ𝑛 ∈ ℕ
(vol*‘𝐴)) |
91 | 5, 90 | breqtrd 4609 |
1
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ Σ𝑛 ∈ ℕ (vol*‘𝐴)) |