Theorem 2cn 9142

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 9141	. 2 |- 2 e. RR
2	1	recni 8119	1 |- 2 e. CC

Syntax hints:   e. wcel 2178   CCcc 7958   2c2 9122

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-resscn 8052  ax-1re 8054  ax-addrcl 8057

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187  df-2 9130

This theorem is referenced by:  2ex  9143  2cnd  9144  2m1e1  9189  3m1e2  9191  2p2e4  9198  times2  9200  2div2e1  9204  1p2e3  9206  3p3e6  9214  4p3e7  9216  5p3e8  9219  6p3e9  9222  2t1e2  9225  2t2e4  9226  3t3e9  9229  2t0e0  9231  4d2e2  9232  2cnne0  9281  1mhlfehlf  9290  8th4div3  9291  halfpm6th  9292  2mulicn  9294  2muliap0  9296  halfcl  9298  half0  9300  2halves  9301  halfaddsub  9306  div4p1lem1div2  9326  3halfnz  9505  zneo  9509  nneoor  9510  zeo  9513  7p3e10  9613  4t4e16  9637  6t3e18  9643  7t7e49  9652  8t5e40  9656  9t9e81  9667  decbin0  9678  decbin2  9679  halfthird  9681  fztpval  10240  fz0tp  10279  fz0to4untppr  10281  fzo0to3tp  10385  2tnp1ge0ge0  10481  fldiv4lem1div2  10487  expubnd  10778  sq2  10817  sq4e2t8  10819  cu2  10820  subsq2  10829  binom2sub  10835  binom3  10839  zesq  10840  fac2  10913  fac3  10914  faclbnd2  10924  bcn2  10946  4bc2eq6  10956  crre  11283  addcj  11317  imval2  11320  resqrexlemover  11436  resqrexlemcalc1  11440  resqrexlemnm  11444  resqrexlemcvg  11445  amgm2  11544  arisum  11924  arisum2  11925  geo2sum2  11941  geo2lim  11942  geoihalfsum  11948  efcllemp  12084  ege2le3  12097  tanval2ap  12139  tanval3ap  12140  efi4p  12143  efival  12158  sinadd  12162  cosadd  12163  sinmul  12170  cosmul  12171  cos2tsin  12177  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  cos1bnd  12185  cos2bnd  12186  cos01gt0  12189  sin02gt0  12190  sin4lt0  12193  cos12dec  12194  egt2lt3  12206  odd2np1lem  12298  odd2np1  12299  ltoddhalfle  12319  halfleoddlt  12320  opoe  12321  omoe  12322  opeo  12323  omeo  12324  nno  12332  nn0o  12333  flodddiv4  12362  bits0  12374  bitsfzolem  12380  0bits  12385  bitsinv1  12388  6gcd4e2  12431  3lcm2e6woprm  12523  6lcm4e12  12524  sqrt2irrlem  12598  oddpwdclemodd  12609  pythagtriplem1  12703  pythagtriplem12  12713  pythagtriplem14  12715  4sqlem11  12839  4sqlem12  12840  dec5dvds  12850  dec2nprm  12853  2exp5  12870  2exp6  12871  2exp7  12872  2exp8  12873  2exp11  12874  2exp16  12875  maxcncf  15202  mincncf  15203  coscn  15357  sinhalfpilem  15378  cospi  15387  ef2pi  15392  ef2kpi  15393  efper  15394  sinperlem  15395  sin2kpi  15398  cos2kpi  15399  sin2pim  15400  cos2pim  15401  ptolemy  15411  sincosq3sgn  15415  sincosq4sgn  15416  sinq12gt0  15417  cosq23lt0  15420  coseq00topi  15422  tangtx  15425  sincos4thpi  15427  sincos6thpi  15429  sincos3rdpi  15430  pigt3  15431  abssinper  15433  coskpi  15435  cosq34lt1  15437  logsqrt  15510  2logb9irrALT  15561  1sgm2ppw  15582  perfect1  15585  perfectlem1  15586  perfectlem2  15587  perfect  15588  lgsdir2lem2  15621  gausslemma2dlem6  15659  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem2  15674  m1lgs  15677  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2lgsoddprmlem2  15698  2lgsoddprmlem3c  15701  2lgsoddprmlem3d  15702  ex-fl  15861  ex-ceil  15862  ex-exp  15863  ex-fac  15864