Metamath Proof Explorer

Theorem ovolmge0

Description: The set M is composed of nonnegative extended real numbers. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypothesis elovolm.1 ⊢ 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
Assertion ovolmge0 ( 𝐵 ∈ 𝑀 → 0 ≤ 𝐵 )

Proof

Step Hyp Ref Expression
1 elovolm.1 ⊢ 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
2 1 elovolm ⊢ ( 𝐵 ∈ 𝑀 ↔ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) )
3 elovolmlem ⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
4 eqid ⊢ ( ( abs ∘ − ) ∘ 𝑓 ) = ( ( abs ∘ − ) ∘ 𝑓 )
5 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) )
6 4 5 ovolsf ⊢ ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
7 1nn ⊢ 1 ∈ ℕ
8 ffvelrn ⊢ ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) : ℕ ⟶ ( 0 [,) +∞ ) ∧ 1 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ∈ ( 0 [,) +∞ ) )
9 6 7 8 sylancl ⊢ ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ∈ ( 0 [,) +∞ ) )
10 elrege0 ⊢ ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ∈ ( 0 [,) +∞ ) ↔ ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ∈ ℝ ∧ 0 ≤ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ) )
11 10 simprbi ⊢ ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ∈ ( 0 [,) +∞ ) → 0 ≤ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) )
12 9 11 syl ⊢ ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 0 ≤ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) )
13 6 frnd ⊢ ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ⊆ ( 0 [,) +∞ ) )
14 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
15 13 14 sstrdi ⊢ ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ⊆ ℝ* )
16 6 ffnd ⊢ ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) Fn ℕ )
17 fnfvelrn ⊢ ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) Fn ℕ ∧ 1 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) )
18 16 7 17 sylancl ⊢ ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) )
19 supxrub ⊢ ( ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ⊆ ℝ* ∧ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) )
20 15 18 19 syl2anc ⊢ ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) )
21 0xr ⊢ 0 ∈ ℝ*
22 14 9 sseldi ⊢ ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ∈ ℝ* )
23 supxrcl ⊢ ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ⊆ ℝ* → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ∈ ℝ* )
24 15 23 syl ⊢ ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ∈ ℝ* )
25 xrletr ⊢ ( ( 0 ∈ ℝ* ∧ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ∈ ℝ* ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ∈ ℝ* ) → ( ( 0 ≤ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ∧ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) → 0 ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) )
26 21 22 24 25 mp3an2i ⊢ ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( 0 ≤ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ∧ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) ‘ 1 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) → 0 ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) )
27 12 20 26 mp2and ⊢ ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 0 ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) )
28 3 27 sylbi ⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → 0 ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) )
29 breq2 ⊢ ( 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) → ( 0 ≤ 𝐵 ↔ 0 ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) )
30 28 29 syl5ibrcom ⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) → 0 ≤ 𝐵 ) )
31 30 adantld ⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) → 0 ≤ 𝐵 ) )
32 31 rexlimiv ⊢ ( ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝐵 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) → 0 ≤ 𝐵 )
33 2 32 sylbi ⊢ ( 𝐵 ∈ 𝑀 → 0 ≤ 𝐵 )