Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
sn-ltp1
Next ⟩
reneg1lt0
Metamath Proof Explorer
Ascii
Unicode
Theorem
sn-ltp1
Description:
ltp1
without
ax-mulcom
.
(Contributed by
SN
, 13-Feb-2024)
Ref
Expression
Assertion
sn-ltp1
⊢
A
∈
ℝ
→
A
<
A
+
1
Proof
Step
Hyp
Ref
Expression
1
1re
⊢
1
∈
ℝ
2
sn-0lt1
⊢
0
<
1
3
sn-ltaddpos
⊢
1
∈
ℝ
∧
A
∈
ℝ
→
0
<
1
↔
A
<
A
+
1
4
2
3
mpbii
⊢
1
∈
ℝ
∧
A
∈
ℝ
→
A
<
A
+
1
5
1
4
mpan
⊢
A
∈
ℝ
→
A
<
A
+
1