Theorem 2cn 9061

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 9060	. 2 |- 2 e. RR
2	1	recni 8038	1 |- 2 e. CC

Syntax hints:   e. wcel 2167   CCcc 7877   2c2 9041

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7971  ax-1re 7973  ax-addrcl 7976

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170  df-2 9049

This theorem is referenced by:  2ex  9062  2cnd  9063  2m1e1  9108  3m1e2  9110  2p2e4  9117  times2  9119  2div2e1  9123  1p2e3  9125  3p3e6  9133  4p3e7  9135  5p3e8  9138  6p3e9  9141  2t1e2  9144  2t2e4  9145  3t3e9  9148  2t0e0  9150  4d2e2  9151  2cnne0  9200  1mhlfehlf  9209  8th4div3  9210  halfpm6th  9211  2mulicn  9213  2muliap0  9215  halfcl  9217  half0  9219  2halves  9220  halfaddsub  9225  div4p1lem1div2  9245  3halfnz  9423  zneo  9427  nneoor  9428  zeo  9431  7p3e10  9531  4t4e16  9555  6t3e18  9561  7t7e49  9570  8t5e40  9574  9t9e81  9585  decbin0  9596  decbin2  9597  halfthird  9599  fztpval  10158  fz0tp  10197  fz0to4untppr  10199  fzo0to3tp  10295  2tnp1ge0ge0  10391  fldiv4lem1div2  10397  expubnd  10688  sq2  10727  sq4e2t8  10729  cu2  10730  subsq2  10739  binom2sub  10745  binom3  10749  zesq  10750  fac2  10823  fac3  10824  faclbnd2  10834  bcn2  10856  4bc2eq6  10866  crre  11022  addcj  11056  imval2  11059  resqrexlemover  11175  resqrexlemcalc1  11179  resqrexlemnm  11183  resqrexlemcvg  11184  amgm2  11283  arisum  11663  arisum2  11664  geo2sum2  11680  geo2lim  11681  geoihalfsum  11687  efcllemp  11823  ege2le3  11836  tanval2ap  11878  tanval3ap  11879  efi4p  11882  efival  11897  sinadd  11901  cosadd  11902  sinmul  11909  cosmul  11910  cos2tsin  11916  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  cos1bnd  11924  cos2bnd  11925  cos01gt0  11928  sin02gt0  11929  sin4lt0  11932  cos12dec  11933  egt2lt3  11945  odd2np1lem  12037  odd2np1  12038  ltoddhalfle  12058  halfleoddlt  12059  opoe  12060  omoe  12061  opeo  12062  omeo  12063  nno  12071  nn0o  12072  flodddiv4  12101  bits0  12112  bitsfzolem  12118  6gcd4e2  12162  3lcm2e6woprm  12254  6lcm4e12  12255  sqrt2irrlem  12329  oddpwdclemodd  12340  pythagtriplem1  12434  pythagtriplem12  12444  pythagtriplem14  12446  4sqlem11  12570  4sqlem12  12571  dec5dvds  12581  dec2nprm  12584  2exp5  12601  2exp6  12602  2exp7  12603  2exp8  12604  2exp11  12605  2exp16  12606  maxcncf  14851  mincncf  14852  coscn  15006  sinhalfpilem  15027  cospi  15036  ef2pi  15041  ef2kpi  15042  efper  15043  sinperlem  15044  sin2kpi  15047  cos2kpi  15048  sin2pim  15049  cos2pim  15050  ptolemy  15060  sincosq3sgn  15064  sincosq4sgn  15065  sinq12gt0  15066  cosq23lt0  15069  coseq00topi  15071  tangtx  15074  sincos4thpi  15076  sincos6thpi  15078  sincos3rdpi  15079  pigt3  15080  abssinper  15082  coskpi  15084  cosq34lt1  15086  logsqrt  15159  2logb9irrALT  15210  1sgm2ppw  15231  perfect1  15234  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgsdir2lem2  15270  gausslemma2dlem6  15308  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem2  15323  m1lgs  15326  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2lgsoddprmlem2  15347  2lgsoddprmlem3c  15350  2lgsoddprmlem3d  15351  ex-fl  15371  ex-ceil  15372  ex-exp  15373  ex-fac  15374