Theorem 2cn 8936

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

Syntax hints:   ∈ wcel 2141  ℂcc 7759  2c2 8916

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 7853  ax-1re 7855  ax-addrcl 7858

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 8924

This theorem is referenced by:  2ex  8937  2cnd  8938  2m1e1  8983  3m1e2  8985  2p2e4  8992  times2  8994  2div2e1  8997  1p2e3  8999  3p3e6  9007  4p3e7  9009  5p3e8  9012  6p3e9  9015  2t1e2  9018  2t2e4  9019  3t3e9  9022  2t0e0  9024  4d2e2  9025  2cnne0  9074  1mhlfehlf  9083  8th4div3  9084  halfpm6th  9085  2mulicn  9087  2muliap0  9089  halfcl  9091  half0  9093  2halves  9094  halfaddsub  9099  div4p1lem1div2  9118  3halfnz  9296  zneo  9300  nneoor  9301  zeo  9304  7p3e10  9404  4t4e16  9428  6t3e18  9434  7t7e49  9443  8t5e40  9447  9t9e81  9458  decbin0  9469  decbin2  9470  halfthird  9472  fztpval  10026  fz0tp  10065  fz0to4untppr  10067  fzo0to3tp  10162  2tnp1ge0ge0  10244  expubnd  10520  sq2  10558  sq4e2t8  10560  cu2  10561  subsq2  10570  binom2sub  10576  binom3  10580  zesq  10581  fac2  10652  fac3  10653  faclbnd2  10663  bcn2  10685  4bc2eq6  10695  crre  10808  addcj  10842  imval2  10845  resqrexlemover  10961  resqrexlemcalc1  10965  resqrexlemnm  10969  resqrexlemcvg  10970  amgm2  11069  arisum  11448  arisum2  11449  geo2sum2  11465  geo2lim  11466  geoihalfsum  11472  efcllemp  11608  ege2le3  11621  tanval2ap  11663  tanval3ap  11664  efi4p  11667  efival  11682  sinadd  11686  cosadd  11687  sinmul  11694  cosmul  11695  cos2tsin  11701  ef01bndlem  11706  sin01bnd  11707  cos01bnd  11708  cos1bnd  11709  cos2bnd  11710  cos01gt0  11712  sin02gt0  11713  sin4lt0  11716  cos12dec  11717  egt2lt3  11729  odd2np1lem  11818  odd2np1  11819  ltoddhalfle  11839  halfleoddlt  11840  opoe  11841  omoe  11842  opeo  11843  omeo  11844  nno  11852  nn0o  11853  flodddiv4  11880  6gcd4e2  11937  3lcm2e6woprm  12027  6lcm4e12  12028  sqrt2irrlem  12102  oddpwdclemodd  12113  pythagtriplem1  12206  pythagtriplem12  12216  pythagtriplem14  12218  coscn  13444  sinhalfpilem  13465  cospi  13474  ef2pi  13479  ef2kpi  13480  efper  13481  sinperlem  13482  sin2kpi  13485  cos2kpi  13486  sin2pim  13487  cos2pim  13488  ptolemy  13498  sincosq3sgn  13502  sincosq4sgn  13503  sinq12gt0  13504  cosq23lt0  13507  coseq00topi  13509  tangtx  13512  sincos4thpi  13514  sincos6thpi  13516  sincos3rdpi  13517  pigt3  13518  abssinper  13520  coskpi  13522  cosq34lt1  13524  logsqrt  13596  2logb9irrALT  13645  lgsdir2lem2  13683  ex-fl  13719  ex-ceil  13720  ex-exp  13721  ex-fac  13722