Theorem rpge0

Description: A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008)

	Ref	Expression
Assertion	rpge0	⊢ ( 𝐴 ∈ ℝ+ → 0 ≤ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rpre	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
2		rpgt0	⊢ ( 𝐴 ∈ ℝ+ → 0 < 𝐴 )
3		0re	⊢ 0 ∈ ℝ
4		ltle	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
5	3 4	mpan	⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
6	1 2 5	sylc	⊢ ( 𝐴 ∈ ℝ+ → 0 ≤ 𝐴 )