Theorem 2cn 9375

Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)

Assertion

Ref	Expression
2cn	|- 2 e. CC

Proof of Theorem 2cn

Step	Hyp	Ref	Expression
1		2re 9374	. 2 |- 2 e. RR
2	1	recni 8338	1 |- 2 e. CC

This proof depends on syntax axioms:   e. wcel 2209   CCcc 8177   2c2 9355

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 8271  ax-1re 8273  ax-addrcl 8276

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 9363

This theorem is used by:  2ex  9376  2cnd  9377  2m1e1  9422  3m1e2  9424  2p2e4  9431  times2  9433  2div2e1  9437  1p2e3  9439  3p3e6  9447  4p3e7  9449  5p3e8  9452  6p3e9  9455  2t1e2  9458  2t2e4  9459  3t3e9  9462  2t0e0  9464  4d2e2  9465  2cnne0  9514  1mhlfehlf  9523  8th4div3  9524  halfpm6th  9525  2mulicn  9527  2muliap0  9529  halfcl  9531  half0  9533  2halves  9534  halfaddsub  9539  div4p1lem1div2  9559  3halfnz  9743  zneo  9747  nneoor  9748  zeo  9751  7p3e10  9851  4t4e16  9875  6t3e18  9881  7t7e49  9890  8t5e40  9894  9t9e81  9905  decbin0  9916  decbin2  9917  halfthird  9919  fztpval  10490  fz0tp  10529  fz0to4untppr  10531  fzo0to3tp  10637  2tnp1ge0ge0  10736  fldiv4lem1div2  10742  expubnd  11033  sq2  11072  sq4e2t8  11074  cu2  11075  subsq2  11084  binom2sub  11090  binom3  11094  zesq  11096  fac2  11169  fac3  11170  faclbnd2  11180  bcn2  11202  4bc2eq6  11213  crre  11622  addcj  11656  imval2  11659  resqrexlemover  11776  resqrexlemcalc1  11780  resqrexlemnm  11784  resqrexlemcvg  11785  amgm2  11884  arisum  12265  arisum2  12266  geo2sum2  12282  geo2lim  12283  geoihalfsum  12289  efcllemp  12425  ege2le3  12438  tanval2ap  12480  tanval3ap  12481  efi4p  12484  efival  12499  sinadd  12503  cosadd  12504  sinmul  12511  cosmul  12512  cos2tsin  12518  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  cos1bnd  12526  cos2bnd  12527  cos01gt0  12530  sin02gt0  12531  sin4lt0  12534  cos12dec  12535  egt2lt3  12547  odd2np1lem  12639  odd2np1  12640  ltoddhalfle  12660  halfleoddlt  12661  opoe  12662  omoe  12663  opeo  12664  omeo  12665  nno  12673  nn0o  12674  flodddiv4  12703  bits0  12715  bitsfzolem  12721  0bits  12726  bitsinv1  12729  6gcd4e2  12772  3lcm2e6woprm  12864  6lcm4e12  12865  sqrt2irrlem  12939  oddpwdclemodd  12950  pythagtriplem1  13044  pythagtriplem12  13054  pythagtriplem14  13056  4sqlem11  13180  4sqlem12  13181  dec5dvds  13191  dec2nprm  13194  2exp5  13211  2exp6  13212  2exp7  13213  2exp8  13214  2exp11  13215  2exp16  13216  ballotfilem2  13228  ballotfilemth  13281  maxcncf  15716  mincncf  15717  coscn  15871  sinhalfpilem  15892  cospi  15901  ef2pi  15906  ef2kpi  15907  efper  15908  sinperlem  15909  sin2kpi  15912  cos2kpi  15913  sin2pim  15914  cos2pim  15915  ptolemy  15925  sincosq3sgn  15929  sincosq4sgn  15930  sinq12gt0  15931  cosq23lt0  15934  coseq00topi  15936  tangtx  15939  sincos4thpi  15941  sincos6thpi  15943  sincos3rdpi  15944  pigt3  15945  abssinper  15947  coskpi  15949  cosq34lt1  15951  logsqrt  16025  2logb9irrALT  16076  log2tlbndlog2  16082  log2ublem2  16084  log2ublem3  16085  log2ublog2  16086  birthdaylog2  16090  1sgm2ppw  16109  perfect1  16112  perfectlem1  16113  perfectlem2  16114  perfect  16115  lgsdir2lem2  16148  gausslemma2dlem6  16186  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem2  16201  m1lgs  16204  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2lgsoddprmlem2  16225  2lgsoddprmlem3c  16228  2lgsoddprmlem3d  16229  clwwlknonex2  16680  ex-fl  16739  ex-ceil  16740  ex-exp  16741  ex-fac  16742