Theorem 2cn 9213

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 9212	. 2 |- 2 e. RR
2	1	recni 8190	1 |- 2 e. CC

Syntax hints:   e. wcel 2202   CCcc 8029   2c2 9193

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

This theorem is referenced by:  2ex  9214  2cnd  9215  2m1e1  9260  3m1e2  9262  2p2e4  9269  times2  9271  2div2e1  9275  1p2e3  9277  3p3e6  9285  4p3e7  9287  5p3e8  9290  6p3e9  9293  2t1e2  9296  2t2e4  9297  3t3e9  9300  2t0e0  9302  4d2e2  9303  2cnne0  9352  1mhlfehlf  9361  8th4div3  9362  halfpm6th  9363  2mulicn  9365  2muliap0  9367  halfcl  9369  half0  9371  2halves  9372  halfaddsub  9377  div4p1lem1div2  9397  3halfnz  9576  zneo  9580  nneoor  9581  zeo  9584  7p3e10  9684  4t4e16  9708  6t3e18  9714  7t7e49  9723  8t5e40  9727  9t9e81  9738  decbin0  9749  decbin2  9750  halfthird  9752  fztpval  10317  fz0tp  10356  fz0to4untppr  10358  fzo0to3tp  10463  2tnp1ge0ge0  10560  fldiv4lem1div2  10566  expubnd  10857  sq2  10896  sq4e2t8  10898  cu2  10899  subsq2  10908  binom2sub  10914  binom3  10918  zesq  10919  fac2  10992  fac3  10993  faclbnd2  11003  bcn2  11025  4bc2eq6  11035  crre  11417  addcj  11451  imval2  11454  resqrexlemover  11570  resqrexlemcalc1  11574  resqrexlemnm  11578  resqrexlemcvg  11579  amgm2  11678  arisum  12058  arisum2  12059  geo2sum2  12075  geo2lim  12076  geoihalfsum  12082  efcllemp  12218  ege2le3  12231  tanval2ap  12273  tanval3ap  12274  efi4p  12277  efival  12292  sinadd  12296  cosadd  12297  sinmul  12304  cosmul  12305  cos2tsin  12311  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  cos1bnd  12319  cos2bnd  12320  cos01gt0  12323  sin02gt0  12324  sin4lt0  12327  cos12dec  12328  egt2lt3  12340  odd2np1lem  12432  odd2np1  12433  ltoddhalfle  12453  halfleoddlt  12454  opoe  12455  omoe  12456  opeo  12457  omeo  12458  nno  12466  nn0o  12467  flodddiv4  12496  bits0  12508  bitsfzolem  12514  0bits  12519  bitsinv1  12522  6gcd4e2  12565  3lcm2e6woprm  12657  6lcm4e12  12658  sqrt2irrlem  12732  oddpwdclemodd  12743  pythagtriplem1  12837  pythagtriplem12  12847  pythagtriplem14  12849  4sqlem11  12973  4sqlem12  12974  dec5dvds  12984  dec2nprm  12987  2exp5  13004  2exp6  13005  2exp7  13006  2exp8  13007  2exp11  13008  2exp16  13009  maxcncf  15338  mincncf  15339  coscn  15493  sinhalfpilem  15514  cospi  15523  ef2pi  15528  ef2kpi  15529  efper  15530  sinperlem  15531  sin2kpi  15534  cos2kpi  15535  sin2pim  15536  cos2pim  15537  ptolemy  15547  sincosq3sgn  15551  sincosq4sgn  15552  sinq12gt0  15553  cosq23lt0  15556  coseq00topi  15558  tangtx  15561  sincos4thpi  15563  sincos6thpi  15565  sincos3rdpi  15566  pigt3  15567  abssinper  15569  coskpi  15571  cosq34lt1  15573  logsqrt  15646  2logb9irrALT  15697  1sgm2ppw  15718  perfect1  15721  perfectlem1  15722  perfectlem2  15723  perfect  15724  lgsdir2lem2  15757  gausslemma2dlem6  15795  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem2  15810  m1lgs  15813  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2lgsoddprmlem2  15834  2lgsoddprmlem3c  15837  2lgsoddprmlem3d  15838  clwwlknonex2  16289  ex-fl  16321  ex-ceil  16322  ex-exp  16323  ex-fac  16324