Theorem 2cn 9358

Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)

Assertion

Ref	Expression
2cn	⊢ 2 ∈ ℂ

Proof of Theorem 2cn

Step	Hyp	Ref	Expression
1		2re 9357	. 2 ⊢ 2 ∈ ℝ
2	1	recni 8332	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2209  ℂcc 8171  2c2 9338

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 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 8265  ax-1re 8267  ax-addrcl 8270

This theorem 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 9346

This theorem is referenced by:  2ex  9359  2cnd  9360  2m1e1  9405  3m1e2  9407  2p2e4  9414  times2  9416  2div2e1  9420  1p2e3  9422  3p3e6  9430  4p3e7  9432  5p3e8  9435  6p3e9  9438  2t1e2  9441  2t2e4  9442  3t3e9  9445  2t0e0  9447  4d2e2  9448  2cnne0  9497  1mhlfehlf  9506  8th4div3  9507  halfpm6th  9508  2mulicn  9510  2muliap0  9512  halfcl  9514  half0  9516  2halves  9517  halfaddsub  9522  div4p1lem1div2  9542  3halfnz  9726  zneo  9730  nneoor  9731  zeo  9734  7p3e10  9834  4t4e16  9858  6t3e18  9864  7t7e49  9873  8t5e40  9877  9t9e81  9888  decbin0  9899  decbin2  9900  halfthird  9902  fztpval  10473  fz0tp  10512  fz0to4untppr  10514  fzo0to3tp  10620  2tnp1ge0ge0  10719  fldiv4lem1div2  10725  expubnd  11016  sq2  11055  sq4e2t8  11057  cu2  11058  subsq2  11067  binom2sub  11073  binom3  11077  zesq  11079  fac2  11152  fac3  11153  faclbnd2  11163  bcn2  11185  4bc2eq6  11196  crre  11605  addcj  11639  imval2  11642  resqrexlemover  11759  resqrexlemcalc1  11763  resqrexlemnm  11767  resqrexlemcvg  11768  amgm2  11867  arisum  12248  arisum2  12249  geo2sum2  12265  geo2lim  12266  geoihalfsum  12272  efcllemp  12408  ege2le3  12421  tanval2ap  12463  tanval3ap  12464  efi4p  12467  efival  12482  sinadd  12486  cosadd  12487  sinmul  12494  cosmul  12495  cos2tsin  12501  ef01bndlem  12506  sin01bnd  12507  cos01bnd  12508  cos1bnd  12509  cos2bnd  12510  cos01gt0  12513  sin02gt0  12514  sin4lt0  12517  cos12dec  12518  egt2lt3  12530  odd2np1lem  12622  odd2np1  12623  ltoddhalfle  12643  halfleoddlt  12644  opoe  12645  omoe  12646  opeo  12647  omeo  12648  nno  12656  nn0o  12657  flodddiv4  12686  bits0  12698  bitsfzolem  12704  0bits  12709  bitsinv1  12712  6gcd4e2  12755  3lcm2e6woprm  12847  6lcm4e12  12848  sqrt2irrlem  12922  oddpwdclemodd  12933  pythagtriplem1  13027  pythagtriplem12  13037  pythagtriplem14  13039  4sqlem11  13163  4sqlem12  13164  dec5dvds  13174  dec2nprm  13177  2exp5  13194  2exp6  13195  2exp7  13196  2exp8  13197  2exp11  13198  2exp16  13199  ballotfilem2  13211  ballotfilemth  13264  maxcncf  15699  mincncf  15700  coscn  15854  sinhalfpilem  15875  cospi  15884  ef2pi  15889  ef2kpi  15890  efper  15891  sinperlem  15892  sin2kpi  15895  cos2kpi  15896  sin2pim  15897  cos2pim  15898  ptolemy  15908  sincosq3sgn  15912  sincosq4sgn  15913  sinq12gt0  15914  cosq23lt0  15917  coseq00topi  15919  tangtx  15922  sincos4thpi  15924  sincos6thpi  15926  sincos3rdpi  15927  pigt3  15928  abssinper  15930  coskpi  15932  cosq34lt1  15934  logsqrt  16008  2logb9irrALT  16059  log2tlbndlog2  16065  log2ublem2  16067  log2ublem3  16068  log2ublog2  16069  birthdaylog2  16073  1sgm2ppw  16092  perfect1  16095  perfectlem1  16096  perfectlem2  16097  perfect  16098  lgsdir2lem2  16131  gausslemma2dlem6  16169  lgsquadlem1  16179  lgsquadlem2  16180  lgsquad2lem2  16184  m1lgs  16187  2lgslem3a  16195  2lgslem3b  16196  2lgslem3c  16197  2lgslem3d  16198  2lgsoddprmlem2  16208  2lgsoddprmlem3c  16211  2lgsoddprmlem3d  16212  clwwlknonex2  16663  ex-fl  16722  ex-ceil  16723  ex-exp  16724  ex-fac  16725