Theorem 2cn 9219

Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)

Assertion

Ref	Expression
2cn	⊢ 2 ∈ ℂ

Proof of Theorem 2cn

Step	Hyp	Ref	Expression
1		2re 9218	. 2 ⊢ 2 ∈ ℝ
2	1	recni 8196	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2201  ℂcc 8035  2c2 9199

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 2212  ax-resscn 8129  ax-1re 8131  ax-addrcl 8134

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-in 3205  df-ss 3212  df-2 9207

This theorem is referenced by:  2ex  9220  2cnd  9221  2m1e1  9266  3m1e2  9268  2p2e4  9275  times2  9277  2div2e1  9281  1p2e3  9283  3p3e6  9291  4p3e7  9293  5p3e8  9296  6p3e9  9299  2t1e2  9302  2t2e4  9303  3t3e9  9306  2t0e0  9308  4d2e2  9309  2cnne0  9358  1mhlfehlf  9367  8th4div3  9368  halfpm6th  9369  2mulicn  9371  2muliap0  9373  halfcl  9375  half0  9377  2halves  9378  halfaddsub  9383  div4p1lem1div2  9403  3halfnz  9582  zneo  9586  nneoor  9587  zeo  9590  7p3e10  9690  4t4e16  9714  6t3e18  9720  7t7e49  9729  8t5e40  9733  9t9e81  9744  decbin0  9755  decbin2  9756  halfthird  9758  fztpval  10323  fz0tp  10362  fz0to4untppr  10364  fzo0to3tp  10470  2tnp1ge0ge0  10567  fldiv4lem1div2  10573  expubnd  10864  sq2  10903  sq4e2t8  10905  cu2  10906  subsq2  10915  binom2sub  10921  binom3  10925  zesq  10926  fac2  10999  fac3  11000  faclbnd2  11010  bcn2  11032  4bc2eq6  11042  crre  11440  addcj  11474  imval2  11477  resqrexlemover  11593  resqrexlemcalc1  11597  resqrexlemnm  11601  resqrexlemcvg  11602  amgm2  11701  arisum  12082  arisum2  12083  geo2sum2  12099  geo2lim  12100  geoihalfsum  12106  efcllemp  12242  ege2le3  12255  tanval2ap  12297  tanval3ap  12298  efi4p  12301  efival  12316  sinadd  12320  cosadd  12321  sinmul  12328  cosmul  12329  cos2tsin  12335  ef01bndlem  12340  sin01bnd  12341  cos01bnd  12342  cos1bnd  12343  cos2bnd  12344  cos01gt0  12347  sin02gt0  12348  sin4lt0  12351  cos12dec  12352  egt2lt3  12364  odd2np1lem  12456  odd2np1  12457  ltoddhalfle  12477  halfleoddlt  12478  opoe  12479  omoe  12480  opeo  12481  omeo  12482  nno  12490  nn0o  12491  flodddiv4  12520  bits0  12532  bitsfzolem  12538  0bits  12543  bitsinv1  12546  6gcd4e2  12589  3lcm2e6woprm  12681  6lcm4e12  12682  sqrt2irrlem  12756  oddpwdclemodd  12767  pythagtriplem1  12861  pythagtriplem12  12871  pythagtriplem14  12873  4sqlem11  12997  4sqlem12  12998  dec5dvds  13008  dec2nprm  13011  2exp5  13028  2exp6  13029  2exp7  13030  2exp8  13031  2exp11  13032  2exp16  13033  maxcncf  15368  mincncf  15369  coscn  15523  sinhalfpilem  15544  cospi  15553  ef2pi  15558  ef2kpi  15559  efper  15560  sinperlem  15561  sin2kpi  15564  cos2kpi  15565  sin2pim  15566  cos2pim  15567  ptolemy  15577  sincosq3sgn  15581  sincosq4sgn  15582  sinq12gt0  15583  cosq23lt0  15586  coseq00topi  15588  tangtx  15591  sincos4thpi  15593  sincos6thpi  15595  sincos3rdpi  15596  pigt3  15597  abssinper  15599  coskpi  15601  cosq34lt1  15603  logsqrt  15676  2logb9irrALT  15727  1sgm2ppw  15748  perfect1  15751  perfectlem1  15752  perfectlem2  15753  perfect  15754  lgsdir2lem2  15787  gausslemma2dlem6  15825  lgsquadlem1  15835  lgsquadlem2  15836  lgsquad2lem2  15840  m1lgs  15843  2lgslem3a  15851  2lgslem3b  15852  2lgslem3c  15853  2lgslem3d  15854  2lgsoddprmlem2  15864  2lgsoddprmlem3c  15867  2lgsoddprmlem3d  15868  clwwlknonex2  16319  ex-fl  16378  ex-ceil  16379  ex-exp  16380  ex-fac  16381