Metamath Proof Explorer


Theorem abvge0

Description: The absolute value of a number is greater than or equal to zero. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses abvf.a 𝐴 = ( AbsVal ‘ 𝑅 )
abvf.b 𝐵 = ( Base ‘ 𝑅 )
Assertion abvge0 ( ( 𝐹𝐴𝑋𝐵 ) → 0 ≤ ( 𝐹𝑋 ) )

Proof

Step Hyp Ref Expression
1 abvf.a 𝐴 = ( AbsVal ‘ 𝑅 )
2 abvf.b 𝐵 = ( Base ‘ 𝑅 )
3 1 2 abvfge0 ( 𝐹𝐴𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) )
4 3 ffvelrnda ( ( 𝐹𝐴𝑋𝐵 ) → ( 𝐹𝑋 ) ∈ ( 0 [,) +∞ ) )
5 elrege0 ( ( 𝐹𝑋 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹𝑋 ) ∈ ℝ ∧ 0 ≤ ( 𝐹𝑋 ) ) )
6 5 simprbi ( ( 𝐹𝑋 ) ∈ ( 0 [,) +∞ ) → 0 ≤ ( 𝐹𝑋 ) )
7 4 6 syl ( ( 𝐹𝐴𝑋𝐵 ) → 0 ≤ ( 𝐹𝑋 ) )