Theorem 2cn 9207

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

Syntax hints:   ∈ wcel 2200  ℂcc 8023  2c2 9187

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8117  ax-1re 8119  ax-addrcl 8122

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211  df-2 9195

This theorem is referenced by:  2ex  9208  2cnd  9209  2m1e1  9254  3m1e2  9256  2p2e4  9263  times2  9265  2div2e1  9269  1p2e3  9271  3p3e6  9279  4p3e7  9281  5p3e8  9284  6p3e9  9287  2t1e2  9290  2t2e4  9291  3t3e9  9294  2t0e0  9296  4d2e2  9297  2cnne0  9346  1mhlfehlf  9355  8th4div3  9356  halfpm6th  9357  2mulicn  9359  2muliap0  9361  halfcl  9363  half0  9365  2halves  9366  halfaddsub  9371  div4p1lem1div2  9391  3halfnz  9570  zneo  9574  nneoor  9575  zeo  9578  7p3e10  9678  4t4e16  9702  6t3e18  9708  7t7e49  9717  8t5e40  9721  9t9e81  9732  decbin0  9743  decbin2  9744  halfthird  9746  fztpval  10311  fz0tp  10350  fz0to4untppr  10352  fzo0to3tp  10457  2tnp1ge0ge0  10554  fldiv4lem1div2  10560  expubnd  10851  sq2  10890  sq4e2t8  10892  cu2  10893  subsq2  10902  binom2sub  10908  binom3  10912  zesq  10913  fac2  10986  fac3  10987  faclbnd2  10997  bcn2  11019  4bc2eq6  11029  crre  11411  addcj  11445  imval2  11448  resqrexlemover  11564  resqrexlemcalc1  11568  resqrexlemnm  11572  resqrexlemcvg  11573  amgm2  11672  arisum  12052  arisum2  12053  geo2sum2  12069  geo2lim  12070  geoihalfsum  12076  efcllemp  12212  ege2le3  12225  tanval2ap  12267  tanval3ap  12268  efi4p  12271  efival  12286  sinadd  12290  cosadd  12291  sinmul  12298  cosmul  12299  cos2tsin  12305  ef01bndlem  12310  sin01bnd  12311  cos01bnd  12312  cos1bnd  12313  cos2bnd  12314  cos01gt0  12317  sin02gt0  12318  sin4lt0  12321  cos12dec  12322  egt2lt3  12334  odd2np1lem  12426  odd2np1  12427  ltoddhalfle  12447  halfleoddlt  12448  opoe  12449  omoe  12450  opeo  12451  omeo  12452  nno  12460  nn0o  12461  flodddiv4  12490  bits0  12502  bitsfzolem  12508  0bits  12513  bitsinv1  12516  6gcd4e2  12559  3lcm2e6woprm  12651  6lcm4e12  12652  sqrt2irrlem  12726  oddpwdclemodd  12737  pythagtriplem1  12831  pythagtriplem12  12841  pythagtriplem14  12843  4sqlem11  12967  4sqlem12  12968  dec5dvds  12978  dec2nprm  12981  2exp5  12998  2exp6  12999  2exp7  13000  2exp8  13001  2exp11  13002  2exp16  13003  maxcncf  15332  mincncf  15333  coscn  15487  sinhalfpilem  15508  cospi  15517  ef2pi  15522  ef2kpi  15523  efper  15524  sinperlem  15525  sin2kpi  15528  cos2kpi  15529  sin2pim  15530  cos2pim  15531  ptolemy  15541  sincosq3sgn  15545  sincosq4sgn  15546  sinq12gt0  15547  cosq23lt0  15550  coseq00topi  15552  tangtx  15555  sincos4thpi  15557  sincos6thpi  15559  sincos3rdpi  15560  pigt3  15561  abssinper  15563  coskpi  15565  cosq34lt1  15567  logsqrt  15640  2logb9irrALT  15691  1sgm2ppw  15712  perfect1  15715  perfectlem1  15716  perfectlem2  15717  perfect  15718  lgsdir2lem2  15751  gausslemma2dlem6  15789  lgsquadlem1  15799  lgsquadlem2  15800  lgsquad2lem2  15804  m1lgs  15807  2lgslem3a  15815  2lgslem3b  15816  2lgslem3c  15817  2lgslem3d  15818  2lgsoddprmlem2  15828  2lgsoddprmlem3c  15831  2lgsoddprmlem3d  15832  clwwlknonex2  16248  ex-fl  16271  ex-ceil  16272  ex-exp  16273  ex-fac  16274