| 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 25540 |
. 2
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, <
)) |
| 6 | | nnuz 12921 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
| 7 | | 1zzd 12648 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℤ) |
| 8 | | fvex 6919 |
. . . . . . . . . . 11
⊢
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ V |
| 9 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑚(vol*‘𝐴) |
| 10 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛vol* |
| 11 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 |
| 12 | 10, 11 | nffv 6916 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(vol*‘⦋𝑚 / 𝑛⦌𝐴) |
| 13 | | csbeq1a 3913 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → 𝐴 = ⦋𝑚 / 𝑛⦌𝐴) |
| 14 | 13 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (vol*‘𝐴) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 15 | 9, 12, 14 | cbvmpt 5253 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦
(vol*‘𝐴)) = (𝑚 ∈ ℕ ↦
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 16 | 2, 15 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑚 ∈ ℕ ↦
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 17 | 16 | fvmpt2 7027 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ V) → (𝐺‘𝑚) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 18 | 8, 17 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → (𝐺‘𝑚) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 19 | 18 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 20 | 4 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ (vol*‘𝐴) ∈ ℝ) |
| 21 | 9 | nfel1 2922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚(vol*‘𝐴) ∈ ℝ |
| 22 | 12 | nfel1 2922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ |
| 23 | 14 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((vol*‘𝐴) ∈ ℝ ↔
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ)) |
| 24 | 21, 22, 23 | cbvralw 3306 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ℕ (vol*‘𝐴)
∈ ℝ ↔ ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
| 25 | 20, 24 | sylib 218 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
| 26 | 25 | r19.21bi 3251 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
| 27 | 19, 26 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) ∈ ℝ) |
| 28 | 6, 7, 27 | serfre 14072 |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
| 29 | 1 | feq1i 6727 |
. . . . . . 7
⊢ (𝑇:ℕ⟶ℝ ↔
seq1( + , 𝐺):ℕ⟶ℝ) |
| 30 | 28, 29 | sylibr 234 |
. . . . . 6
⊢ (𝜑 → 𝑇:ℕ⟶ℝ) |
| 31 | 30 | frnd 6744 |
. . . . 5
⊢ (𝜑 → ran 𝑇 ⊆ ℝ) |
| 32 | | 1nn 12277 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
| 33 | 30 | fdmd 6746 |
. . . . . . . 8
⊢ (𝜑 → dom 𝑇 = ℕ) |
| 34 | 32, 33 | eleqtrrid 2848 |
. . . . . . 7
⊢ (𝜑 → 1 ∈ dom 𝑇) |
| 35 | 34 | ne0d 4342 |
. . . . . 6
⊢ (𝜑 → dom 𝑇 ≠ ∅) |
| 36 | | dm0rn0 5935 |
. . . . . . 7
⊢ (dom
𝑇 = ∅ ↔ ran
𝑇 =
∅) |
| 37 | 36 | necon3bii 2993 |
. . . . . 6
⊢ (dom
𝑇 ≠ ∅ ↔ ran
𝑇 ≠
∅) |
| 38 | 35, 37 | sylib 218 |
. . . . 5
⊢ (𝜑 → ran 𝑇 ≠ ∅) |
| 39 | | ovoliun2.t |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ dom ⇝ ) |
| 40 | 1, 39 | eqeltrrid 2846 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐺) ∈ dom ⇝
) |
| 41 | 6, 7, 19, 26, 40 | isumrecl 15801 |
. . . . . . 7
⊢ (𝜑 → Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
| 42 | | elfznn 13593 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (1...𝑘) → 𝑚 ∈ ℕ) |
| 43 | 42 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → 𝑚 ∈ ℕ) |
| 44 | 43, 18 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (𝐺‘𝑚) = (vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 45 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
| 46 | 45, 6 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
| 47 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝜑) |
| 48 | 47, 42, 26 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ) |
| 49 | 48 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℂ) |
| 50 | 44, 46, 49 | fsumser 15766 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(vol*‘⦋𝑚 / 𝑛⦌𝐴) = (seq1( + , 𝐺)‘𝑘)) |
| 51 | 1 | fveq1i 6907 |
. . . . . . . . . 10
⊢ (𝑇‘𝑘) = (seq1( + , 𝐺)‘𝑘) |
| 52 | 50, 51 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(vol*‘⦋𝑚 / 𝑛⦌𝐴) = (𝑇‘𝑘)) |
| 53 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...𝑘) ∈ Fin) |
| 54 | | fz1ssnn 13595 |
. . . . . . . . . . . 12
⊢
(1...𝑘) ⊆
ℕ |
| 55 | 54 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...𝑘) ⊆ ℕ) |
| 56 | 3 | ralrimiva 3146 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑛 ∈ ℕ 𝐴 ⊆ ℝ) |
| 57 | | nfv 1914 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚 𝐴 ⊆
ℝ |
| 58 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛ℝ |
| 59 | 11, 58 | nfss 3976 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ |
| 60 | 13 | sseq1d 4015 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝐴 ⊆ ℝ ↔ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ)) |
| 61 | 57, 59, 60 | cbvralw 3306 |
. . . . . . . . . . . . . 14
⊢
(∀𝑛 ∈
ℕ 𝐴 ⊆ ℝ
↔ ∀𝑚 ∈
ℕ ⦋𝑚 /
𝑛⦌𝐴 ⊆
ℝ) |
| 62 | 56, 61 | sylib 218 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑚 ∈ ℕ ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
| 63 | 62 | r19.21bi 3251 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ⦋𝑚 / 𝑛⦌𝐴 ⊆ ℝ) |
| 64 | | ovolge0 25516 |
. . . . . . . . . . . 12
⊢
(⦋𝑚 /
𝑛⦌𝐴 ⊆ ℝ → 0 ≤
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 65 | 63, 64 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0 ≤
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 66 | 6, 7, 53, 55, 19, 26, 65, 40 | isumless 15881 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑚 ∈ (1...𝑘)(vol*‘⦋𝑚 / 𝑛⦌𝐴) ≤ Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 67 | 66 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(vol*‘⦋𝑚 / 𝑛⦌𝐴) ≤ Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 68 | 52, 67 | eqbrtrrd 5167 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ≤ Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 69 | 68 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 70 | | brralrspcev 5203 |
. . . . . . 7
⊢
((Σ𝑚 ∈
ℕ (vol*‘⦋𝑚 / 𝑛⦌𝐴) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ 𝑥) |
| 71 | 41, 69, 70 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ 𝑥) |
| 72 | 30 | ffnd 6737 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 Fn ℕ) |
| 73 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑧 = (𝑇‘𝑘) → (𝑧 ≤ 𝑥 ↔ (𝑇‘𝑘) ≤ 𝑥)) |
| 74 | 73 | ralrn 7108 |
. . . . . . . 8
⊢ (𝑇 Fn ℕ →
(∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ 𝑥)) |
| 75 | 72, 74 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ 𝑥)) |
| 76 | 75 | rexbidv 3179 |
. . . . . 6
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ 𝑥)) |
| 77 | 71, 76 | mpbird 257 |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥) |
| 78 | | supxrre 13369 |
. . . . 5
⊢ ((ran
𝑇 ⊆ ℝ ∧ ran
𝑇 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥) → sup(ran 𝑇, ℝ*, < ) = sup(ran
𝑇, ℝ, <
)) |
| 79 | 31, 38, 77, 78 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) = sup(ran
𝑇, ℝ, <
)) |
| 80 | 6, 1, 7, 19, 26, 65, 71 | isumsup 15883 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) = sup(ran 𝑇, ℝ, < )) |
| 81 | 79, 80 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) = Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴)) |
| 82 | 14, 9, 12 | cbvsum 15731 |
. . 3
⊢
Σ𝑛 ∈
ℕ (vol*‘𝐴) =
Σ𝑚 ∈ ℕ
(vol*‘⦋𝑚 / 𝑛⦌𝐴) |
| 83 | 81, 82 | eqtr4di 2795 |
. 2
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) = Σ𝑛 ∈ ℕ
(vol*‘𝐴)) |
| 84 | 5, 83 | breqtrd 5169 |
1
⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ Σ𝑛 ∈ ℕ (vol*‘𝐴)) |