Theorem 2cn 9114

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

Syntax hints:   ∈ wcel 2177  ℂcc 7930  2c2 9094

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-resscn 8024  ax-1re 8026  ax-addrcl 8029

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3173  df-ss 3180  df-2 9102

This theorem is referenced by:  2ex  9115  2cnd  9116  2m1e1  9161  3m1e2  9163  2p2e4  9170  times2  9172  2div2e1  9176  1p2e3  9178  3p3e6  9186  4p3e7  9188  5p3e8  9191  6p3e9  9194  2t1e2  9197  2t2e4  9198  3t3e9  9201  2t0e0  9203  4d2e2  9204  2cnne0  9253  1mhlfehlf  9262  8th4div3  9263  halfpm6th  9264  2mulicn  9266  2muliap0  9268  halfcl  9270  half0  9272  2halves  9273  halfaddsub  9278  div4p1lem1div2  9298  3halfnz  9477  zneo  9481  nneoor  9482  zeo  9485  7p3e10  9585  4t4e16  9609  6t3e18  9615  7t7e49  9624  8t5e40  9628  9t9e81  9639  decbin0  9650  decbin2  9651  halfthird  9653  fztpval  10212  fz0tp  10251  fz0to4untppr  10253  fzo0to3tp  10355  2tnp1ge0ge0  10451  fldiv4lem1div2  10457  expubnd  10748  sq2  10787  sq4e2t8  10789  cu2  10790  subsq2  10799  binom2sub  10805  binom3  10809  zesq  10810  fac2  10883  fac3  10884  faclbnd2  10894  bcn2  10916  4bc2eq6  10926  crre  11212  addcj  11246  imval2  11249  resqrexlemover  11365  resqrexlemcalc1  11369  resqrexlemnm  11373  resqrexlemcvg  11374  amgm2  11473  arisum  11853  arisum2  11854  geo2sum2  11870  geo2lim  11871  geoihalfsum  11877  efcllemp  12013  ege2le3  12026  tanval2ap  12068  tanval3ap  12069  efi4p  12072  efival  12087  sinadd  12091  cosadd  12092  sinmul  12099  cosmul  12100  cos2tsin  12106  ef01bndlem  12111  sin01bnd  12112  cos01bnd  12113  cos1bnd  12114  cos2bnd  12115  cos01gt0  12118  sin02gt0  12119  sin4lt0  12122  cos12dec  12123  egt2lt3  12135  odd2np1lem  12227  odd2np1  12228  ltoddhalfle  12248  halfleoddlt  12249  opoe  12250  omoe  12251  opeo  12252  omeo  12253  nno  12261  nn0o  12262  flodddiv4  12291  bits0  12303  bitsfzolem  12309  0bits  12314  bitsinv1  12317  6gcd4e2  12360  3lcm2e6woprm  12452  6lcm4e12  12453  sqrt2irrlem  12527  oddpwdclemodd  12538  pythagtriplem1  12632  pythagtriplem12  12642  pythagtriplem14  12644  4sqlem11  12768  4sqlem12  12769  dec5dvds  12779  dec2nprm  12782  2exp5  12799  2exp6  12800  2exp7  12801  2exp8  12802  2exp11  12803  2exp16  12804  maxcncf  15131  mincncf  15132  coscn  15286  sinhalfpilem  15307  cospi  15316  ef2pi  15321  ef2kpi  15322  efper  15323  sinperlem  15324  sin2kpi  15327  cos2kpi  15328  sin2pim  15329  cos2pim  15330  ptolemy  15340  sincosq3sgn  15344  sincosq4sgn  15345  sinq12gt0  15346  cosq23lt0  15349  coseq00topi  15351  tangtx  15354  sincos4thpi  15356  sincos6thpi  15358  sincos3rdpi  15359  pigt3  15360  abssinper  15362  coskpi  15364  cosq34lt1  15366  logsqrt  15439  2logb9irrALT  15490  1sgm2ppw  15511  perfect1  15514  perfectlem1  15515  perfectlem2  15516  perfect  15517  lgsdir2lem2  15550  gausslemma2dlem6  15588  lgsquadlem1  15598  lgsquadlem2  15599  lgsquad2lem2  15603  m1lgs  15606  2lgslem3a  15614  2lgslem3b  15615  2lgslem3c  15616  2lgslem3d  15617  2lgsoddprmlem2  15627  2lgsoddprmlem3c  15630  2lgsoddprmlem3d  15631  ex-fl  15735  ex-ceil  15736  ex-exp  15737  ex-fac  15738