Metamath Proof Explorer


Theorem sn-ltp1

Description: ltp1 without ax-mulcom . (Contributed by SN, 13-Feb-2024)

Ref Expression
Assertion sn-ltp1 ( 𝐴 ∈ ℝ → 𝐴 < ( 𝐴 + 1 ) )

Proof

Step Hyp Ref Expression
1 1re 1 ∈ ℝ
2 sn-0lt1 0 < 1
3 sn-ltaddpos ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 1 ↔ 𝐴 < ( 𝐴 + 1 ) ) )
4 2 3 mpbii ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → 𝐴 < ( 𝐴 + 1 ) )
5 1 4 mpan ( 𝐴 ∈ ℝ → 𝐴 < ( 𝐴 + 1 ) )