Theorem 2cn 9313

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

Syntax hints:   ∈ wcel 2205  ℂcc 8130  2c2 9293

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 8224  ax-1re 8226  ax-addrcl 8229

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 3219  df-ss 3226  df-2 9301

This theorem is referenced by:  2ex  9314  2cnd  9315  2m1e1  9360  3m1e2  9362  2p2e4  9369  times2  9371  2div2e1  9375  1p2e3  9377  3p3e6  9385  4p3e7  9387  5p3e8  9390  6p3e9  9393  2t1e2  9396  2t2e4  9397  3t3e9  9400  2t0e0  9402  4d2e2  9403  2cnne0  9452  1mhlfehlf  9461  8th4div3  9462  halfpm6th  9463  2mulicn  9465  2muliap0  9467  halfcl  9469  half0  9471  2halves  9472  halfaddsub  9477  div4p1lem1div2  9497  3halfnz  9681  zneo  9685  nneoor  9686  zeo  9689  7p3e10  9789  4t4e16  9813  6t3e18  9819  7t7e49  9828  8t5e40  9832  9t9e81  9843  decbin0  9854  decbin2  9855  halfthird  9857  fztpval  10424  fz0tp  10463  fz0to4untppr  10465  fzo0to3tp  10571  2tnp1ge0ge0  10668  fldiv4lem1div2  10674  expubnd  10965  sq2  11004  sq4e2t8  11006  cu2  11007  subsq2  11016  binom2sub  11022  binom3  11026  zesq  11028  fac2  11101  fac3  11102  faclbnd2  11112  bcn2  11134  4bc2eq6  11145  crre  11550  addcj  11584  imval2  11587  resqrexlemover  11703  resqrexlemcalc1  11707  resqrexlemnm  11711  resqrexlemcvg  11712  amgm2  11811  arisum  12192  arisum2  12193  geo2sum2  12209  geo2lim  12210  geoihalfsum  12216  efcllemp  12352  ege2le3  12365  tanval2ap  12407  tanval3ap  12408  efi4p  12411  efival  12426  sinadd  12430  cosadd  12431  sinmul  12438  cosmul  12439  cos2tsin  12445  ef01bndlem  12450  sin01bnd  12451  cos01bnd  12452  cos1bnd  12453  cos2bnd  12454  cos01gt0  12457  sin02gt0  12458  sin4lt0  12461  cos12dec  12462  egt2lt3  12474  odd2np1lem  12566  odd2np1  12567  ltoddhalfle  12587  halfleoddlt  12588  opoe  12589  omoe  12590  opeo  12591  omeo  12592  nno  12600  nn0o  12601  flodddiv4  12630  bits0  12642  bitsfzolem  12648  0bits  12653  bitsinv1  12656  6gcd4e2  12699  3lcm2e6woprm  12791  6lcm4e12  12792  sqrt2irrlem  12866  oddpwdclemodd  12877  pythagtriplem1  12971  pythagtriplem12  12981  pythagtriplem14  12983  4sqlem11  13107  4sqlem12  13108  dec5dvds  13118  dec2nprm  13121  2exp5  13138  2exp6  13139  2exp7  13140  2exp8  13141  2exp11  13142  2exp16  13143  ballotfilem2  13153  maxcncf  15529  mincncf  15530  coscn  15684  sinhalfpilem  15705  cospi  15714  ef2pi  15719  ef2kpi  15720  efper  15721  sinperlem  15722  sin2kpi  15725  cos2kpi  15726  sin2pim  15727  cos2pim  15728  ptolemy  15738  sincosq3sgn  15742  sincosq4sgn  15743  sinq12gt0  15744  cosq23lt0  15747  coseq00topi  15749  tangtx  15752  sincos4thpi  15754  sincos6thpi  15756  sincos3rdpi  15757  pigt3  15758  abssinper  15760  coskpi  15762  cosq34lt1  15764  logsqrt  15837  2logb9irrALT  15888  1sgm2ppw  15912  perfect1  15915  perfectlem1  15916  perfectlem2  15917  perfect  15918  lgsdir2lem2  15951  gausslemma2dlem6  15989  lgsquadlem1  15999  lgsquadlem2  16000  lgsquad2lem2  16004  m1lgs  16007  2lgslem3a  16015  2lgslem3b  16016  2lgslem3c  16017  2lgslem3d  16018  2lgsoddprmlem2  16028  2lgsoddprmlem3c  16031  2lgsoddprmlem3d  16032  clwwlknonex2  16483  ex-fl  16542  ex-ceil  16543  ex-exp  16544  ex-fac  16545