Database
REAL AND COMPLEX NUMBERS
Integer sets
Decimal representation of numbers
2thalfe1
Next ⟩
3pos
Metamath Proof Explorer
Ascii
Unicode
Theorem
2thalfe1
Description:
2 times one half equals 1.
(Contributed by
Umit Teoman Dogan
, 10-Jun-2026)
Ref
Expression
Assertion
2thalfe1
⊢
2
⁢
1
2
=
1
Proof
Step
Hyp
Ref
Expression
1
2cn
⊢
2
∈
ℂ
2
2ne0
⊢
2
≠
0
3
1
2
recidi
⊢
2
⁢
1
2
=
1