Theorem 2cn 9385

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

This proof depends on syntax axioms:   ∈ wcel 2209  ℂcc 8184  2c2 9365

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 8278  ax-1re 8280  ax-addrcl 8283

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 9373

This theorem is used by:  2ex  9386  2cnd  9387  2m1e1  9432  3m1e2  9434  2p2e4  9441  times2  9443  2div2e1  9447  1p2e3  9449  3p3e6  9457  4p3e7  9459  5p3e8  9462  6p3e9  9465  2t1e2  9468  2t2e4  9469  2t3e6  9472  3t3e9  9473  2t4e8  9475  2t0e0  9476  4d2e2  9477  2cnne0  9526  1mhlfehlf  9535  8th4div3  9536  halfpm6th  9537  2mulicn  9539  2muliap0  9541  halfcl  9543  half0  9545  2halves  9546  halfaddsub  9551  div4p1lem1div2  9571  3halfnz  9755  zneo  9759  nneoor  9760  zeo  9763  7p3e10  9868  4t4e16  9892  6t3e18  9898  7t7e49  9907  8t5e40  9911  9t9e81  9922  decbin0  9933  decbin2  9934  halfthird  9936  fztpval  10508  fz0tp  10547  fz0to4untppr  10549  fzo0to3tp  10655  2tnp1ge0ge0  10758  fldiv4lem1div2  10764  expubnd  11055  sq2  11094  sq4e2t8  11096  cu2  11097  subsq2  11106  binom2sub  11112  binom3  11116  zesq  11118  fac2  11192  fac3  11193  faclbnd2  11203  bcn2  11225  4bc2eq6  11236  crre  11645  addcj  11679  imval2  11682  resqrexlemover  11799  resqrexlemcalc1  11803  resqrexlemnm  11807  resqrexlemcvg  11808  amgm2  11908  arisum  12291  arisum2  12292  geo2sum2  12308  geo2lim  12309  geoihalfsum  12315  efcllemp  12451  ege2le3  12464  tanval2ap  12506  tanval3ap  12507  efi4p  12510  efival  12525  sinadd  12529  cosadd  12530  sinmul  12537  cosmul  12538  cos2tsin  12544  ef01bndlem  12549  sin01bnd  12550  cos01bnd  12551  cos1bnd  12552  cos2bnd  12553  cos01gt0  12556  sin02gt0  12557  sin4lt0  12560  cos12dec  12561  egt2lt3  12573  odd2np1lem  12665  odd2np1  12666  ltoddhalfle  12686  halfleoddlt  12687  opoe  12688  omoe  12689  opeo  12690  omeo  12691  nno  12699  nn0o  12700  flodddiv4  12729  bits0  12741  bitsfzolem  12747  0bits  12752  bitsinv1  12755  6gcd4e2  12798  3lcm2e6woprm  12890  6lcm4e12  12891  sqrt2irrlem  12966  pythagtriplem1  13074  pythagtriplem12  13084  pythagtriplem14  13086  4sqlem11  13210  4sqlem12  13211  dec5dvds  13221  dec2nprm  13224  2exp5  13242  2exp6  13243  2exp7  13244  2exp8  13245  2exp11  13246  2exp16  13247  10nprm  13258  11prm  13259  13prm  13260  37prm  13265  43prm  13266  83prm  13267  139prm  13268  163prm  13269  317prm  13270  631prm  13271  1259lem1  13272  1259lem2  13273  1259lem3  13274  1259lem4  13275  1259lem5  13276  1259prm  13277  ballotfilem2  13287  ballotfilemth  13340  maxcncf  15853  mincncf  15854  coscn  16008  sinhalfpilem  16030  cospi  16039  ef2pi  16044  ef2kpi  16045  efper  16046  sinperlem  16047  sin2kpi  16050  cos2kpi  16051  sin2pim  16052  cos2pim  16053  ptolemy  16063  sincosq3sgn  16067  sincosq4sgn  16068  sinq12gt0  16069  cosq23lt0  16072  coseq00topi  16074  tangtx  16077  sincos4thpi  16079  sincos6thpi  16081  sincos3rdpi  16082  pigt3  16083  abssinper  16085  coskpi  16087  sineq0re  16088  cosq34lt1  16090  root1idef  16096  logsqrt  16170  efnthr  16188  2logb9irrALT  16222  log2tlbndlog2  16232  log2ublem2  16234  log2ublem3  16235  log2ublog2  16236  birthdaylog2  16240  1sgm2ppw  16301  ppiqub  16305  chtublem  16307  chtqub  16308  perfect1  16310  perfectlem1  16311  perfectlem2  16312  perfect  16313  bcmax  16317  bcp1ctr  16318  bclbnd  16319  bpos1lem  16321  bpos1  16322  bposlem1  16323  bposlem2  16324  bposlem4  16326  bposlem5  16327  bposlem6  16328  bposlem8  16330  bposlem9  16331  lgsdir2lem2  16365  gausslemma2dlem6  16403  lgsquadlem1  16413  lgsquadlem2  16414  lgsquad2lem2  16418  m1lgs  16421  2lgslem3a  16429  2lgslem3b  16430  2lgslem3c  16431  2lgslem3d  16432  2lgsoddprmlem2  16442  2lgsoddprmlem3c  16445  2lgsoddprmlem3d  16446  clwwlknonex2  16897  ex-fl  16956  ex-ceil  16957  ex-exp  16958  ex-fac  16959