Theorem 2cn 9053

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 9052	. 2 |- 2 e. RR
2	1	recni 8031	1 |- 2 e. CC

Syntax hints:   e. wcel 2164   CCcc 7870   2c2 9033

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166  df-2 9041

This theorem is referenced by:  2ex  9054  2cnd  9055  2m1e1  9100  3m1e2  9102  2p2e4  9109  times2  9111  2div2e1  9114  1p2e3  9116  3p3e6  9124  4p3e7  9126  5p3e8  9129  6p3e9  9132  2t1e2  9135  2t2e4  9136  3t3e9  9139  2t0e0  9141  4d2e2  9142  2cnne0  9191  1mhlfehlf  9200  8th4div3  9201  halfpm6th  9202  2mulicn  9204  2muliap0  9206  halfcl  9208  half0  9210  2halves  9211  halfaddsub  9216  div4p1lem1div2  9236  3halfnz  9414  zneo  9418  nneoor  9419  zeo  9422  7p3e10  9522  4t4e16  9546  6t3e18  9552  7t7e49  9561  8t5e40  9565  9t9e81  9576  decbin0  9587  decbin2  9588  halfthird  9590  fztpval  10149  fz0tp  10188  fz0to4untppr  10190  fzo0to3tp  10286  2tnp1ge0ge0  10370  fldiv4lem1div2  10376  expubnd  10667  sq2  10706  sq4e2t8  10708  cu2  10709  subsq2  10718  binom2sub  10724  binom3  10728  zesq  10729  fac2  10802  fac3  10803  faclbnd2  10813  bcn2  10835  4bc2eq6  10845  crre  11001  addcj  11035  imval2  11038  resqrexlemover  11154  resqrexlemcalc1  11158  resqrexlemnm  11162  resqrexlemcvg  11163  amgm2  11262  arisum  11641  arisum2  11642  geo2sum2  11658  geo2lim  11659  geoihalfsum  11665  efcllemp  11801  ege2le3  11814  tanval2ap  11856  tanval3ap  11857  efi4p  11860  efival  11875  sinadd  11879  cosadd  11880  sinmul  11887  cosmul  11888  cos2tsin  11894  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  cos1bnd  11902  cos2bnd  11903  cos01gt0  11906  sin02gt0  11907  sin4lt0  11910  cos12dec  11911  egt2lt3  11923  odd2np1lem  12013  odd2np1  12014  ltoddhalfle  12034  halfleoddlt  12035  opoe  12036  omoe  12037  opeo  12038  omeo  12039  nno  12047  nn0o  12048  flodddiv4  12075  6gcd4e2  12132  3lcm2e6woprm  12224  6lcm4e12  12225  sqrt2irrlem  12299  oddpwdclemodd  12310  pythagtriplem1  12403  pythagtriplem12  12413  pythagtriplem14  12415  4sqlem11  12539  4sqlem12  12540  maxcncf  14769  mincncf  14770  coscn  14905  sinhalfpilem  14926  cospi  14935  ef2pi  14940  ef2kpi  14941  efper  14942  sinperlem  14943  sin2kpi  14946  cos2kpi  14947  sin2pim  14948  cos2pim  14949  ptolemy  14959  sincosq3sgn  14963  sincosq4sgn  14964  sinq12gt0  14965  cosq23lt0  14968  coseq00topi  14970  tangtx  14973  sincos4thpi  14975  sincos6thpi  14977  sincos3rdpi  14978  pigt3  14979  abssinper  14981  coskpi  14983  cosq34lt1  14985  logsqrt  15057  2logb9irrALT  15106  lgsdir2lem2  15145  gausslemma2dlem6  15183  lgsquadlem1  15191  m1lgs  15192  2lgsoddprmlem2  15194  2lgsoddprmlem3c  15197  2lgsoddprmlem3d  15198  ex-fl  15217  ex-ceil  15218  ex-exp  15219  ex-fac  15220