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