Theorem 2cn 9192

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 9191	. 2 |- 2 e. RR
2	1	recni 8169	1 |- 2 e. CC

Syntax hints:   e. wcel 2200   CCcc 8008   2c2 9172

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8102  ax-1re 8104  ax-addrcl 8107

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-2 9180

This theorem is referenced by:  2ex  9193  2cnd  9194  2m1e1  9239  3m1e2  9241  2p2e4  9248  times2  9250  2div2e1  9254  1p2e3  9256  3p3e6  9264  4p3e7  9266  5p3e8  9269  6p3e9  9272  2t1e2  9275  2t2e4  9276  3t3e9  9279  2t0e0  9281  4d2e2  9282  2cnne0  9331  1mhlfehlf  9340  8th4div3  9341  halfpm6th  9342  2mulicn  9344  2muliap0  9346  halfcl  9348  half0  9350  2halves  9351  halfaddsub  9356  div4p1lem1div2  9376  3halfnz  9555  zneo  9559  nneoor  9560  zeo  9563  7p3e10  9663  4t4e16  9687  6t3e18  9693  7t7e49  9702  8t5e40  9706  9t9e81  9717  decbin0  9728  decbin2  9729  halfthird  9731  fztpval  10291  fz0tp  10330  fz0to4untppr  10332  fzo0to3tp  10437  2tnp1ge0ge0  10533  fldiv4lem1div2  10539  expubnd  10830  sq2  10869  sq4e2t8  10871  cu2  10872  subsq2  10881  binom2sub  10887  binom3  10891  zesq  10892  fac2  10965  fac3  10966  faclbnd2  10976  bcn2  10998  4bc2eq6  11008  crre  11383  addcj  11417  imval2  11420  resqrexlemover  11536  resqrexlemcalc1  11540  resqrexlemnm  11544  resqrexlemcvg  11545  amgm2  11644  arisum  12024  arisum2  12025  geo2sum2  12041  geo2lim  12042  geoihalfsum  12048  efcllemp  12184  ege2le3  12197  tanval2ap  12239  tanval3ap  12240  efi4p  12243  efival  12258  sinadd  12262  cosadd  12263  sinmul  12270  cosmul  12271  cos2tsin  12277  ef01bndlem  12282  sin01bnd  12283  cos01bnd  12284  cos1bnd  12285  cos2bnd  12286  cos01gt0  12289  sin02gt0  12290  sin4lt0  12293  cos12dec  12294  egt2lt3  12306  odd2np1lem  12398  odd2np1  12399  ltoddhalfle  12419  halfleoddlt  12420  opoe  12421  omoe  12422  opeo  12423  omeo  12424  nno  12432  nn0o  12433  flodddiv4  12462  bits0  12474  bitsfzolem  12480  0bits  12485  bitsinv1  12488  6gcd4e2  12531  3lcm2e6woprm  12623  6lcm4e12  12624  sqrt2irrlem  12698  oddpwdclemodd  12709  pythagtriplem1  12803  pythagtriplem12  12813  pythagtriplem14  12815  4sqlem11  12939  4sqlem12  12940  dec5dvds  12950  dec2nprm  12953  2exp5  12970  2exp6  12971  2exp7  12972  2exp8  12973  2exp11  12974  2exp16  12975  maxcncf  15304  mincncf  15305  coscn  15459  sinhalfpilem  15480  cospi  15489  ef2pi  15494  ef2kpi  15495  efper  15496  sinperlem  15497  sin2kpi  15500  cos2kpi  15501  sin2pim  15502  cos2pim  15503  ptolemy  15513  sincosq3sgn  15517  sincosq4sgn  15518  sinq12gt0  15519  cosq23lt0  15522  coseq00topi  15524  tangtx  15527  sincos4thpi  15529  sincos6thpi  15531  sincos3rdpi  15532  pigt3  15533  abssinper  15535  coskpi  15537  cosq34lt1  15539  logsqrt  15612  2logb9irrALT  15663  1sgm2ppw  15684  perfect1  15687  perfectlem1  15688  perfectlem2  15689  perfect  15690  lgsdir2lem2  15723  gausslemma2dlem6  15761  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2lem2  15776  m1lgs  15779  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2lgsoddprmlem2  15800  2lgsoddprmlem3c  15803  2lgsoddprmlem3d  15804  ex-fl  16144  ex-ceil  16145  ex-exp  16146  ex-fac  16147