Theorem rpgecl

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

	Ref	Expression
Assertion	rpgecl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		simp2	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
2		0red	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 0 ∈ ℝ )
3		rpre	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
4	3	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ )
5		rpgt0	⊢ ( 𝐴 ∈ ℝ+ → 0 < 𝐴 )
6	5	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 0 < 𝐴 )
7		simp3	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
8	2 4 1 6 7	ltletrd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 0 < 𝐵 )
9		elrp	⊢ ( 𝐵 ∈ ℝ+ ↔ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
10	1 8 9	sylanbrc	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ+ )