Theorem 2cn 9308

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 9307	. 2 |- 2 e. RR
2	1	recni 8286	1 |- 2 e. CC

Syntax hints:   e. wcel 2203   CCcc 8125   2c2 9288

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-resscn 8219  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224  df-2 9296

This theorem is referenced by:  2ex  9309  2cnd  9310  2m1e1  9355  3m1e2  9357  2p2e4  9364  times2  9366  2div2e1  9370  1p2e3  9372  3p3e6  9380  4p3e7  9382  5p3e8  9385  6p3e9  9388  2t1e2  9391  2t2e4  9392  3t3e9  9395  2t0e0  9397  4d2e2  9398  2cnne0  9447  1mhlfehlf  9456  8th4div3  9457  halfpm6th  9458  2mulicn  9460  2muliap0  9462  halfcl  9464  half0  9466  2halves  9467  halfaddsub  9472  div4p1lem1div2  9492  3halfnz  9675  zneo  9679  nneoor  9680  zeo  9683  7p3e10  9783  4t4e16  9807  6t3e18  9813  7t7e49  9822  8t5e40  9826  9t9e81  9837  decbin0  9848  decbin2  9849  halfthird  9851  fztpval  10417  fz0tp  10456  fz0to4untppr  10458  fzo0to3tp  10564  2tnp1ge0ge0  10661  fldiv4lem1div2  10667  expubnd  10958  sq2  10997  sq4e2t8  10999  cu2  11000  subsq2  11009  binom2sub  11015  binom3  11019  zesq  11020  fac2  11093  fac3  11094  faclbnd2  11104  bcn2  11126  4bc2eq6  11137  crre  11542  addcj  11576  imval2  11579  resqrexlemover  11695  resqrexlemcalc1  11699  resqrexlemnm  11703  resqrexlemcvg  11704  amgm2  11803  arisum  12184  arisum2  12185  geo2sum2  12201  geo2lim  12202  geoihalfsum  12208  efcllemp  12344  ege2le3  12357  tanval2ap  12399  tanval3ap  12400  efi4p  12403  efival  12418  sinadd  12422  cosadd  12423  sinmul  12430  cosmul  12431  cos2tsin  12437  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  cos1bnd  12445  cos2bnd  12446  cos01gt0  12449  sin02gt0  12450  sin4lt0  12453  cos12dec  12454  egt2lt3  12466  odd2np1lem  12558  odd2np1  12559  ltoddhalfle  12579  halfleoddlt  12580  opoe  12581  omoe  12582  opeo  12583  omeo  12584  nno  12592  nn0o  12593  flodddiv4  12622  bits0  12634  bitsfzolem  12640  0bits  12645  bitsinv1  12648  6gcd4e2  12691  3lcm2e6woprm  12783  6lcm4e12  12784  sqrt2irrlem  12858  oddpwdclemodd  12869  pythagtriplem1  12963  pythagtriplem12  12973  pythagtriplem14  12975  4sqlem11  13099  4sqlem12  13100  dec5dvds  13110  dec2nprm  13113  2exp5  13130  2exp6  13131  2exp7  13132  2exp8  13133  2exp11  13134  2exp16  13135  ballotfilem2  13142  maxcncf  15480  mincncf  15481  coscn  15635  sinhalfpilem  15656  cospi  15665  ef2pi  15670  ef2kpi  15671  efper  15672  sinperlem  15673  sin2kpi  15676  cos2kpi  15677  sin2pim  15678  cos2pim  15679  ptolemy  15689  sincosq3sgn  15693  sincosq4sgn  15694  sinq12gt0  15695  cosq23lt0  15698  coseq00topi  15700  tangtx  15703  sincos4thpi  15705  sincos6thpi  15707  sincos3rdpi  15708  pigt3  15709  abssinper  15711  coskpi  15713  cosq34lt1  15715  logsqrt  15788  2logb9irrALT  15839  1sgm2ppw  15863  perfect1  15866  perfectlem1  15867  perfectlem2  15868  perfect  15869  lgsdir2lem2  15902  gausslemma2dlem6  15940  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem2  15955  m1lgs  15958  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2lgsoddprmlem2  15979  2lgsoddprmlem3c  15982  2lgsoddprmlem3d  15983  clwwlknonex2  16434  ex-fl  16493  ex-ceil  16494  ex-exp  16495  ex-fac  16496