Theorem 2cn 8784

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

Syntax hints:   ∈ wcel 1480  ℂcc 7611  2c2 8764

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-resscn 7705  ax-1re 7707  ax-addrcl 7710

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-in 3072  df-ss 3079  df-2 8772

This theorem is referenced by:  2ex  8785  2cnd  8786  2m1e1  8831  3m1e2  8833  2p2e4  8840  times2  8842  2div2e1  8845  1p2e3  8847  3p3e6  8855  4p3e7  8857  5p3e8  8860  6p3e9  8863  2t1e2  8866  2t2e4  8867  3t3e9  8870  2t0e0  8872  4d2e2  8873  2cnne0  8922  1mhlfehlf  8931  8th4div3  8932  halfpm6th  8933  2mulicn  8935  2muliap0  8937  halfcl  8939  half0  8941  2halves  8942  halfaddsub  8947  div4p1lem1div2  8966  3halfnz  9141  zneo  9145  nneoor  9146  zeo  9149  7p3e10  9249  4t4e16  9273  6t3e18  9279  7t7e49  9288  8t5e40  9292  9t9e81  9303  decbin0  9314  decbin2  9315  halfthird  9317  fztpval  9856  fz0tp  9894  fzo0to3tp  9989  2tnp1ge0ge0  10067  expubnd  10343  sq2  10381  sq4e2t8  10383  cu2  10384  subsq2  10393  binom2sub  10398  binom3  10402  zesq  10403  fac2  10470  fac3  10471  faclbnd2  10481  bcn2  10503  4bc2eq6  10513  crre  10622  addcj  10656  imval2  10659  resqrexlemover  10775  resqrexlemcalc1  10779  resqrexlemnm  10783  resqrexlemcvg  10784  amgm2  10883  arisum  11260  arisum2  11261  geo2sum2  11277  geo2lim  11278  geoihalfsum  11284  efcllemp  11353  ege2le3  11366  tanval2ap  11409  tanval3ap  11410  efi4p  11413  efival  11428  sinadd  11432  cosadd  11433  sinmul  11440  cosmul  11441  cos2tsin  11447  ef01bndlem  11452  sin01bnd  11453  cos01bnd  11454  cos1bnd  11455  cos2bnd  11456  cos01gt0  11458  sin02gt0  11459  sin4lt0  11462  cos12dec  11463  egt2lt3  11475  odd2np1lem  11558  odd2np1  11559  ltoddhalfle  11579  halfleoddlt  11580  opoe  11581  omoe  11582  opeo  11583  omeo  11584  nno  11592  nn0o  11593  flodddiv4  11620  6gcd4e2  11672  3lcm2e6woprm  11756  6lcm4e12  11757  sqrt2irrlem  11828  oddpwdclemodd  11839  coscn  12848  sinhalfpilem  12861  cospi  12870  ef2pi  12875  ef2kpi  12876  efper  12877  sinperlem  12878  sin2kpi  12881  cos2kpi  12882  sin2pim  12883  cos2pim  12884  ptolemy  12894  sincosq3sgn  12898  sincosq4sgn  12899  sinq12gt0  12900  cosq23lt0  12903  coseq00topi  12905  tangtx  12908  sincos4thpi  12910  sincos6thpi  12912  sincos3rdpi  12913  pigt3  12914  abssinper  12916  coskpi  12918  cosq34lt1  12920  ex-fl  12926  ex-ceil  12927  ex-exp  12928  ex-fac  12929