Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
2div2e1
Next ⟩
2p1e3
Metamath Proof Explorer
Ascii
Structured
Theorem
2div2e1
Description:
2 divided by 2 is 1.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
2div2e1
⊢
( 2 / 2 ) = 1
Proof
Step
Hyp
Ref
Expression
1
2cn
⊢
2 ∈ ℂ
2
2ne0
⊢
2 ≠ 0
3
1
2
dividi
⊢
( 2 / 2 ) = 1