Theorem 2cn 9055

Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)

Assertion

Ref	Expression
2cn	|- 2 e. CC

Proof of Theorem 2cn

Step	Hyp	Ref	Expression
1		2re 9054	. 2 |- 2 e. RR
2	1	recni 8033	1 |- 2 e. CC

Syntax hints:   e. wcel 2164   CCcc 7872   2c2 9035

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7966  ax-1re 7968  ax-addrcl 7971

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167  df-2 9043

This theorem is referenced by:  2ex  9056  2cnd  9057  2m1e1  9102  3m1e2  9104  2p2e4  9111  times2  9113  2div2e1  9117  1p2e3  9119  3p3e6  9127  4p3e7  9129  5p3e8  9132  6p3e9  9135  2t1e2  9138  2t2e4  9139  3t3e9  9142  2t0e0  9144  4d2e2  9145  2cnne0  9194  1mhlfehlf  9203  8th4div3  9204  halfpm6th  9205  2mulicn  9207  2muliap0  9209  halfcl  9211  half0  9213  2halves  9214  halfaddsub  9219  div4p1lem1div2  9239  3halfnz  9417  zneo  9421  nneoor  9422  zeo  9425  7p3e10  9525  4t4e16  9549  6t3e18  9555  7t7e49  9564  8t5e40  9568  9t9e81  9579  decbin0  9590  decbin2  9591  halfthird  9593  fztpval  10152  fz0tp  10191  fz0to4untppr  10193  fzo0to3tp  10289  2tnp1ge0ge0  10373  fldiv4lem1div2  10379  expubnd  10670  sq2  10709  sq4e2t8  10711  cu2  10712  subsq2  10721  binom2sub  10727  binom3  10731  zesq  10732  fac2  10805  fac3  10806  faclbnd2  10816  bcn2  10838  4bc2eq6  10848  crre  11004  addcj  11038  imval2  11041  resqrexlemover  11157  resqrexlemcalc1  11161  resqrexlemnm  11165  resqrexlemcvg  11166  amgm2  11265  arisum  11644  arisum2  11645  geo2sum2  11661  geo2lim  11662  geoihalfsum  11668  efcllemp  11804  ege2le3  11817  tanval2ap  11859  tanval3ap  11860  efi4p  11863  efival  11878  sinadd  11882  cosadd  11883  sinmul  11890  cosmul  11891  cos2tsin  11897  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  cos1bnd  11905  cos2bnd  11906  cos01gt0  11909  sin02gt0  11910  sin4lt0  11913  cos12dec  11914  egt2lt3  11926  odd2np1lem  12016  odd2np1  12017  ltoddhalfle  12037  halfleoddlt  12038  opoe  12039  omoe  12040  opeo  12041  omeo  12042  nno  12050  nn0o  12051  flodddiv4  12078  6gcd4e2  12135  3lcm2e6woprm  12227  6lcm4e12  12228  sqrt2irrlem  12302  oddpwdclemodd  12313  pythagtriplem1  12406  pythagtriplem12  12416  pythagtriplem14  12418  4sqlem11  12542  4sqlem12  12543  maxcncf  14794  mincncf  14795  coscn  14946  sinhalfpilem  14967  cospi  14976  ef2pi  14981  ef2kpi  14982  efper  14983  sinperlem  14984  sin2kpi  14987  cos2kpi  14988  sin2pim  14989  cos2pim  14990  ptolemy  15000  sincosq3sgn  15004  sincosq4sgn  15005  sinq12gt0  15006  cosq23lt0  15009  coseq00topi  15011  tangtx  15014  sincos4thpi  15016  sincos6thpi  15018  sincos3rdpi  15019  pigt3  15020  abssinper  15022  coskpi  15024  cosq34lt1  15026  logsqrt  15098  2logb9irrALT  15147  lgsdir2lem2  15186  gausslemma2dlem6  15224  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem2  15239  m1lgs  15242  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgsoddprmlem2  15263  2lgsoddprmlem3c  15266  2lgsoddprmlem3d  15267  ex-fl  15287  ex-ceil  15288  ex-exp  15289  ex-fac  15290