Theorem 2picn

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

	Ref	Expression
Assertion	2picn	⊢ ( 2 · π ) ∈ ℂ

Proof

Step	Hyp	Ref	Expression
1		2cn	⊢ 2 ∈ ℂ
2		picn	⊢ π ∈ ℂ
3	1 2	mulcli	⊢ ( 2 · π ) ∈ ℂ