Theorem 2cn 9304

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

Syntax hints:   ∈ wcel 2203  ℂcc 8121  2c2 9284

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 2214  ax-resscn 8215  ax-1re 8217  ax-addrcl 8220

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223  df-2 9292

This theorem is referenced by:  2ex  9305  2cnd  9306  2m1e1  9351  3m1e2  9353  2p2e4  9360  times2  9362  2div2e1  9366  1p2e3  9368  3p3e6  9376  4p3e7  9378  5p3e8  9381  6p3e9  9384  2t1e2  9387  2t2e4  9388  3t3e9  9391  2t0e0  9393  4d2e2  9394  2cnne0  9443  1mhlfehlf  9452  8th4div3  9453  halfpm6th  9454  2mulicn  9456  2muliap0  9458  halfcl  9460  half0  9462  2halves  9463  halfaddsub  9468  div4p1lem1div2  9488  3halfnz  9671  zneo  9675  nneoor  9676  zeo  9679  7p3e10  9779  4t4e16  9803  6t3e18  9809  7t7e49  9818  8t5e40  9822  9t9e81  9833  decbin0  9844  decbin2  9845  halfthird  9847  fztpval  10413  fz0tp  10452  fz0to4untppr  10454  fzo0to3tp  10560  2tnp1ge0ge0  10657  fldiv4lem1div2  10663  expubnd  10954  sq2  10993  sq4e2t8  10995  cu2  10996  subsq2  11005  binom2sub  11011  binom3  11015  zesq  11016  fac2  11089  fac3  11090  faclbnd2  11100  bcn2  11122  4bc2eq6  11132  crre  11535  addcj  11569  imval2  11572  resqrexlemover  11688  resqrexlemcalc1  11692  resqrexlemnm  11696  resqrexlemcvg  11697  amgm2  11796  arisum  12177  arisum2  12178  geo2sum2  12194  geo2lim  12195  geoihalfsum  12201  efcllemp  12337  ege2le3  12350  tanval2ap  12392  tanval3ap  12393  efi4p  12396  efival  12411  sinadd  12415  cosadd  12416  sinmul  12423  cosmul  12424  cos2tsin  12430  ef01bndlem  12435  sin01bnd  12436  cos01bnd  12437  cos1bnd  12438  cos2bnd  12439  cos01gt0  12442  sin02gt0  12443  sin4lt0  12446  cos12dec  12447  egt2lt3  12459  odd2np1lem  12551  odd2np1  12552  ltoddhalfle  12572  halfleoddlt  12573  opoe  12574  omoe  12575  opeo  12576  omeo  12577  nno  12585  nn0o  12586  flodddiv4  12615  bits0  12627  bitsfzolem  12633  0bits  12638  bitsinv1  12641  6gcd4e2  12684  3lcm2e6woprm  12776  6lcm4e12  12777  sqrt2irrlem  12851  oddpwdclemodd  12862  pythagtriplem1  12956  pythagtriplem12  12966  pythagtriplem14  12968  4sqlem11  13092  4sqlem12  13093  dec5dvds  13103  dec2nprm  13106  2exp5  13123  2exp6  13124  2exp7  13125  2exp8  13126  2exp11  13127  2exp16  13128  maxcncf  15467  mincncf  15468  coscn  15622  sinhalfpilem  15643  cospi  15652  ef2pi  15657  ef2kpi  15658  efper  15659  sinperlem  15660  sin2kpi  15663  cos2kpi  15664  sin2pim  15665  cos2pim  15666  ptolemy  15676  sincosq3sgn  15680  sincosq4sgn  15681  sinq12gt0  15682  cosq23lt0  15685  coseq00topi  15687  tangtx  15690  sincos4thpi  15692  sincos6thpi  15694  sincos3rdpi  15695  pigt3  15696  abssinper  15698  coskpi  15700  cosq34lt1  15702  logsqrt  15775  2logb9irrALT  15826  1sgm2ppw  15850  perfect1  15853  perfectlem1  15854  perfectlem2  15855  perfect  15856  lgsdir2lem2  15889  gausslemma2dlem6  15927  lgsquadlem1  15937  lgsquadlem2  15938  lgsquad2lem2  15942  m1lgs  15945  2lgslem3a  15953  2lgslem3b  15954  2lgslem3c  15955  2lgslem3d  15956  2lgsoddprmlem2  15966  2lgsoddprmlem3c  15969  2lgsoddprmlem3d  15970  clwwlknonex2  16421  ex-fl  16480  ex-ceil  16481  ex-exp  16482  ex-fac  16483