Theorem 2cn 9107

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 9106	. 2 |- 2 e. RR
2	1	recni 8084	1 |- 2 e. CC

Syntax hints:   e. wcel 2176   CCcc 7923   2c2 9087

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-resscn 8017  ax-1re 8019  ax-addrcl 8022

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179  df-2 9095

This theorem is referenced by:  2ex  9108  2cnd  9109  2m1e1  9154  3m1e2  9156  2p2e4  9163  times2  9165  2div2e1  9169  1p2e3  9171  3p3e6  9179  4p3e7  9181  5p3e8  9184  6p3e9  9187  2t1e2  9190  2t2e4  9191  3t3e9  9194  2t0e0  9196  4d2e2  9197  2cnne0  9246  1mhlfehlf  9255  8th4div3  9256  halfpm6th  9257  2mulicn  9259  2muliap0  9261  halfcl  9263  half0  9265  2halves  9266  halfaddsub  9271  div4p1lem1div2  9291  3halfnz  9470  zneo  9474  nneoor  9475  zeo  9478  7p3e10  9578  4t4e16  9602  6t3e18  9608  7t7e49  9617  8t5e40  9621  9t9e81  9632  decbin0  9643  decbin2  9644  halfthird  9646  fztpval  10205  fz0tp  10244  fz0to4untppr  10246  fzo0to3tp  10348  2tnp1ge0ge0  10444  fldiv4lem1div2  10450  expubnd  10741  sq2  10780  sq4e2t8  10782  cu2  10783  subsq2  10792  binom2sub  10798  binom3  10802  zesq  10803  fac2  10876  fac3  10877  faclbnd2  10887  bcn2  10909  4bc2eq6  10919  crre  11168  addcj  11202  imval2  11205  resqrexlemover  11321  resqrexlemcalc1  11325  resqrexlemnm  11329  resqrexlemcvg  11330  amgm2  11429  arisum  11809  arisum2  11810  geo2sum2  11826  geo2lim  11827  geoihalfsum  11833  efcllemp  11969  ege2le3  11982  tanval2ap  12024  tanval3ap  12025  efi4p  12028  efival  12043  sinadd  12047  cosadd  12048  sinmul  12055  cosmul  12056  cos2tsin  12062  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  cos1bnd  12070  cos2bnd  12071  cos01gt0  12074  sin02gt0  12075  sin4lt0  12078  cos12dec  12079  egt2lt3  12091  odd2np1lem  12183  odd2np1  12184  ltoddhalfle  12204  halfleoddlt  12205  opoe  12206  omoe  12207  opeo  12208  omeo  12209  nno  12217  nn0o  12218  flodddiv4  12247  bits0  12259  bitsfzolem  12265  0bits  12270  bitsinv1  12273  6gcd4e2  12316  3lcm2e6woprm  12408  6lcm4e12  12409  sqrt2irrlem  12483  oddpwdclemodd  12494  pythagtriplem1  12588  pythagtriplem12  12598  pythagtriplem14  12600  4sqlem11  12724  4sqlem12  12725  dec5dvds  12735  dec2nprm  12738  2exp5  12755  2exp6  12756  2exp7  12757  2exp8  12758  2exp11  12759  2exp16  12760  maxcncf  15087  mincncf  15088  coscn  15242  sinhalfpilem  15263  cospi  15272  ef2pi  15277  ef2kpi  15278  efper  15279  sinperlem  15280  sin2kpi  15283  cos2kpi  15284  sin2pim  15285  cos2pim  15286  ptolemy  15296  sincosq3sgn  15300  sincosq4sgn  15301  sinq12gt0  15302  cosq23lt0  15305  coseq00topi  15307  tangtx  15310  sincos4thpi  15312  sincos6thpi  15314  sincos3rdpi  15315  pigt3  15316  abssinper  15318  coskpi  15320  cosq34lt1  15322  logsqrt  15395  2logb9irrALT  15446  1sgm2ppw  15467  perfect1  15470  perfectlem1  15471  perfectlem2  15472  perfect  15473  lgsdir2lem2  15506  gausslemma2dlem6  15544  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2lem2  15559  m1lgs  15562  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2lgsoddprmlem2  15583  2lgsoddprmlem3c  15586  2lgsoddprmlem3d  15587  ex-fl  15661  ex-ceil  15662  ex-exp  15663  ex-fac  15664