Theorem 2cn 9384

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 9383	. 2 |- 2 e. RR
2	1	recni 8344	1 |- 2 e. CC

This proof depends on syntax axioms:   e. wcel 2209   CCcc 8183   2c2 9364

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 8277  ax-1re 8279  ax-addrcl 8282

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 9372

This theorem is used by:  2ex  9385  2cnd  9386  2m1e1  9431  3m1e2  9433  2p2e4  9440  times2  9442  2div2e1  9446  1p2e3  9448  3p3e6  9456  4p3e7  9458  5p3e8  9461  6p3e9  9464  2t1e2  9467  2t2e4  9468  2t3e6  9471  3t3e9  9472  2t4e8  9474  2t0e0  9475  4d2e2  9476  2cnne0  9525  1mhlfehlf  9534  8th4div3  9535  halfpm6th  9536  2mulicn  9538  2muliap0  9540  halfcl  9542  half0  9544  2halves  9545  halfaddsub  9550  div4p1lem1div2  9570  3halfnz  9754  zneo  9758  nneoor  9759  zeo  9762  7p3e10  9867  4t4e16  9891  6t3e18  9897  7t7e49  9906  8t5e40  9910  9t9e81  9921  decbin0  9932  decbin2  9933  halfthird  9935  fztpval  10507  fz0tp  10546  fz0to4untppr  10548  fzo0to3tp  10654  2tnp1ge0ge0  10757  fldiv4lem1div2  10763  expubnd  11054  sq2  11093  sq4e2t8  11095  cu2  11096  subsq2  11105  binom2sub  11111  binom3  11115  zesq  11117  fac2  11191  fac3  11192  faclbnd2  11202  bcn2  11224  4bc2eq6  11235  crre  11644  addcj  11678  imval2  11681  resqrexlemover  11798  resqrexlemcalc1  11802  resqrexlemnm  11806  resqrexlemcvg  11807  amgm2  11907  arisum  12290  arisum2  12291  geo2sum2  12307  geo2lim  12308  geoihalfsum  12314  efcllemp  12450  ege2le3  12463  tanval2ap  12505  tanval3ap  12506  efi4p  12509  efival  12524  sinadd  12528  cosadd  12529  sinmul  12536  cosmul  12537  cos2tsin  12543  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  cos1bnd  12551  cos2bnd  12552  cos01gt0  12555  sin02gt0  12556  sin4lt0  12559  cos12dec  12560  egt2lt3  12572  odd2np1lem  12664  odd2np1  12665  ltoddhalfle  12685  halfleoddlt  12686  opoe  12687  omoe  12688  opeo  12689  omeo  12690  nno  12698  nn0o  12699  flodddiv4  12728  bits0  12740  bitsfzolem  12746  0bits  12751  bitsinv1  12754  6gcd4e2  12797  3lcm2e6woprm  12889  6lcm4e12  12890  sqrt2irrlem  12965  pythagtriplem1  13073  pythagtriplem12  13083  pythagtriplem14  13085  4sqlem11  13209  4sqlem12  13210  dec5dvds  13220  dec2nprm  13223  2exp5  13241  2exp6  13242  2exp7  13243  2exp8  13244  2exp11  13245  2exp16  13246  10nprm  13257  11prm  13258  13prm  13259  37prm  13264  43prm  13265  83prm  13266  139prm  13267  163prm  13268  317prm  13269  631prm  13270  1259lem1  13271  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  1259prm  13276  ballotfilem2  13286  ballotfilemth  13339  maxcncf  15841  mincncf  15842  coscn  15996  sinhalfpilem  16018  cospi  16027  ef2pi  16032  ef2kpi  16033  efper  16034  sinperlem  16035  sin2kpi  16038  cos2kpi  16039  sin2pim  16040  cos2pim  16041  ptolemy  16051  sincosq3sgn  16055  sincosq4sgn  16056  sinq12gt0  16057  cosq23lt0  16060  coseq00topi  16062  tangtx  16065  sincos4thpi  16067  sincos6thpi  16069  sincos3rdpi  16070  pigt3  16071  abssinper  16073  coskpi  16075  sineq0re  16076  cosq34lt1  16078  root1idef  16084  logsqrt  16158  efnthr  16176  2logb9irrALT  16210  log2tlbndlog2  16220  log2ublem2  16222  log2ublem3  16223  log2ublog2  16224  birthdaylog2  16228  1sgm2ppw  16289  ppiqub  16293  chtublem  16295  chtqub  16296  perfect1  16298  perfectlem1  16299  perfectlem2  16300  perfect  16301  bcmax  16305  bcp1ctr  16306  bclbnd  16307  bpos1lem  16309  bpos1  16310  bposlem1  16311  bposlem2  16312  bposlem4  16314  bposlem5  16315  bposlem6  16316  bposlem8  16318  bposlem9  16319  lgsdir2lem2  16353  gausslemma2dlem6  16391  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem2  16406  m1lgs  16409  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2lgsoddprmlem2  16430  2lgsoddprmlem3c  16433  2lgsoddprmlem3d  16434  clwwlknonex2  16885  ex-fl  16944  ex-ceil  16945  ex-exp  16946  ex-fac  16947