Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
0p1e1
Next ⟩
fv0p1e1
Metamath Proof Explorer
Ascii
Structured
Theorem
0p1e1
Description:
0 + 1 = 1.
(Contributed by
David A. Wheeler
, 7-Jul-2016)
Ref
Expression
Assertion
0p1e1
⊢
( 0 + 1 ) = 1
Proof
Step
Hyp
Ref
Expression
1
ax-1cn
⊢
1 ∈ ℂ
2
1
addid2i
⊢
( 0 + 1 ) = 1