Theorem 2cn 8988

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 8987	. 2 |- 2 e. RR
2	1	recni 7968	1 |- 2 e. CC

Syntax hints:   e. wcel 2148   CCcc 7808   2c2 8968

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7902  ax-1re 7904  ax-addrcl 7907

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142  df-2 8976

This theorem is referenced by:  2ex  8989  2cnd  8990  2m1e1  9035  3m1e2  9037  2p2e4  9044  times2  9046  2div2e1  9049  1p2e3  9051  3p3e6  9059  4p3e7  9061  5p3e8  9064  6p3e9  9067  2t1e2  9070  2t2e4  9071  3t3e9  9074  2t0e0  9076  4d2e2  9077  2cnne0  9126  1mhlfehlf  9135  8th4div3  9136  halfpm6th  9137  2mulicn  9139  2muliap0  9141  halfcl  9143  half0  9145  2halves  9146  halfaddsub  9151  div4p1lem1div2  9170  3halfnz  9348  zneo  9352  nneoor  9353  zeo  9356  7p3e10  9456  4t4e16  9480  6t3e18  9486  7t7e49  9495  8t5e40  9499  9t9e81  9510  decbin0  9521  decbin2  9522  halfthird  9524  fztpval  10080  fz0tp  10119  fz0to4untppr  10121  fzo0to3tp  10216  2tnp1ge0ge0  10298  expubnd  10574  sq2  10612  sq4e2t8  10614  cu2  10615  subsq2  10624  binom2sub  10630  binom3  10634  zesq  10635  fac2  10706  fac3  10707  faclbnd2  10717  bcn2  10739  4bc2eq6  10749  crre  10861  addcj  10895  imval2  10898  resqrexlemover  11014  resqrexlemcalc1  11018  resqrexlemnm  11022  resqrexlemcvg  11023  amgm2  11122  arisum  11501  arisum2  11502  geo2sum2  11518  geo2lim  11519  geoihalfsum  11525  efcllemp  11661  ege2le3  11674  tanval2ap  11716  tanval3ap  11717  efi4p  11720  efival  11735  sinadd  11739  cosadd  11740  sinmul  11747  cosmul  11748  cos2tsin  11754  ef01bndlem  11759  sin01bnd  11760  cos01bnd  11761  cos1bnd  11762  cos2bnd  11763  cos01gt0  11765  sin02gt0  11766  sin4lt0  11769  cos12dec  11770  egt2lt3  11782  odd2np1lem  11871  odd2np1  11872  ltoddhalfle  11892  halfleoddlt  11893  opoe  11894  omoe  11895  opeo  11896  omeo  11897  nno  11905  nn0o  11906  flodddiv4  11933  6gcd4e2  11990  3lcm2e6woprm  12080  6lcm4e12  12081  sqrt2irrlem  12155  oddpwdclemodd  12166  pythagtriplem1  12259  pythagtriplem12  12269  pythagtriplem14  12271  coscn  14084  sinhalfpilem  14105  cospi  14114  ef2pi  14119  ef2kpi  14120  efper  14121  sinperlem  14122  sin2kpi  14125  cos2kpi  14126  sin2pim  14127  cos2pim  14128  ptolemy  14138  sincosq3sgn  14142  sincosq4sgn  14143  sinq12gt0  14144  cosq23lt0  14147  coseq00topi  14149  tangtx  14152  sincos4thpi  14154  sincos6thpi  14156  sincos3rdpi  14157  pigt3  14158  abssinper  14160  coskpi  14162  cosq34lt1  14164  logsqrt  14236  2logb9irrALT  14285  lgsdir2lem2  14323  ex-fl  14359  ex-ceil  14360  ex-exp  14361  ex-fac  14362