Theorem 2cn 9181

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 9180	. 2 |- 2 e. RR
2	1	recni 8158	1 |- 2 e. CC

Syntax hints:   e. wcel 2200   CCcc 7997   2c2 9161

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 8091  ax-1re 8093  ax-addrcl 8096

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 9169

This theorem is referenced by:  2ex  9182  2cnd  9183  2m1e1  9228  3m1e2  9230  2p2e4  9237  times2  9239  2div2e1  9243  1p2e3  9245  3p3e6  9253  4p3e7  9255  5p3e8  9258  6p3e9  9261  2t1e2  9264  2t2e4  9265  3t3e9  9268  2t0e0  9270  4d2e2  9271  2cnne0  9320  1mhlfehlf  9329  8th4div3  9330  halfpm6th  9331  2mulicn  9333  2muliap0  9335  halfcl  9337  half0  9339  2halves  9340  halfaddsub  9345  div4p1lem1div2  9365  3halfnz  9544  zneo  9548  nneoor  9549  zeo  9552  7p3e10  9652  4t4e16  9676  6t3e18  9682  7t7e49  9691  8t5e40  9695  9t9e81  9706  decbin0  9717  decbin2  9718  halfthird  9720  fztpval  10279  fz0tp  10318  fz0to4untppr  10320  fzo0to3tp  10425  2tnp1ge0ge0  10521  fldiv4lem1div2  10527  expubnd  10818  sq2  10857  sq4e2t8  10859  cu2  10860  subsq2  10869  binom2sub  10875  binom3  10879  zesq  10880  fac2  10953  fac3  10954  faclbnd2  10964  bcn2  10986  4bc2eq6  10996  crre  11368  addcj  11402  imval2  11405  resqrexlemover  11521  resqrexlemcalc1  11525  resqrexlemnm  11529  resqrexlemcvg  11530  amgm2  11629  arisum  12009  arisum2  12010  geo2sum2  12026  geo2lim  12027  geoihalfsum  12033  efcllemp  12169  ege2le3  12182  tanval2ap  12224  tanval3ap  12225  efi4p  12228  efival  12243  sinadd  12247  cosadd  12248  sinmul  12255  cosmul  12256  cos2tsin  12262  ef01bndlem  12267  sin01bnd  12268  cos01bnd  12269  cos1bnd  12270  cos2bnd  12271  cos01gt0  12274  sin02gt0  12275  sin4lt0  12278  cos12dec  12279  egt2lt3  12291  odd2np1lem  12383  odd2np1  12384  ltoddhalfle  12404  halfleoddlt  12405  opoe  12406  omoe  12407  opeo  12408  omeo  12409  nno  12417  nn0o  12418  flodddiv4  12447  bits0  12459  bitsfzolem  12465  0bits  12470  bitsinv1  12473  6gcd4e2  12516  3lcm2e6woprm  12608  6lcm4e12  12609  sqrt2irrlem  12683  oddpwdclemodd  12694  pythagtriplem1  12788  pythagtriplem12  12798  pythagtriplem14  12800  4sqlem11  12924  4sqlem12  12925  dec5dvds  12935  dec2nprm  12938  2exp5  12955  2exp6  12956  2exp7  12957  2exp8  12958  2exp11  12959  2exp16  12960  maxcncf  15289  mincncf  15290  coscn  15444  sinhalfpilem  15465  cospi  15474  ef2pi  15479  ef2kpi  15480  efper  15481  sinperlem  15482  sin2kpi  15485  cos2kpi  15486  sin2pim  15487  cos2pim  15488  ptolemy  15498  sincosq3sgn  15502  sincosq4sgn  15503  sinq12gt0  15504  cosq23lt0  15507  coseq00topi  15509  tangtx  15512  sincos4thpi  15514  sincos6thpi  15516  sincos3rdpi  15517  pigt3  15518  abssinper  15520  coskpi  15522  cosq34lt1  15524  logsqrt  15597  2logb9irrALT  15648  1sgm2ppw  15669  perfect1  15672  perfectlem1  15673  perfectlem2  15674  perfect  15675  lgsdir2lem2  15708  gausslemma2dlem6  15746  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem2  15761  m1lgs  15764  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2lgsoddprmlem2  15785  2lgsoddprmlem3c  15788  2lgsoddprmlem3d  15789  ex-fl  16089  ex-ceil  16090  ex-exp  16091  ex-fac  16092