Theorem 2cn 9204

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 9203	. 2 |- 2 e. RR
2	1	recni 8181	1 |- 2 e. CC

Syntax hints:   e. wcel 2200   CCcc 8020   2c2 9184

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 8114  ax-1re 8116  ax-addrcl 8119

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 3204  df-ss 3211  df-2 9192

This theorem is referenced by:  2ex  9205  2cnd  9206  2m1e1  9251  3m1e2  9253  2p2e4  9260  times2  9262  2div2e1  9266  1p2e3  9268  3p3e6  9276  4p3e7  9278  5p3e8  9281  6p3e9  9284  2t1e2  9287  2t2e4  9288  3t3e9  9291  2t0e0  9293  4d2e2  9294  2cnne0  9343  1mhlfehlf  9352  8th4div3  9353  halfpm6th  9354  2mulicn  9356  2muliap0  9358  halfcl  9360  half0  9362  2halves  9363  halfaddsub  9368  div4p1lem1div2  9388  3halfnz  9567  zneo  9571  nneoor  9572  zeo  9575  7p3e10  9675  4t4e16  9699  6t3e18  9705  7t7e49  9714  8t5e40  9718  9t9e81  9729  decbin0  9740  decbin2  9741  halfthird  9743  fztpval  10308  fz0tp  10347  fz0to4untppr  10349  fzo0to3tp  10454  2tnp1ge0ge0  10551  fldiv4lem1div2  10557  expubnd  10848  sq2  10887  sq4e2t8  10889  cu2  10890  subsq2  10899  binom2sub  10905  binom3  10909  zesq  10910  fac2  10983  fac3  10984  faclbnd2  10994  bcn2  11016  4bc2eq6  11026  crre  11408  addcj  11442  imval2  11445  resqrexlemover  11561  resqrexlemcalc1  11565  resqrexlemnm  11569  resqrexlemcvg  11570  amgm2  11669  arisum  12049  arisum2  12050  geo2sum2  12066  geo2lim  12067  geoihalfsum  12073  efcllemp  12209  ege2le3  12222  tanval2ap  12264  tanval3ap  12265  efi4p  12268  efival  12283  sinadd  12287  cosadd  12288  sinmul  12295  cosmul  12296  cos2tsin  12302  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  cos1bnd  12310  cos2bnd  12311  cos01gt0  12314  sin02gt0  12315  sin4lt0  12318  cos12dec  12319  egt2lt3  12331  odd2np1lem  12423  odd2np1  12424  ltoddhalfle  12444  halfleoddlt  12445  opoe  12446  omoe  12447  opeo  12448  omeo  12449  nno  12457  nn0o  12458  flodddiv4  12487  bits0  12499  bitsfzolem  12505  0bits  12510  bitsinv1  12513  6gcd4e2  12556  3lcm2e6woprm  12648  6lcm4e12  12649  sqrt2irrlem  12723  oddpwdclemodd  12734  pythagtriplem1  12828  pythagtriplem12  12838  pythagtriplem14  12840  4sqlem11  12964  4sqlem12  12965  dec5dvds  12975  dec2nprm  12978  2exp5  12995  2exp6  12996  2exp7  12997  2exp8  12998  2exp11  12999  2exp16  13000  maxcncf  15329  mincncf  15330  coscn  15484  sinhalfpilem  15505  cospi  15514  ef2pi  15519  ef2kpi  15520  efper  15521  sinperlem  15522  sin2kpi  15525  cos2kpi  15526  sin2pim  15527  cos2pim  15528  ptolemy  15538  sincosq3sgn  15542  sincosq4sgn  15543  sinq12gt0  15544  cosq23lt0  15547  coseq00topi  15549  tangtx  15552  sincos4thpi  15554  sincos6thpi  15556  sincos3rdpi  15557  pigt3  15558  abssinper  15560  coskpi  15562  cosq34lt1  15564  logsqrt  15637  2logb9irrALT  15688  1sgm2ppw  15709  perfect1  15712  perfectlem1  15713  perfectlem2  15714  perfect  15715  lgsdir2lem2  15748  gausslemma2dlem6  15786  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem2  15801  m1lgs  15804  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2lgsoddprmlem2  15825  2lgsoddprmlem3c  15828  2lgsoddprmlem3d  15829  clwwlknonex2  16234  ex-fl  16257  ex-ceil  16258  ex-exp  16259  ex-fac  16260