Theorem 2cn 9177

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 9176	. 2 |- 2 e. RR
2	1	recni 8154	1 |- 2 e. CC

Syntax hints:   e. wcel 2200   CCcc 7993   2c2 9157

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 8087  ax-1re 8089  ax-addrcl 8092

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 9165

This theorem is referenced by:  2ex  9178  2cnd  9179  2m1e1  9224  3m1e2  9226  2p2e4  9233  times2  9235  2div2e1  9239  1p2e3  9241  3p3e6  9249  4p3e7  9251  5p3e8  9254  6p3e9  9257  2t1e2  9260  2t2e4  9261  3t3e9  9264  2t0e0  9266  4d2e2  9267  2cnne0  9316  1mhlfehlf  9325  8th4div3  9326  halfpm6th  9327  2mulicn  9329  2muliap0  9331  halfcl  9333  half0  9335  2halves  9336  halfaddsub  9341  div4p1lem1div2  9361  3halfnz  9540  zneo  9544  nneoor  9545  zeo  9548  7p3e10  9648  4t4e16  9672  6t3e18  9678  7t7e49  9687  8t5e40  9691  9t9e81  9702  decbin0  9713  decbin2  9714  halfthird  9716  fztpval  10275  fz0tp  10314  fz0to4untppr  10316  fzo0to3tp  10420  2tnp1ge0ge0  10516  fldiv4lem1div2  10522  expubnd  10813  sq2  10852  sq4e2t8  10854  cu2  10855  subsq2  10864  binom2sub  10870  binom3  10874  zesq  10875  fac2  10948  fac3  10949  faclbnd2  10959  bcn2  10981  4bc2eq6  10991  crre  11363  addcj  11397  imval2  11400  resqrexlemover  11516  resqrexlemcalc1  11520  resqrexlemnm  11524  resqrexlemcvg  11525  amgm2  11624  arisum  12004  arisum2  12005  geo2sum2  12021  geo2lim  12022  geoihalfsum  12028  efcllemp  12164  ege2le3  12177  tanval2ap  12219  tanval3ap  12220  efi4p  12223  efival  12238  sinadd  12242  cosadd  12243  sinmul  12250  cosmul  12251  cos2tsin  12257  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  cos1bnd  12265  cos2bnd  12266  cos01gt0  12269  sin02gt0  12270  sin4lt0  12273  cos12dec  12274  egt2lt3  12286  odd2np1lem  12378  odd2np1  12379  ltoddhalfle  12399  halfleoddlt  12400  opoe  12401  omoe  12402  opeo  12403  omeo  12404  nno  12412  nn0o  12413  flodddiv4  12442  bits0  12454  bitsfzolem  12460  0bits  12465  bitsinv1  12468  6gcd4e2  12511  3lcm2e6woprm  12603  6lcm4e12  12604  sqrt2irrlem  12678  oddpwdclemodd  12689  pythagtriplem1  12783  pythagtriplem12  12793  pythagtriplem14  12795  4sqlem11  12919  4sqlem12  12920  dec5dvds  12930  dec2nprm  12933  2exp5  12950  2exp6  12951  2exp7  12952  2exp8  12953  2exp11  12954  2exp16  12955  maxcncf  15283  mincncf  15284  coscn  15438  sinhalfpilem  15459  cospi  15468  ef2pi  15473  ef2kpi  15474  efper  15475  sinperlem  15476  sin2kpi  15479  cos2kpi  15480  sin2pim  15481  cos2pim  15482  ptolemy  15492  sincosq3sgn  15496  sincosq4sgn  15497  sinq12gt0  15498  cosq23lt0  15501  coseq00topi  15503  tangtx  15506  sincos4thpi  15508  sincos6thpi  15510  sincos3rdpi  15511  pigt3  15512  abssinper  15514  coskpi  15516  cosq34lt1  15518  logsqrt  15591  2logb9irrALT  15642  1sgm2ppw  15663  perfect1  15666  perfectlem1  15667  perfectlem2  15668  perfect  15669  lgsdir2lem2  15702  gausslemma2dlem6  15740  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2lem2  15755  m1lgs  15758  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2lgsoddprmlem2  15779  2lgsoddprmlem3c  15782  2lgsoddprmlem3d  15783  ex-fl  16047  ex-ceil  16048  ex-exp  16049  ex-fac  16050