Theorem 2cn 9377

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 9376	. 2 |- 2 e. RR
2	1	recni 8338	1 |- 2 e. CC

This proof depends on syntax axioms:   e. wcel 2209   CCcc 8177   2c2 9357

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-2 9365

This theorem is used by:  2ex  9378  2cnd  9379  2m1e1  9424  3m1e2  9426  2p2e4  9433  times2  9435  2div2e1  9439  1p2e3  9441  3p3e6  9449  4p3e7  9451  5p3e8  9454  6p3e9  9457  2t1e2  9460  2t2e4  9461  2t3e6  9464  3t3e9  9465  2t4e8  9467  2t0e0  9468  4d2e2  9469  2cnne0  9518  1mhlfehlf  9527  8th4div3  9528  halfpm6th  9529  2mulicn  9531  2muliap0  9533  halfcl  9535  half0  9537  2halves  9538  halfaddsub  9543  div4p1lem1div2  9563  3halfnz  9747  zneo  9751  nneoor  9752  zeo  9755  7p3e10  9860  4t4e16  9884  6t3e18  9890  7t7e49  9899  8t5e40  9903  9t9e81  9914  decbin0  9925  decbin2  9926  halfthird  9928  fztpval  10500  fz0tp  10539  fz0to4untppr  10541  fzo0to3tp  10647  2tnp1ge0ge0  10749  fldiv4lem1div2  10755  expubnd  11046  sq2  11085  sq4e2t8  11087  cu2  11088  subsq2  11097  binom2sub  11103  binom3  11107  zesq  11109  fac2  11183  fac3  11184  faclbnd2  11194  bcn2  11216  4bc2eq6  11227  crre  11636  addcj  11670  imval2  11673  resqrexlemover  11790  resqrexlemcalc1  11794  resqrexlemnm  11798  resqrexlemcvg  11799  amgm2  11899  arisum  12281  arisum2  12282  geo2sum2  12298  geo2lim  12299  geoihalfsum  12305  efcllemp  12441  ege2le3  12454  tanval2ap  12496  tanval3ap  12497  efi4p  12500  efival  12515  sinadd  12519  cosadd  12520  sinmul  12527  cosmul  12528  cos2tsin  12534  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  cos1bnd  12542  cos2bnd  12543  cos01gt0  12546  sin02gt0  12547  sin4lt0  12550  cos12dec  12551  egt2lt3  12563  odd2np1lem  12655  odd2np1  12656  ltoddhalfle  12676  halfleoddlt  12677  opoe  12678  omoe  12679  opeo  12680  omeo  12681  nno  12689  nn0o  12690  flodddiv4  12719  bits0  12731  bitsfzolem  12737  0bits  12742  bitsinv1  12745  6gcd4e2  12788  3lcm2e6woprm  12880  6lcm4e12  12881  sqrt2irrlem  12956  pythagtriplem1  13064  pythagtriplem12  13074  pythagtriplem14  13076  4sqlem11  13200  4sqlem12  13201  dec5dvds  13211  dec2nprm  13214  2exp5  13232  2exp6  13233  2exp7  13234  2exp8  13235  2exp11  13236  2exp16  13237  10nprm  13248  11prm  13249  13prm  13250  37prm  13255  43prm  13256  83prm  13257  139prm  13258  163prm  13259  317prm  13260  631prm  13261  1259lem1  13262  1259lem2  13263  1259lem3  13264  1259lem4  13265  1259lem5  13266  1259prm  13267  ballotfilem2  13277  ballotfilemth  13330  maxcncf  15765  mincncf  15766  coscn  15920  sinhalfpilem  15942  cospi  15951  ef2pi  15956  ef2kpi  15957  efper  15958  sinperlem  15959  sin2kpi  15962  cos2kpi  15963  sin2pim  15964  cos2pim  15965  ptolemy  15975  sincosq3sgn  15979  sincosq4sgn  15980  sinq12gt0  15981  cosq23lt0  15984  coseq00topi  15986  tangtx  15989  sincos4thpi  15991  sincos6thpi  15993  sincos3rdpi  15994  pigt3  15995  abssinper  15997  coskpi  15999  cosq34lt1  16001  logsqrt  16078  2logb9irrALT  16129  log2tlbndlog2  16139  log2ublem2  16141  log2ublem3  16142  log2ublog2  16143  birthdaylog2  16147  1sgm2ppw  16190  ppiqub  16194  perfect1  16196  perfectlem1  16197  perfectlem2  16198  perfect  16199  bcmax  16203  bcp1ctr  16204  bclbnd  16205  bpos1lem  16207  bpos1  16208  bposlem1  16209  bposlem2  16210  bposlem4  16212  bposlem5  16213  lgsdir2lem2  16246  gausslemma2dlem6  16284  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem2  16299  m1lgs  16302  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2lgsoddprmlem2  16323  2lgsoddprmlem3c  16326  2lgsoddprmlem3d  16327  clwwlknonex2  16778  ex-fl  16837  ex-ceil  16838  ex-exp  16839  ex-fac  16840