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 ≤ ( 𝐹 ‘ 𝑋 ) )