Theorem 3cn 9312

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 9311	. 2 ⊢ 3 ∈ ℝ
2	1	recni 8286	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2203  ℂcc 8125  3c3 9289

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-resscn 8219  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224  df-2 9296  df-3 9297

This theorem is referenced by:  3ex  9313  3m1e2  9357  4m1e3  9358  3p2e5  9379  3p3e6  9380  4p4e8  9383  5p4e9  9386  3t1e3  9393  3t2e6  9394  3t3e9  9395  8th4div3  9457  halfpm6th  9458  6p4e10  9780  9t8e72  9836  halfthird  9851  fzo0to42pr  10565  sq3  10998  expnass  11007  fac3  11094  4bc3eq4  11136  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  cos1bnd  12445  cos2bnd  12446  cos01gt0  12449  3dvdsdec  12551  3dvds2dec  12552  5ndvds3  12620  3lcm2e6woprm  12783  2exp6  13131  2exp16  13135  cosq23lt0  15698  tangtx  15703  sincos6thpi  15707  sincos3rdpi  15708  pigt3  15709  binom4  15844  lgsdir2lem1  15901  lgsdir2lem5  15905  2lgslem3b  15967  2lgslem3d  15969  2lgsoddprmlem3c  15982  2lgsoddprmlem3d  15983  ex-exp  16495  ex-dvds  16498  ex-gcd  16499