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

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 ⊢ φ → A ∈ ℝ
rpgecld.2 ⊢ φ → B ∈ ℝ +
rpgecld.3 ⊢ φ → B ≤ A
Assertion rpgecld ⊢ φ → A ∈ ℝ +

Proof

Step Hyp Ref Expression
1 rpgecld.1 ⊢ φ → A ∈ ℝ
2 rpgecld.2 ⊢ φ → B ∈ ℝ +
3 rpgecld.3 ⊢ φ → B ≤ A
4 rpgecl ⊢ B ∈ ℝ + ∧ A ∈ ℝ ∧ B ≤ A → A ∈ ℝ +
5 2 1 3 4 syl3anc ⊢ φ → A ∈ ℝ +