Proof of Theorem ovolmge0
Step | Hyp | Ref
| Expression |
1 | | ovolval.1 |
. . 3
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} |
2 | 1 | elovolm 23050 |
. 2
⊢ (𝐵 ∈ 𝑀 ↔ ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, <
))) |
3 | | reex 9906 |
. . . . . . . . 9
⊢ ℝ
∈ V |
4 | 3, 3 | xpex 6860 |
. . . . . . . 8
⊢ (ℝ
× ℝ) ∈ V |
5 | 4 | inex2 4728 |
. . . . . . 7
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V |
6 | | nnex 10903 |
. . . . . . 7
⊢ ℕ
∈ V |
7 | 5, 6 | elmap 7772 |
. . . . . 6
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ↔ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
8 | | eqid 2610 |
. . . . . . . . . 10
⊢ ((abs
∘ − ) ∘ 𝑓) = ((abs ∘ − ) ∘ 𝑓) |
9 | | eqid 2610 |
. . . . . . . . . 10
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) |
10 | 8, 9 | ovolsf 23048 |
. . . . . . . . 9
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘
𝑓)):ℕ⟶(0[,)+∞)) |
11 | | 1nn 10908 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
12 | | ffvelrn 6265 |
. . . . . . . . 9
⊢ ((seq1( +
, ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞) ∧ 1
∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝑓))‘1) ∈
(0[,)+∞)) |
13 | 10, 11, 12 | sylancl 693 |
. . . . . . . 8
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (seq1( + , ((abs ∘ − ) ∘
𝑓))‘1) ∈
(0[,)+∞)) |
14 | | elrege0 12149 |
. . . . . . . . 9
⊢ ((seq1( +
, ((abs ∘ − ) ∘ 𝑓))‘1) ∈ (0[,)+∞) ↔
((seq1( + , ((abs ∘ − ) ∘ 𝑓))‘1) ∈ ℝ ∧ 0 ≤
(seq1( + , ((abs ∘ − ) ∘ 𝑓))‘1))) |
15 | 14 | simprbi 479 |
. . . . . . . 8
⊢ ((seq1( +
, ((abs ∘ − ) ∘ 𝑓))‘1) ∈ (0[,)+∞) → 0
≤ (seq1( + , ((abs ∘ − ) ∘ 𝑓))‘1)) |
16 | 13, 15 | syl 17 |
. . . . . . 7
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 0 ≤ (seq1( + , ((abs ∘ − )
∘ 𝑓))‘1)) |
17 | | frn 5966 |
. . . . . . . . . 10
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞) → ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ (0[,)+∞)) |
18 | 10, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ran seq1( + , ((abs ∘ − ) ∘
𝑓)) ⊆
(0[,)+∞)) |
19 | | icossxr 12129 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ* |
20 | 18, 19 | syl6ss 3580 |
. . . . . . . 8
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ran seq1( + , ((abs ∘ − ) ∘
𝑓)) ⊆
ℝ*) |
21 | | ffn 5958 |
. . . . . . . . . 10
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞) → seq1(
+ , ((abs ∘ − ) ∘ 𝑓)) Fn ℕ) |
22 | 10, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘
𝑓)) Fn
ℕ) |
23 | | fnfvelrn 6264 |
. . . . . . . . 9
⊢ ((seq1( +
, ((abs ∘ − ) ∘ 𝑓)) Fn ℕ ∧ 1 ∈ ℕ) →
(seq1( + , ((abs ∘ − ) ∘ 𝑓))‘1) ∈ ran seq1( + , ((abs
∘ − ) ∘ 𝑓))) |
24 | 22, 11, 23 | sylancl 693 |
. . . . . . . 8
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (seq1( + , ((abs ∘ − ) ∘
𝑓))‘1) ∈ ran
seq1( + , ((abs ∘ − ) ∘ 𝑓))) |
25 | | supxrub 12026 |
. . . . . . . 8
⊢ ((ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ ℝ* ∧ (seq1( +
, ((abs ∘ − ) ∘ 𝑓))‘1) ∈ ran seq1( + , ((abs
∘ − ) ∘ 𝑓))) → (seq1( + , ((abs ∘ − )
∘ 𝑓))‘1) ≤
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
)) |
26 | 20, 24, 25 | syl2anc 691 |
. . . . . . 7
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (seq1( + , ((abs ∘ − ) ∘
𝑓))‘1) ≤ sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
)) |
27 | 19, 13 | sseldi 3566 |
. . . . . . . 8
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → (seq1( + , ((abs ∘ − ) ∘
𝑓))‘1) ∈
ℝ*) |
28 | | supxrcl 12017 |
. . . . . . . . 9
⊢ (ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ ℝ* → sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈
ℝ*) |
29 | 20, 28 | syl 17 |
. . . . . . . 8
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ) ∈ ℝ*) |
30 | | 0xr 9965 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
31 | | xrletr 11865 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ (seq1( + , ((abs ∘ − ) ∘
𝑓))‘1) ∈
ℝ* ∧ sup(ran seq1( + , ((abs ∘ − ) ∘
𝑓)), ℝ*,
< ) ∈ ℝ*) → ((0 ≤ (seq1( + , ((abs ∘
− ) ∘ 𝑓))‘1) ∧ (seq1( + , ((abs ∘
− ) ∘ 𝑓))‘1) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) → 0
≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
))) |
32 | 30, 31 | mp3an1 1403 |
. . . . . . . 8
⊢ (((seq1(
+ , ((abs ∘ − ) ∘ 𝑓))‘1) ∈ ℝ* ∧
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈
ℝ*) → ((0 ≤ (seq1( + , ((abs ∘ − ) ∘
𝑓))‘1) ∧ (seq1( +
, ((abs ∘ − ) ∘ 𝑓))‘1) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) → 0
≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
))) |
33 | 27, 29, 32 | syl2anc 691 |
. . . . . . 7
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((0 ≤ (seq1( + , ((abs ∘ − )
∘ 𝑓))‘1) ∧
(seq1( + , ((abs ∘ − ) ∘ 𝑓))‘1) ≤ sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) → 0
≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
))) |
34 | 16, 26, 33 | mp2and 711 |
. . . . . 6
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 0 ≤ sup(ran seq1( + , ((abs ∘
− ) ∘ 𝑓)),
ℝ*, < )) |
35 | 7, 34 | sylbi 206 |
. . . . 5
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → 0 ≤ sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
)) |
36 | | breq2 4587 |
. . . . 5
⊢ (𝐵 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < ) → (0
≤ 𝐵 ↔ 0 ≤
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, <
))) |
37 | 35, 36 | syl5ibrcom 236 |
. . . 4
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → (𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ) → 0 ≤ 𝐵)) |
38 | 37 | adantld 482 |
. . 3
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → ((𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → 0 ≤ 𝐵)) |
39 | 38 | rexlimiv 3009 |
. 2
⊢
(∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → 0 ≤ 𝐵) |
40 | 2, 39 | sylbi 206 |
1
⊢ (𝐵 ∈ 𝑀 → 0 ≤ 𝐵) |