Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for David A. Wheeler
Miscellaneous
5m4e1
Next ⟩
2p2ne5
Metamath Proof Explorer
Ascii
Unicode
Theorem
5m4e1
Description:
Prove that 5 - 4 = 1.
(Contributed by
David A. Wheeler
, 31-Jan-2017)
Ref
Expression
Assertion
5m4e1
⊢
5
−
4
=
1
Proof
Step
Hyp
Ref
Expression
1
5cn
⊢
5
∈
ℂ
2
4cn
⊢
4
∈
ℂ
3
ax-1cn
⊢
1
∈
ℂ
4
4p1e5
⊢
4
+
1
=
5
5
1
2
3
4
subaddrii
⊢
5
−
4
=
1