Theorem 2cn 9328

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

Syntax hints:   ∈ wcel 2205  ℂcc 8141  2c2 9308

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227  df-2 9316

This theorem is referenced by:  2ex  9329  2cnd  9330  2m1e1  9375  3m1e2  9377  2p2e4  9384  times2  9386  2div2e1  9390  1p2e3  9392  3p3e6  9400  4p3e7  9402  5p3e8  9405  6p3e9  9408  2t1e2  9411  2t2e4  9412  3t3e9  9415  2t0e0  9417  4d2e2  9418  2cnne0  9467  1mhlfehlf  9476  8th4div3  9477  halfpm6th  9478  2mulicn  9480  2muliap0  9482  halfcl  9484  half0  9486  2halves  9487  halfaddsub  9492  div4p1lem1div2  9512  3halfnz  9696  zneo  9700  nneoor  9701  zeo  9704  7p3e10  9804  4t4e16  9828  6t3e18  9834  7t7e49  9843  8t5e40  9847  9t9e81  9858  decbin0  9869  decbin2  9870  halfthird  9872  fztpval  10442  fz0tp  10481  fz0to4untppr  10483  fzo0to3tp  10589  2tnp1ge0ge0  10688  fldiv4lem1div2  10694  expubnd  10985  sq2  11024  sq4e2t8  11026  cu2  11027  subsq2  11036  binom2sub  11042  binom3  11046  zesq  11048  fac2  11121  fac3  11122  faclbnd2  11132  bcn2  11154  4bc2eq6  11165  crre  11570  addcj  11604  imval2  11607  resqrexlemover  11723  resqrexlemcalc1  11727  resqrexlemnm  11731  resqrexlemcvg  11732  amgm2  11831  arisum  12212  arisum2  12213  geo2sum2  12229  geo2lim  12230  geoihalfsum  12236  efcllemp  12372  ege2le3  12385  tanval2ap  12427  tanval3ap  12428  efi4p  12431  efival  12446  sinadd  12450  cosadd  12451  sinmul  12458  cosmul  12459  cos2tsin  12465  ef01bndlem  12470  sin01bnd  12471  cos01bnd  12472  cos1bnd  12473  cos2bnd  12474  cos01gt0  12477  sin02gt0  12478  sin4lt0  12481  cos12dec  12482  egt2lt3  12494  odd2np1lem  12586  odd2np1  12587  ltoddhalfle  12607  halfleoddlt  12608  opoe  12609  omoe  12610  opeo  12611  omeo  12612  nno  12620  nn0o  12621  flodddiv4  12650  bits0  12662  bitsfzolem  12668  0bits  12673  bitsinv1  12676  6gcd4e2  12719  3lcm2e6woprm  12811  6lcm4e12  12812  sqrt2irrlem  12886  oddpwdclemodd  12897  pythagtriplem1  12991  pythagtriplem12  13001  pythagtriplem14  13003  4sqlem11  13127  4sqlem12  13128  dec5dvds  13138  dec2nprm  13141  2exp5  13158  2exp6  13159  2exp7  13160  2exp8  13161  2exp11  13162  2exp16  13163  ballotfilem2  13175  ballotfilemth  13228  maxcncf  15609  mincncf  15610  coscn  15764  sinhalfpilem  15785  cospi  15794  ef2pi  15799  ef2kpi  15800  efper  15801  sinperlem  15802  sin2kpi  15805  cos2kpi  15806  sin2pim  15807  cos2pim  15808  ptolemy  15818  sincosq3sgn  15822  sincosq4sgn  15823  sinq12gt0  15824  cosq23lt0  15827  coseq00topi  15829  tangtx  15832  sincos4thpi  15834  sincos6thpi  15836  sincos3rdpi  15837  pigt3  15838  abssinper  15840  coskpi  15842  cosq34lt1  15844  logsqrt  15917  2logb9irrALT  15968  1sgm2ppw  15992  perfect1  15995  perfectlem1  15996  perfectlem2  15997  perfect  15998  lgsdir2lem2  16031  gausslemma2dlem6  16069  lgsquadlem1  16079  lgsquadlem2  16080  lgsquad2lem2  16084  m1lgs  16087  2lgslem3a  16095  2lgslem3b  16096  2lgslem3c  16097  2lgslem3d  16098  2lgsoddprmlem2  16108  2lgsoddprmlem3c  16111  2lgsoddprmlem3d  16112  clwwlknonex2  16563  ex-fl  16622  ex-ceil  16623  ex-exp  16624  ex-fac  16625