Theorem 3cn 8923

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

Assertion

Ref	Expression
3cn	|- 3 e. CC

Proof of Theorem 3cn

Step	Hyp	Ref	Expression
1		3re 8922	. 2 |- 3 e. RR
2	1	recni 7902	1 |- 3 e. CC

Syntax hints:   e. wcel 2135   CCcc 7742   3c3 8900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146  ax-resscn 7836  ax-1re 7838  ax-addrcl 7841

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-in 3117  df-ss 3124  df-2 8907  df-3 8908

This theorem is referenced by:  3ex  8924  3m1e2  8968  4m1e3  8969  3p2e5  8989  3p3e6  8990  4p4e8  8993  5p4e9  8996  3t1e3  9003  3t2e6  9004  3t3e9  9005  8th4div3  9067  halfpm6th  9068  6p4e10  9384  9t8e72  9440  halfthird  9455  fzo0to42pr  10145  sq3  10541  expnass  10550  fac3  10634  4bc3eq4  10675  ef01bndlem  11683  sin01bnd  11684  cos01bnd  11685  cos1bnd  11686  cos2bnd  11687  cos01gt0  11689  3dvdsdec  11787  3dvds2dec  11788  3lcm2e6woprm  11997  cosq23lt0  13295  tangtx  13300  sincos6thpi  13304  sincos3rdpi  13305  pigt3  13306  binom4  13438  ex-exp  13445  ex-dvds  13448  ex-gcd  13449