Theorem 2cn 9376

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 9375	. 2 ⊢ 2 ∈ ℝ
2	1	recni 8338	1 ⊢ 2 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2209  ℂcc 8177  2c2 9356

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 9364

This theorem is used by:  2ex  9377  2cnd  9378  2m1e1  9423  3m1e2  9425  2p2e4  9432  times2  9434  2div2e1  9438  1p2e3  9440  3p3e6  9448  4p3e7  9450  5p3e8  9453  6p3e9  9456  2t1e2  9459  2t2e4  9460  2t3e6  9463  3t3e9  9464  2t0e0  9466  4d2e2  9467  2cnne0  9516  1mhlfehlf  9525  8th4div3  9526  halfpm6th  9527  2mulicn  9529  2muliap0  9531  halfcl  9533  half0  9535  2halves  9536  halfaddsub  9541  div4p1lem1div2  9561  3halfnz  9745  zneo  9749  nneoor  9750  zeo  9753  7p3e10  9853  4t4e16  9877  6t3e18  9883  7t7e49  9892  8t5e40  9896  9t9e81  9907  decbin0  9918  decbin2  9919  halfthird  9921  fztpval  10492  fz0tp  10531  fz0to4untppr  10533  fzo0to3tp  10639  2tnp1ge0ge0  10738  fldiv4lem1div2  10744  expubnd  11035  sq2  11074  sq4e2t8  11076  cu2  11077  subsq2  11086  binom2sub  11092  binom3  11096  zesq  11098  fac2  11171  fac3  11172  faclbnd2  11182  bcn2  11204  4bc2eq6  11215  crre  11624  addcj  11658  imval2  11661  resqrexlemover  11778  resqrexlemcalc1  11782  resqrexlemnm  11786  resqrexlemcvg  11787  amgm2  11886  arisum  12267  arisum2  12268  geo2sum2  12284  geo2lim  12285  geoihalfsum  12291  efcllemp  12427  ege2le3  12440  tanval2ap  12482  tanval3ap  12483  efi4p  12486  efival  12501  sinadd  12505  cosadd  12506  sinmul  12513  cosmul  12514  cos2tsin  12520  ef01bndlem  12525  sin01bnd  12526  cos01bnd  12527  cos1bnd  12528  cos2bnd  12529  cos01gt0  12532  sin02gt0  12533  sin4lt0  12536  cos12dec  12537  egt2lt3  12549  odd2np1lem  12641  odd2np1  12642  ltoddhalfle  12662  halfleoddlt  12663  opoe  12664  omoe  12665  opeo  12666  omeo  12667  nno  12675  nn0o  12676  flodddiv4  12705  bits0  12717  bitsfzolem  12723  0bits  12728  bitsinv1  12731  6gcd4e2  12774  3lcm2e6woprm  12866  6lcm4e12  12867  sqrt2irrlem  12941  oddpwdclemodd  12952  pythagtriplem1  13046  pythagtriplem12  13056  pythagtriplem14  13058  4sqlem11  13182  4sqlem12  13183  dec5dvds  13193  dec2nprm  13196  2exp5  13213  2exp6  13214  2exp7  13215  2exp8  13216  2exp11  13217  2exp16  13218  ballotfilem2  13230  ballotfilemth  13283  maxcncf  15718  mincncf  15719  coscn  15873  sinhalfpilem  15895  cospi  15904  ef2pi  15909  ef2kpi  15910  efper  15911  sinperlem  15912  sin2kpi  15915  cos2kpi  15916  sin2pim  15917  cos2pim  15918  ptolemy  15928  sincosq3sgn  15932  sincosq4sgn  15933  sinq12gt0  15934  cosq23lt0  15937  coseq00topi  15939  tangtx  15942  sincos4thpi  15944  sincos6thpi  15946  sincos3rdpi  15947  pigt3  15948  abssinper  15950  coskpi  15952  cosq34lt1  15954  logsqrt  16031  2logb9irrALT  16082  log2tlbndlog2  16088  log2ublem2  16090  log2ublem3  16091  log2ublog2  16092  birthdaylog2  16096  1sgm2ppw  16115  perfect1  16118  perfectlem1  16119  perfectlem2  16120  perfect  16121  bcmax  16125  bcp1ctr  16126  bclbnd  16127  lgsdir2lem2  16160  gausslemma2dlem6  16198  lgsquadlem1  16208  lgsquadlem2  16209  lgsquad2lem2  16213  m1lgs  16216  2lgslem3a  16224  2lgslem3b  16225  2lgslem3c  16226  2lgslem3d  16227  2lgsoddprmlem2  16237  2lgsoddprmlem3c  16240  2lgsoddprmlem3d  16241  clwwlknonex2  16692  ex-fl  16751  ex-ceil  16752  ex-exp  16753  ex-fac  16754