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

Metamath Proof Explorer

Theorem ge0p1rp

Description: A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Assertion ge0p1rp ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝐴 + 1 ) ∈ ℝ+ )

Proof

Step Hyp Ref Expression
1 peano2re ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝐴 + 1 ) ∈ ℝ )
3 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ∈ ℝ )
4 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
5 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ 𝐴 )
6 ltp1 ⊢ ( 𝐴 ∈ ℝ → 𝐴 < ( 𝐴 + 1 ) )
7 6 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 < ( 𝐴 + 1 ) )
8 3 4 2 5 7 lelttrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 < ( 𝐴 + 1 ) )
9 elrp ⊢ ( ( 𝐴 + 1 ) ∈ ℝ+ ↔ ( ( 𝐴 + 1 ) ∈ ℝ ∧ 0 < ( 𝐴 + 1 ) ) )
10 2 8 9 sylanbrc ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝐴 + 1 ) ∈ ℝ+ )