Theorem 2picn

Description: ( 2 x. _pi ) is a complex number. (Contributed by Umit Teoman Dogan, 10-Jun-2026)

	Ref	Expression
Assertion	2picn	$$⊢2\mathrm{\pi }\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2		picn	$$⊢\mathrm{\pi }\in ℂ$$
3	1 2	mulcli	$$⊢2\mathrm{\pi }\in ℂ$$