Database
REAL AND COMPLEX NUMBERS
Real and complex numbers - basic operations
Division
1div1e1
Next ⟩
diveq1
Metamath Proof Explorer
Ascii
Unicode
Theorem
1div1e1
Description:
1 divided by 1 is 1.
(Contributed by
David A. Wheeler
, 7-Dec-2018)
Ref
Expression
Assertion
1div1e1
⊢
1
1
=
1
Proof
Step
Hyp
Ref
Expression
1
ax-1cn
⊢
1
∈
ℂ
2
div1
⊢
1
∈
ℂ
→
1
1
=
1
3
1
2
ax-mp
⊢
1
1
=
1