Theorem 2cn 9080

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

Syntax hints:   ∈ wcel 2167  ℂcc 7896  2c2 9060

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7990  ax-1re 7992  ax-addrcl 7995

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170  df-2 9068

This theorem is referenced by:  2ex  9081  2cnd  9082  2m1e1  9127  3m1e2  9129  2p2e4  9136  times2  9138  2div2e1  9142  1p2e3  9144  3p3e6  9152  4p3e7  9154  5p3e8  9157  6p3e9  9160  2t1e2  9163  2t2e4  9164  3t3e9  9167  2t0e0  9169  4d2e2  9170  2cnne0  9219  1mhlfehlf  9228  8th4div3  9229  halfpm6th  9230  2mulicn  9232  2muliap0  9234  halfcl  9236  half0  9238  2halves  9239  halfaddsub  9244  div4p1lem1div2  9264  3halfnz  9442  zneo  9446  nneoor  9447  zeo  9450  7p3e10  9550  4t4e16  9574  6t3e18  9580  7t7e49  9589  8t5e40  9593  9t9e81  9604  decbin0  9615  decbin2  9616  halfthird  9618  fztpval  10177  fz0tp  10216  fz0to4untppr  10218  fzo0to3tp  10314  2tnp1ge0ge0  10410  fldiv4lem1div2  10416  expubnd  10707  sq2  10746  sq4e2t8  10748  cu2  10749  subsq2  10758  binom2sub  10764  binom3  10768  zesq  10769  fac2  10842  fac3  10843  faclbnd2  10853  bcn2  10875  4bc2eq6  10885  crre  11041  addcj  11075  imval2  11078  resqrexlemover  11194  resqrexlemcalc1  11198  resqrexlemnm  11202  resqrexlemcvg  11203  amgm2  11302  arisum  11682  arisum2  11683  geo2sum2  11699  geo2lim  11700  geoihalfsum  11706  efcllemp  11842  ege2le3  11855  tanval2ap  11897  tanval3ap  11898  efi4p  11901  efival  11916  sinadd  11920  cosadd  11921  sinmul  11928  cosmul  11929  cos2tsin  11935  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  cos1bnd  11943  cos2bnd  11944  cos01gt0  11947  sin02gt0  11948  sin4lt0  11951  cos12dec  11952  egt2lt3  11964  odd2np1lem  12056  odd2np1  12057  ltoddhalfle  12077  halfleoddlt  12078  opoe  12079  omoe  12080  opeo  12081  omeo  12082  nno  12090  nn0o  12091  flodddiv4  12120  bits0  12132  bitsfzolem  12138  0bits  12143  bitsinv1  12146  6gcd4e2  12189  3lcm2e6woprm  12281  6lcm4e12  12282  sqrt2irrlem  12356  oddpwdclemodd  12367  pythagtriplem1  12461  pythagtriplem12  12471  pythagtriplem14  12473  4sqlem11  12597  4sqlem12  12598  dec5dvds  12608  dec2nprm  12611  2exp5  12628  2exp6  12629  2exp7  12630  2exp8  12631  2exp11  12632  2exp16  12633  maxcncf  14959  mincncf  14960  coscn  15114  sinhalfpilem  15135  cospi  15144  ef2pi  15149  ef2kpi  15150  efper  15151  sinperlem  15152  sin2kpi  15155  cos2kpi  15156  sin2pim  15157  cos2pim  15158  ptolemy  15168  sincosq3sgn  15172  sincosq4sgn  15173  sinq12gt0  15174  cosq23lt0  15177  coseq00topi  15179  tangtx  15182  sincos4thpi  15184  sincos6thpi  15186  sincos3rdpi  15187  pigt3  15188  abssinper  15190  coskpi  15192  cosq34lt1  15194  logsqrt  15267  2logb9irrALT  15318  1sgm2ppw  15339  perfect1  15342  perfectlem1  15343  perfectlem2  15344  perfect  15345  lgsdir2lem2  15378  gausslemma2dlem6  15416  lgsquadlem1  15426  lgsquadlem2  15427  lgsquad2lem2  15431  m1lgs  15434  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2lgsoddprmlem2  15455  2lgsoddprmlem3c  15458  2lgsoddprmlem3d  15459  ex-fl  15479  ex-ceil  15480  ex-exp  15481  ex-fac  15482