Theorem 2cn 8990

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 8989	. 2 |- 2 e. RR
2	1	recni 7969	1 |- 2 e. CC

Syntax hints:   e. wcel 2148   CCcc 7809   2c2 8970

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 7903  ax-1re 7905  ax-addrcl 7908

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 3136  df-ss 3143  df-2 8978

This theorem is referenced by:  2ex  8991  2cnd  8992  2m1e1  9037  3m1e2  9039  2p2e4  9046  times2  9048  2div2e1  9051  1p2e3  9053  3p3e6  9061  4p3e7  9063  5p3e8  9066  6p3e9  9069  2t1e2  9072  2t2e4  9073  3t3e9  9076  2t0e0  9078  4d2e2  9079  2cnne0  9128  1mhlfehlf  9137  8th4div3  9138  halfpm6th  9139  2mulicn  9141  2muliap0  9143  halfcl  9145  half0  9147  2halves  9148  halfaddsub  9153  div4p1lem1div2  9172  3halfnz  9350  zneo  9354  nneoor  9355  zeo  9358  7p3e10  9458  4t4e16  9482  6t3e18  9488  7t7e49  9497  8t5e40  9501  9t9e81  9512  decbin0  9523  decbin2  9524  halfthird  9526  fztpval  10083  fz0tp  10122  fz0to4untppr  10124  fzo0to3tp  10219  2tnp1ge0ge0  10301  expubnd  10577  sq2  10616  sq4e2t8  10618  cu2  10619  subsq2  10628  binom2sub  10634  binom3  10638  zesq  10639  fac2  10711  fac3  10712  faclbnd2  10722  bcn2  10744  4bc2eq6  10754  crre  10866  addcj  10900  imval2  10903  resqrexlemover  11019  resqrexlemcalc1  11023  resqrexlemnm  11027  resqrexlemcvg  11028  amgm2  11127  arisum  11506  arisum2  11507  geo2sum2  11523  geo2lim  11524  geoihalfsum  11530  efcllemp  11666  ege2le3  11679  tanval2ap  11721  tanval3ap  11722  efi4p  11725  efival  11740  sinadd  11744  cosadd  11745  sinmul  11752  cosmul  11753  cos2tsin  11759  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  cos1bnd  11767  cos2bnd  11768  cos01gt0  11770  sin02gt0  11771  sin4lt0  11774  cos12dec  11775  egt2lt3  11787  odd2np1lem  11877  odd2np1  11878  ltoddhalfle  11898  halfleoddlt  11899  opoe  11900  omoe  11901  opeo  11902  omeo  11903  nno  11911  nn0o  11912  flodddiv4  11939  6gcd4e2  11996  3lcm2e6woprm  12086  6lcm4e12  12087  sqrt2irrlem  12161  oddpwdclemodd  12172  pythagtriplem1  12265  pythagtriplem12  12275  pythagtriplem14  12277  coscn  14194  sinhalfpilem  14215  cospi  14224  ef2pi  14229  ef2kpi  14230  efper  14231  sinperlem  14232  sin2kpi  14235  cos2kpi  14236  sin2pim  14237  cos2pim  14238  ptolemy  14248  sincosq3sgn  14252  sincosq4sgn  14253  sinq12gt0  14254  cosq23lt0  14257  coseq00topi  14259  tangtx  14262  sincos4thpi  14264  sincos6thpi  14266  sincos3rdpi  14267  pigt3  14268  abssinper  14270  coskpi  14272  cosq34lt1  14274  logsqrt  14346  2logb9irrALT  14395  lgsdir2lem2  14433  m1lgs  14455  2lgsoddprmlem2  14457  2lgsoddprmlem3c  14460  2lgsoddprmlem3d  14461  ex-fl  14480  ex-ceil  14481  ex-exp  14482  ex-fac  14483