Theorem 2cn 8984

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

Syntax hints:   ∈ wcel 2148  ℂcc 7804  2c2 8964

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7898  ax-1re 7900  ax-addrcl 7903

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142  df-2 8972

This theorem is referenced by:  2ex  8985  2cnd  8986  2m1e1  9031  3m1e2  9033  2p2e4  9040  times2  9042  2div2e1  9045  1p2e3  9047  3p3e6  9055  4p3e7  9057  5p3e8  9060  6p3e9  9063  2t1e2  9066  2t2e4  9067  3t3e9  9070  2t0e0  9072  4d2e2  9073  2cnne0  9122  1mhlfehlf  9131  8th4div3  9132  halfpm6th  9133  2mulicn  9135  2muliap0  9137  halfcl  9139  half0  9141  2halves  9142  halfaddsub  9147  div4p1lem1div2  9166  3halfnz  9344  zneo  9348  nneoor  9349  zeo  9352  7p3e10  9452  4t4e16  9476  6t3e18  9482  7t7e49  9491  8t5e40  9495  9t9e81  9506  decbin0  9517  decbin2  9518  halfthird  9520  fztpval  10076  fz0tp  10115  fz0to4untppr  10117  fzo0to3tp  10212  2tnp1ge0ge0  10294  expubnd  10570  sq2  10608  sq4e2t8  10610  cu2  10611  subsq2  10620  binom2sub  10626  binom3  10630  zesq  10631  fac2  10702  fac3  10703  faclbnd2  10713  bcn2  10735  4bc2eq6  10745  crre  10857  addcj  10891  imval2  10894  resqrexlemover  11010  resqrexlemcalc1  11014  resqrexlemnm  11018  resqrexlemcvg  11019  amgm2  11118  arisum  11497  arisum2  11498  geo2sum2  11514  geo2lim  11515  geoihalfsum  11521  efcllemp  11657  ege2le3  11670  tanval2ap  11712  tanval3ap  11713  efi4p  11716  efival  11731  sinadd  11735  cosadd  11736  sinmul  11743  cosmul  11744  cos2tsin  11750  ef01bndlem  11755  sin01bnd  11756  cos01bnd  11757  cos1bnd  11758  cos2bnd  11759  cos01gt0  11761  sin02gt0  11762  sin4lt0  11765  cos12dec  11766  egt2lt3  11778  odd2np1lem  11867  odd2np1  11868  ltoddhalfle  11888  halfleoddlt  11889  opoe  11890  omoe  11891  opeo  11892  omeo  11893  nno  11901  nn0o  11902  flodddiv4  11929  6gcd4e2  11986  3lcm2e6woprm  12076  6lcm4e12  12077  sqrt2irrlem  12151  oddpwdclemodd  12162  pythagtriplem1  12255  pythagtriplem12  12265  pythagtriplem14  12267  coscn  13973  sinhalfpilem  13994  cospi  14003  ef2pi  14008  ef2kpi  14009  efper  14010  sinperlem  14011  sin2kpi  14014  cos2kpi  14015  sin2pim  14016  cos2pim  14017  ptolemy  14027  sincosq3sgn  14031  sincosq4sgn  14032  sinq12gt0  14033  cosq23lt0  14036  coseq00topi  14038  tangtx  14041  sincos4thpi  14043  sincos6thpi  14045  sincos3rdpi  14046  pigt3  14047  abssinper  14049  coskpi  14051  cosq34lt1  14053  logsqrt  14125  2logb9irrALT  14174  lgsdir2lem2  14212  ex-fl  14248  ex-ceil  14249  ex-exp  14250  ex-fac  14251