Theorem 2cn 9378

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 9377	. 2 |- 2 e. RR
2	1	recni 8339	1 |- 2 e. CC

This proof depends on syntax axioms:   e. wcel 2209   CCcc 8178   2c2 9358

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 8272  ax-1re 8274  ax-addrcl 8277

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 9366

This theorem is used by:  2ex  9379  2cnd  9380  2m1e1  9425  3m1e2  9427  2p2e4  9434  times2  9436  2div2e1  9440  1p2e3  9442  3p3e6  9450  4p3e7  9452  5p3e8  9455  6p3e9  9458  2t1e2  9461  2t2e4  9462  2t3e6  9465  3t3e9  9466  2t4e8  9468  2t0e0  9469  4d2e2  9470  2cnne0  9519  1mhlfehlf  9528  8th4div3  9529  halfpm6th  9530  2mulicn  9532  2muliap0  9534  halfcl  9536  half0  9538  2halves  9539  halfaddsub  9544  div4p1lem1div2  9564  3halfnz  9748  zneo  9752  nneoor  9753  zeo  9756  7p3e10  9861  4t4e16  9885  6t3e18  9891  7t7e49  9900  8t5e40  9904  9t9e81  9915  decbin0  9926  decbin2  9927  halfthird  9929  fztpval  10501  fz0tp  10540  fz0to4untppr  10542  fzo0to3tp  10648  2tnp1ge0ge0  10751  fldiv4lem1div2  10757  expubnd  11048  sq2  11087  sq4e2t8  11089  cu2  11090  subsq2  11099  binom2sub  11105  binom3  11109  zesq  11111  fac2  11185  fac3  11186  faclbnd2  11196  bcn2  11218  4bc2eq6  11229  crre  11638  addcj  11672  imval2  11675  resqrexlemover  11792  resqrexlemcalc1  11796  resqrexlemnm  11800  resqrexlemcvg  11801  amgm2  11901  arisum  12284  arisum2  12285  geo2sum2  12301  geo2lim  12302  geoihalfsum  12308  efcllemp  12444  ege2le3  12457  tanval2ap  12499  tanval3ap  12500  efi4p  12503  efival  12518  sinadd  12522  cosadd  12523  sinmul  12530  cosmul  12531  cos2tsin  12537  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  cos1bnd  12545  cos2bnd  12546  cos01gt0  12549  sin02gt0  12550  sin4lt0  12553  cos12dec  12554  egt2lt3  12566  odd2np1lem  12658  odd2np1  12659  ltoddhalfle  12679  halfleoddlt  12680  opoe  12681  omoe  12682  opeo  12683  omeo  12684  nno  12692  nn0o  12693  flodddiv4  12722  bits0  12734  bitsfzolem  12740  0bits  12745  bitsinv1  12748  6gcd4e2  12791  3lcm2e6woprm  12883  6lcm4e12  12884  sqrt2irrlem  12959  pythagtriplem1  13067  pythagtriplem12  13077  pythagtriplem14  13079  4sqlem11  13203  4sqlem12  13204  dec5dvds  13214  dec2nprm  13217  2exp5  13235  2exp6  13236  2exp7  13237  2exp8  13238  2exp11  13239  2exp16  13240  10nprm  13251  11prm  13252  13prm  13253  37prm  13258  43prm  13259  83prm  13260  139prm  13261  163prm  13262  317prm  13263  631prm  13264  1259lem1  13265  1259lem2  13266  1259lem3  13267  1259lem4  13268  1259lem5  13269  1259prm  13270  ballotfilem2  13280  ballotfilemth  13333  maxcncf  15769  mincncf  15770  coscn  15924  sinhalfpilem  15946  cospi  15955  ef2pi  15960  ef2kpi  15961  efper  15962  sinperlem  15963  sin2kpi  15966  cos2kpi  15967  sin2pim  15968  cos2pim  15969  ptolemy  15979  sincosq3sgn  15983  sincosq4sgn  15984  sinq12gt0  15985  cosq23lt0  15988  coseq00topi  15990  tangtx  15993  sincos4thpi  15995  sincos6thpi  15997  sincos3rdpi  15998  pigt3  15999  abssinper  16001  coskpi  16003  cosq34lt1  16005  logsqrt  16082  2logb9irrALT  16133  log2tlbndlog2  16143  log2ublem2  16145  log2ublem3  16146  log2ublog2  16147  birthdaylog2  16151  1sgm2ppw  16212  ppiqub  16216  chtublem  16218  chtqub  16219  perfect1  16221  perfectlem1  16222  perfectlem2  16223  perfect  16224  bcmax  16228  bcp1ctr  16229  bclbnd  16230  bpos1lem  16232  bpos1  16233  bposlem1  16234  bposlem2  16235  bposlem4  16237  bposlem5  16238  bposlem6  16239  bposlem8  16241  bposlem9  16242  lgsdir2lem2  16276  gausslemma2dlem6  16314  lgsquadlem1  16324  lgsquadlem2  16325  lgsquad2lem2  16329  m1lgs  16332  2lgslem3a  16340  2lgslem3b  16341  2lgslem3c  16342  2lgslem3d  16343  2lgsoddprmlem2  16353  2lgsoddprmlem3c  16356  2lgsoddprmlem3d  16357  clwwlknonex2  16808  ex-fl  16867  ex-ceil  16868  ex-exp  16869  ex-fac  16870