Proof of Theorem ovolmge0
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elovolm.1 | . . 3
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, <
))} | 
| 2 | 1 | elovolm 25510 | . 2
⊢ (𝐵 ∈ 𝑀 ↔ ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, <
))) | 
| 3 |  | elovolmlem 25509 | . . . . . 6
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ↔ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) | 
| 4 |  | eqid 2737 | . . . . . . . . . 10
⊢ ((abs
∘ − ) ∘ 𝑓) = ((abs ∘ − ) ∘ 𝑓) | 
| 5 |  | eqid 2737 | . . . . . . . . . 10
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) | 
| 6 | 4, 5 | ovolsf 25507 | . . . . . . . . 9
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘
𝑓)):ℕ⟶(0[,)+∞)) | 
| 7 |  | 1nn 12277 | . . . . . . . . 9
⊢ 1 ∈
ℕ | 
| 8 |  | ffvelcdm 7101 | . . . . . . . . 9
⊢ ((seq1( +
, ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞) ∧ 1
∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝑓))‘1) ∈
(0[,)+∞)) | 
| 9 | 6, 7, 8 | sylancl 586 | . . . . . . . 8
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (seq1( + , ((abs ∘ − ) ∘
𝑓))‘1) ∈
(0[,)+∞)) | 
| 10 |  | elrege0 13494 | . . . . . . . . 9
⊢ ((seq1( +
, ((abs ∘ − ) ∘ 𝑓))‘1) ∈ (0[,)+∞) ↔
((seq1( + , ((abs ∘ − ) ∘ 𝑓))‘1) ∈ ℝ ∧ 0 ≤
(seq1( + , ((abs ∘ − ) ∘ 𝑓))‘1))) | 
| 11 | 10 | simprbi 496 | . . . . . . . 8
⊢ ((seq1( +
, ((abs ∘ − ) ∘ 𝑓))‘1) ∈ (0[,)+∞) → 0
≤ (seq1( + , ((abs ∘ − ) ∘ 𝑓))‘1)) | 
| 12 | 9, 11 | syl 17 | . . . . . . 7
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 0 ≤ (seq1( + , ((abs ∘ − )
∘ 𝑓))‘1)) | 
| 13 | 6 | frnd 6744 | . . . . . . . . 9
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ran seq1( + , ((abs ∘ − ) ∘
𝑓)) ⊆
(0[,)+∞)) | 
| 14 |  | icossxr 13472 | . . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ* | 
| 15 | 13, 14 | sstrdi 3996 | . . . . . . . 8
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ran seq1( + , ((abs ∘ − ) ∘
𝑓)) ⊆
ℝ*) | 
| 16 | 6 | ffnd 6737 | . . . . . . . . 9
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘
𝑓)) Fn
ℕ) | 
| 17 |  | fnfvelrn 7100 | . . . . . . . . 9
⊢ ((seq1( +
, ((abs ∘ − ) ∘ 𝑓)) Fn ℕ ∧ 1 ∈ ℕ) →
(seq1( + , ((abs ∘ − ) ∘ 𝑓))‘1) ∈ ran seq1( + , ((abs
∘ − ) ∘ 𝑓))) | 
| 18 | 16, 7, 17 | sylancl 586 | . . . . . . . 8
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (seq1( + , ((abs ∘ − ) ∘
𝑓))‘1) ∈ ran
seq1( + , ((abs ∘ − ) ∘ 𝑓))) | 
| 19 |  | supxrub 13366 | . . . . . . . 8
⊢ ((ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ ℝ* ∧ (seq1( +
, ((abs ∘ − ) ∘ 𝑓))‘1) ∈ ran seq1( + , ((abs
∘ − ) ∘ 𝑓))) → (seq1( + , ((abs ∘ − )
∘ 𝑓))‘1) ≤
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
)) | 
| 20 | 15, 18, 19 | syl2anc 584 | . . . . . . 7
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (seq1( + , ((abs ∘ − ) ∘
𝑓))‘1) ≤ sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
)) | 
| 21 |  | 0xr 11308 | . . . . . . . 8
⊢ 0 ∈
ℝ* | 
| 22 | 14, 9 | sselid 3981 | . . . . . . . 8
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (seq1( + , ((abs ∘ − ) ∘
𝑓))‘1) ∈
ℝ*) | 
| 23 |  | supxrcl 13357 | . . . . . . . . 9
⊢ (ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ ℝ* → sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈
ℝ*) | 
| 24 | 15, 23 | syl 17 | . . . . . . . 8
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ) ∈ ℝ*) | 
| 25 |  | xrletr 13200 | . . . . . . . 8
⊢ ((0
∈ ℝ* ∧ (seq1( + , ((abs ∘ − ) ∘
𝑓))‘1) ∈
ℝ* ∧ sup(ran seq1( + , ((abs ∘ − ) ∘
𝑓)), ℝ*,
< ) ∈ ℝ*) → ((0 ≤ (seq1( + , ((abs ∘
− ) ∘ 𝑓))‘1) ∧ (seq1( + , ((abs ∘
− ) ∘ 𝑓))‘1) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) → 0
≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
))) | 
| 26 | 21, 22, 24, 25 | mp3an2i 1468 | . . . . . . 7
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((0 ≤ (seq1( + , ((abs ∘ − )
∘ 𝑓))‘1) ∧
(seq1( + , ((abs ∘ − ) ∘ 𝑓))‘1) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) → 0
≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
))) | 
| 27 | 12, 20, 26 | mp2and 699 | . . . . . 6
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 0 ≤ sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < )) | 
| 28 | 3, 27 | sylbi 217 | . . . . 5
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → 0 ≤ sup(ran seq1( + ,
((abs ∘ − ) ∘ 𝑓)), ℝ*, <
)) | 
| 29 |  | breq2 5147 | . . . . 5
⊢ (𝐵 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < ) → (0
≤ 𝐵 ↔ 0 ≤
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
))) | 
| 30 | 28, 29 | syl5ibrcom 247 | . . . 4
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → (𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ) → 0 ≤ 𝐵)) | 
| 31 | 30 | adantld 490 | . . 3
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) → 0
≤ 𝐵)) | 
| 32 | 31 | rexlimiv 3148 | . 2
⊢
(∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → 0 ≤ 𝐵) | 
| 33 | 2, 32 | sylbi 217 | 1
⊢ (𝐵 ∈ 𝑀 → 0 ≤ 𝐵) |