This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrge0f

Description: A real function is a nonnegative extended real function if all its values are greater than or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 28-Jul-2014)

Ref Expression
Assertion xrge0f ( ( 𝐹 : ℝ ⟶ ℝ ∧ 0𝑝 ∘r ≤ 𝐹 ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 ffn ⊢ ( 𝐹 : ℝ ⟶ ℝ → 𝐹 Fn ℝ )
2 1 adantr ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 0𝑝 ∘r ≤ 𝐹 ) → 𝐹 Fn ℝ )
3 ax-resscn ⊢ ℝ ⊆ ℂ
4 3 a1i ⊢ ( 𝐹 : ℝ ⟶ ℝ → ℝ ⊆ ℂ )
5 4 1 0pledm ⊢ ( 𝐹 : ℝ ⟶ ℝ → ( 0𝑝 ∘r ≤ 𝐹 ↔ ( ℝ × { 0 } ) ∘r ≤ 𝐹 ) )
6 0re ⊢ 0 ∈ ℝ
7 fnconstg ⊢ ( 0 ∈ ℝ → ( ℝ × { 0 } ) Fn ℝ )
8 6 7 mp1i ⊢ ( 𝐹 : ℝ ⟶ ℝ → ( ℝ × { 0 } ) Fn ℝ )
9 reex ⊢ ℝ ∈ V
10 9 a1i ⊢ ( 𝐹 : ℝ ⟶ ℝ → ℝ ∈ V )
11 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
12 c0ex ⊢ 0 ∈ V
13 12 fvconst2 ⊢ ( 𝑥 ∈ ℝ → ( ( ℝ × { 0 } ) ‘ 𝑥 ) = 0 )
14 13 adantl ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ℝ × { 0 } ) ‘ 𝑥 ) = 0 )
15 eqidd ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
16 8 1 10 10 11 14 15 ofrfval ⊢ ( 𝐹 : ℝ ⟶ ℝ → ( ( ℝ × { 0 } ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
17 ffvelcdm ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
18 17 rexrd ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
19 18 biantrurd ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
20 elxrge0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
21 19 20 bitr4di ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) )
22 21 ralbidva ⊢ ( 𝐹 : ℝ ⟶ ℝ → ( ∀ 𝑥 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) )
23 5 16 22 3bitrd ⊢ ( 𝐹 : ℝ ⟶ ℝ → ( 0𝑝 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) )
24 23 biimpa ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 0𝑝 ∘r ≤ 𝐹 ) → ∀ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
25 ffnfv ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ↔ ( 𝐹 Fn ℝ ∧ ∀ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) )
26 2 24 25 sylanbrc ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 0𝑝 ∘r ≤ 𝐹 ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )