Theorem 2cn 9384

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

This proof depends on syntax axioms:   ∈ wcel 2209  ℂcc 8183  2c2 9364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-2 9372

This theorem is used by:  2ex  9385  2cnd  9386  2m1e1  9431  3m1e2  9433  2p2e4  9440  times2  9442  2div2e1  9446  1p2e3  9448  3p3e6  9456  4p3e7  9458  5p3e8  9461  6p3e9  9464  2t1e2  9467  2t2e4  9468  2t3e6  9471  3t3e9  9472  2t4e8  9474  2t0e0  9475  4d2e2  9476  2cnne0  9525  1mhlfehlf  9534  8th4div3  9535  halfpm6th  9536  2mulicn  9538  2muliap0  9540  halfcl  9542  half0  9544  2halves  9545  halfaddsub  9550  div4p1lem1div2  9570  3halfnz  9753  zneo  9757  nneoor  9758  zeo  9761  7p3e10  9866  4t4e16  9890  6t3e18  9896  7t7e49  9905  8t5e40  9909  9t9e81  9920  decbin0  9931  decbin2  9932  halfthird  9934  fztpval  10506  fz0tp  10545  fz0to4untppr  10547  fzo0to3tp  10653  2tnp1ge0ge0  10756  fldiv4lem1div2  10762  expubnd  11053  sq2  11092  sq4e2t8  11094  cu2  11095  subsq2  11104  binom2sub  11110  binom3  11114  zesq  11116  fac2  11190  fac3  11191  faclbnd2  11201  bcn2  11223  4bc2eq6  11234  crre  11643  addcj  11677  imval2  11680  resqrexlemover  11797  resqrexlemcalc1  11801  resqrexlemnm  11805  resqrexlemcvg  11806  amgm2  11906  arisum  12289  arisum2  12290  geo2sum2  12306  geo2lim  12307  geoihalfsum  12313  efcllemp  12449  ege2le3  12462  tanval2ap  12504  tanval3ap  12505  efi4p  12508  efival  12523  sinadd  12527  cosadd  12528  sinmul  12535  cosmul  12536  cos2tsin  12542  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  cos1bnd  12550  cos2bnd  12551  cos01gt0  12554  sin02gt0  12555  sin4lt0  12558  cos12dec  12559  egt2lt3  12571  odd2np1lem  12663  odd2np1  12664  ltoddhalfle  12684  halfleoddlt  12685  opoe  12686  omoe  12687  opeo  12688  omeo  12689  nno  12697  nn0o  12698  flodddiv4  12727  bits0  12739  bitsfzolem  12745  0bits  12750  bitsinv1  12753  6gcd4e2  12796  3lcm2e6woprm  12888  6lcm4e12  12889  sqrt2irrlem  12964  pythagtriplem1  13072  pythagtriplem12  13082  pythagtriplem14  13084  4sqlem11  13208  4sqlem12  13209  dec5dvds  13219  dec2nprm  13222  2exp5  13240  2exp6  13241  2exp7  13242  2exp8  13243  2exp11  13244  2exp16  13245  10nprm  13256  11prm  13257  13prm  13258  37prm  13263  43prm  13264  83prm  13265  139prm  13266  163prm  13267  317prm  13268  631prm  13269  1259lem1  13270  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  1259prm  13275  ballotfilem2  13285  ballotfilemth  13338  maxcncf  15858  mincncf  15859  coscn  16013  sinhalfpilem  16035  cospi  16044  ef2pi  16049  ef2kpi  16050  efper  16051  sinperlem  16052  sin2kpi  16055  cos2kpi  16056  sin2pim  16057  cos2pim  16058  ptolemy  16068  sincosq3sgn  16072  sincosq4sgn  16073  sinq12gt0  16074  cosq23lt0  16077  coseq00topi  16079  tangtx  16082  sincos4thpi  16084  sincos6thpi  16086  sincos3rdpi  16087  pigt3  16088  abssinper  16090  coskpi  16092  sineq0re  16093  cosq34lt1  16095  root1idef  16101  logsqrt  16175  efnthr  16193  2logb9irrALT  16227  log2tlbndlog2  16237  log2ublem2  16239  log2ublem3  16240  log2ublog2  16241  birthdaylog2  16245  1sgm2ppw  16306  ppiqub  16310  chtublem  16312  chtqub  16313  perfect1  16315  perfectlem1  16316  perfectlem2  16317  perfect  16318  bcmax  16322  bcp1ctr  16323  bclbnd  16324  bpos1lem  16326  bpos1  16327  bposlem1  16328  bposlem2  16329  bposlem4  16331  bposlem5  16332  bposlem6  16333  bposlem8  16335  bposlem9  16336  lgsdir2lem2  16370  gausslemma2dlem6  16408  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem2  16423  m1lgs  16426  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2lgsoddprmlem2  16447  2lgsoddprmlem3c  16450  2lgsoddprmlem3d  16451  clwwlknonex2  16902  ex-fl  16961  ex-ceil  16962  ex-exp  16963  ex-fac  16964