Theorem 2cn 9354

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 9353	. 2 |- 2 e. RR
2	1	recni 8328	1 |- 2 e. CC

Syntax hints:   e. wcel 2209   CCcc 8167   2c2 9334

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 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 8261  ax-1re 8263  ax-addrcl 8266

This theorem 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 9342

This theorem is referenced by:  2ex  9355  2cnd  9356  2m1e1  9401  3m1e2  9403  2p2e4  9410  times2  9412  2div2e1  9416  1p2e3  9418  3p3e6  9426  4p3e7  9428  5p3e8  9431  6p3e9  9434  2t1e2  9437  2t2e4  9438  3t3e9  9441  2t0e0  9443  4d2e2  9444  2cnne0  9493  1mhlfehlf  9502  8th4div3  9503  halfpm6th  9504  2mulicn  9506  2muliap0  9508  halfcl  9510  half0  9512  2halves  9513  halfaddsub  9518  div4p1lem1div2  9538  3halfnz  9722  zneo  9726  nneoor  9727  zeo  9730  7p3e10  9830  4t4e16  9854  6t3e18  9860  7t7e49  9869  8t5e40  9873  9t9e81  9884  decbin0  9895  decbin2  9896  halfthird  9898  fztpval  10468  fz0tp  10507  fz0to4untppr  10509  fzo0to3tp  10615  2tnp1ge0ge0  10714  fldiv4lem1div2  10720  expubnd  11011  sq2  11050  sq4e2t8  11052  cu2  11053  subsq2  11062  binom2sub  11068  binom3  11072  zesq  11074  fac2  11147  fac3  11148  faclbnd2  11158  bcn2  11180  4bc2eq6  11191  crre  11600  addcj  11634  imval2  11637  resqrexlemover  11754  resqrexlemcalc1  11758  resqrexlemnm  11762  resqrexlemcvg  11763  amgm2  11862  arisum  12243  arisum2  12244  geo2sum2  12260  geo2lim  12261  geoihalfsum  12267  efcllemp  12403  ege2le3  12416  tanval2ap  12458  tanval3ap  12459  efi4p  12462  efival  12477  sinadd  12481  cosadd  12482  sinmul  12489  cosmul  12490  cos2tsin  12496  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  cos1bnd  12504  cos2bnd  12505  cos01gt0  12508  sin02gt0  12509  sin4lt0  12512  cos12dec  12513  egt2lt3  12525  odd2np1lem  12617  odd2np1  12618  ltoddhalfle  12638  halfleoddlt  12639  opoe  12640  omoe  12641  opeo  12642  omeo  12643  nno  12651  nn0o  12652  flodddiv4  12681  bits0  12693  bitsfzolem  12699  0bits  12704  bitsinv1  12707  6gcd4e2  12750  3lcm2e6woprm  12842  6lcm4e12  12843  sqrt2irrlem  12917  oddpwdclemodd  12928  pythagtriplem1  13022  pythagtriplem12  13032  pythagtriplem14  13034  4sqlem11  13158  4sqlem12  13159  dec5dvds  13169  dec2nprm  13172  2exp5  13189  2exp6  13190  2exp7  13191  2exp8  13192  2exp11  13193  2exp16  13194  ballotfilem2  13206  ballotfilemth  13259  maxcncf  15639  mincncf  15640  coscn  15794  sinhalfpilem  15815  cospi  15824  ef2pi  15829  ef2kpi  15830  efper  15831  sinperlem  15832  sin2kpi  15835  cos2kpi  15836  sin2pim  15837  cos2pim  15838  ptolemy  15848  sincosq3sgn  15852  sincosq4sgn  15853  sinq12gt0  15854  cosq23lt0  15857  coseq00topi  15859  tangtx  15862  sincos4thpi  15864  sincos6thpi  15866  sincos3rdpi  15867  pigt3  15868  abssinper  15870  coskpi  15872  cosq34lt1  15874  logsqrt  15948  2logb9irrALT  15999  1sgm2ppw  16023  perfect1  16026  perfectlem1  16027  perfectlem2  16028  perfect  16029  lgsdir2lem2  16062  gausslemma2dlem6  16100  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem2  16115  m1lgs  16118  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2lgsoddprmlem2  16139  2lgsoddprmlem3c  16142  2lgsoddprmlem3d  16143  clwwlknonex2  16594  ex-fl  16653  ex-ceil  16654  ex-exp  16655  ex-fac  16656