Metamath Proof Explorer


Theorem rpgecld

Description: A number greater than or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses rpgecld.1 ( 𝜑𝐴 ∈ ℝ )
rpgecld.2 ( 𝜑𝐵 ∈ ℝ+ )
rpgecld.3 ( 𝜑𝐵𝐴 )
Assertion rpgecld ( 𝜑𝐴 ∈ ℝ+ )

Proof

Step Hyp Ref Expression
1 rpgecld.1 ( 𝜑𝐴 ∈ ℝ )
2 rpgecld.2 ( 𝜑𝐵 ∈ ℝ+ )
3 rpgecld.3 ( 𝜑𝐵𝐴 )
4 rpgecl ( ( 𝐵 ∈ ℝ+𝐴 ∈ ℝ ∧ 𝐵𝐴 ) → 𝐴 ∈ ℝ+ )
5 2 1 3 4 syl3anc ( 𝜑𝐴 ∈ ℝ+ )