Theorem 2cn 9214

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 9213	. 2 |- 2 e. RR
2	1	recni 8191	1 |- 2 e. CC

Syntax hints:   e. wcel 2202   CCcc 8030   2c2 9194

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213  df-2 9202

This theorem is referenced by:  2ex  9215  2cnd  9216  2m1e1  9261  3m1e2  9263  2p2e4  9270  times2  9272  2div2e1  9276  1p2e3  9278  3p3e6  9286  4p3e7  9288  5p3e8  9291  6p3e9  9294  2t1e2  9297  2t2e4  9298  3t3e9  9301  2t0e0  9303  4d2e2  9304  2cnne0  9353  1mhlfehlf  9362  8th4div3  9363  halfpm6th  9364  2mulicn  9366  2muliap0  9368  halfcl  9370  half0  9372  2halves  9373  halfaddsub  9378  div4p1lem1div2  9398  3halfnz  9577  zneo  9581  nneoor  9582  zeo  9585  7p3e10  9685  4t4e16  9709  6t3e18  9715  7t7e49  9724  8t5e40  9728  9t9e81  9739  decbin0  9750  decbin2  9751  halfthird  9753  fztpval  10318  fz0tp  10357  fz0to4untppr  10359  fzo0to3tp  10465  2tnp1ge0ge0  10562  fldiv4lem1div2  10568  expubnd  10859  sq2  10898  sq4e2t8  10900  cu2  10901  subsq2  10910  binom2sub  10916  binom3  10920  zesq  10921  fac2  10994  fac3  10995  faclbnd2  11005  bcn2  11027  4bc2eq6  11037  crre  11435  addcj  11469  imval2  11472  resqrexlemover  11588  resqrexlemcalc1  11592  resqrexlemnm  11596  resqrexlemcvg  11597  amgm2  11696  arisum  12077  arisum2  12078  geo2sum2  12094  geo2lim  12095  geoihalfsum  12101  efcllemp  12237  ege2le3  12250  tanval2ap  12292  tanval3ap  12293  efi4p  12296  efival  12311  sinadd  12315  cosadd  12316  sinmul  12323  cosmul  12324  cos2tsin  12330  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  cos1bnd  12338  cos2bnd  12339  cos01gt0  12342  sin02gt0  12343  sin4lt0  12346  cos12dec  12347  egt2lt3  12359  odd2np1lem  12451  odd2np1  12452  ltoddhalfle  12472  halfleoddlt  12473  opoe  12474  omoe  12475  opeo  12476  omeo  12477  nno  12485  nn0o  12486  flodddiv4  12515  bits0  12527  bitsfzolem  12533  0bits  12538  bitsinv1  12541  6gcd4e2  12584  3lcm2e6woprm  12676  6lcm4e12  12677  sqrt2irrlem  12751  oddpwdclemodd  12762  pythagtriplem1  12856  pythagtriplem12  12866  pythagtriplem14  12868  4sqlem11  12992  4sqlem12  12993  dec5dvds  13003  dec2nprm  13006  2exp5  13023  2exp6  13024  2exp7  13025  2exp8  13026  2exp11  13027  2exp16  13028  maxcncf  15358  mincncf  15359  coscn  15513  sinhalfpilem  15534  cospi  15543  ef2pi  15548  ef2kpi  15549  efper  15550  sinperlem  15551  sin2kpi  15554  cos2kpi  15555  sin2pim  15556  cos2pim  15557  ptolemy  15567  sincosq3sgn  15571  sincosq4sgn  15572  sinq12gt0  15573  cosq23lt0  15576  coseq00topi  15578  tangtx  15581  sincos4thpi  15583  sincos6thpi  15585  sincos3rdpi  15586  pigt3  15587  abssinper  15589  coskpi  15591  cosq34lt1  15593  logsqrt  15666  2logb9irrALT  15717  1sgm2ppw  15738  perfect1  15741  perfectlem1  15742  perfectlem2  15743  perfect  15744  lgsdir2lem2  15777  gausslemma2dlem6  15815  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem2  15830  m1lgs  15833  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2lgsoddprmlem2  15854  2lgsoddprmlem3c  15857  2lgsoddprmlem3d  15858  clwwlknonex2  16309  ex-fl  16368  ex-ceil  16369  ex-exp  16370  ex-fac  16371