Theorem 2cn 8949

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

Syntax hints:   ∈ wcel 2141  ℂcc 7772  2c2 8929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-resscn 7866  ax-1re 7868  ax-addrcl 7871

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134  df-2 8937

This theorem is referenced by:  2ex  8950  2cnd  8951  2m1e1  8996  3m1e2  8998  2p2e4  9005  times2  9007  2div2e1  9010  1p2e3  9012  3p3e6  9020  4p3e7  9022  5p3e8  9025  6p3e9  9028  2t1e2  9031  2t2e4  9032  3t3e9  9035  2t0e0  9037  4d2e2  9038  2cnne0  9087  1mhlfehlf  9096  8th4div3  9097  halfpm6th  9098  2mulicn  9100  2muliap0  9102  halfcl  9104  half0  9106  2halves  9107  halfaddsub  9112  div4p1lem1div2  9131  3halfnz  9309  zneo  9313  nneoor  9314  zeo  9317  7p3e10  9417  4t4e16  9441  6t3e18  9447  7t7e49  9456  8t5e40  9460  9t9e81  9471  decbin0  9482  decbin2  9483  halfthird  9485  fztpval  10039  fz0tp  10078  fz0to4untppr  10080  fzo0to3tp  10175  2tnp1ge0ge0  10257  expubnd  10533  sq2  10571  sq4e2t8  10573  cu2  10574  subsq2  10583  binom2sub  10589  binom3  10593  zesq  10594  fac2  10665  fac3  10666  faclbnd2  10676  bcn2  10698  4bc2eq6  10708  crre  10821  addcj  10855  imval2  10858  resqrexlemover  10974  resqrexlemcalc1  10978  resqrexlemnm  10982  resqrexlemcvg  10983  amgm2  11082  arisum  11461  arisum2  11462  geo2sum2  11478  geo2lim  11479  geoihalfsum  11485  efcllemp  11621  ege2le3  11634  tanval2ap  11676  tanval3ap  11677  efi4p  11680  efival  11695  sinadd  11699  cosadd  11700  sinmul  11707  cosmul  11708  cos2tsin  11714  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  cos1bnd  11722  cos2bnd  11723  cos01gt0  11725  sin02gt0  11726  sin4lt0  11729  cos12dec  11730  egt2lt3  11742  odd2np1lem  11831  odd2np1  11832  ltoddhalfle  11852  halfleoddlt  11853  opoe  11854  omoe  11855  opeo  11856  omeo  11857  nno  11865  nn0o  11866  flodddiv4  11893  6gcd4e2  11950  3lcm2e6woprm  12040  6lcm4e12  12041  sqrt2irrlem  12115  oddpwdclemodd  12126  pythagtriplem1  12219  pythagtriplem12  12229  pythagtriplem14  12231  coscn  13485  sinhalfpilem  13506  cospi  13515  ef2pi  13520  ef2kpi  13521  efper  13522  sinperlem  13523  sin2kpi  13526  cos2kpi  13527  sin2pim  13528  cos2pim  13529  ptolemy  13539  sincosq3sgn  13543  sincosq4sgn  13544  sinq12gt0  13545  cosq23lt0  13548  coseq00topi  13550  tangtx  13553  sincos4thpi  13555  sincos6thpi  13557  sincos3rdpi  13558  pigt3  13559  abssinper  13561  coskpi  13563  cosq34lt1  13565  logsqrt  13637  2logb9irrALT  13686  lgsdir2lem2  13724  ex-fl  13760  ex-ceil  13761  ex-exp  13762  ex-fac  13763