Theorem 3cn 9217

Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)

Assertion

Ref	Expression
3cn	⊢ 3 ∈ ℂ

Proof of Theorem 3cn

Step	Hyp	Ref	Expression
1		3re 9216	. 2 ⊢ 3 ∈ ℝ
2	1	recni 8190	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2202  ℂcc 8029  3c3 9194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8123  ax-1re 8125  ax-addrcl 8128

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213  df-2 9201  df-3 9202

This theorem is referenced by:  3ex  9218  3m1e2  9262  4m1e3  9263  3p2e5  9284  3p3e6  9285  4p4e8  9288  5p4e9  9291  3t1e3  9298  3t2e6  9299  3t3e9  9300  8th4div3  9362  halfpm6th  9363  6p4e10  9681  9t8e72  9737  halfthird  9752  fzo0to42pr  10464  sq3  10897  expnass  10906  fac3  10993  4bc3eq4  11034  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  cos1bnd  12319  cos2bnd  12320  cos01gt0  12323  3dvdsdec  12425  3dvds2dec  12426  5ndvds3  12494  3lcm2e6woprm  12657  2exp6  13005  2exp16  13009  cosq23lt0  15556  tangtx  15561  sincos6thpi  15565  sincos3rdpi  15566  pigt3  15567  binom4  15702  lgsdir2lem1  15756  lgsdir2lem5  15760  2lgslem3b  15822  2lgslem3d  15824  2lgsoddprmlem3c  15837  2lgsoddprmlem3d  15838  ex-exp  16323  ex-dvds  16326  ex-gcd  16327