MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2cn Structured version   Visualization version   GIF version

Theorem 2cn 11036
Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
Assertion
Ref Expression
2cn 2 ∈ ℂ

Proof of Theorem 2cn
StepHypRef Expression
1 2re 11035 . 2 2 ∈ ℝ
21recni 9997 1 2 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1992  cc 9879  2c2 11015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-i2m1 9949  ax-1ne0 9950  ax-rrecex 9953  ax-cnre 9954
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5813  df-fv 5858  df-ov 6608  df-2 11024
This theorem is referenced by:  2ex  11037  2cnd  11038  2m1e1  11080  3m1e2  11082  2p2e4  11089  times2  11091  2div2e1  11095  1p2e3  11097  3p3e6  11106  4p3e7  11108  5p3e8  11111  6p3e9  11115  7p3e10OLD  11118  2t1e2  11121  2t2e4  11122  3t3e9  11125  2t0e0  11128  4d2e2  11129  2cnne0  11187  halfcn  11192  1mhlfehlf  11196  8th4div3  11197  halfpm6th  11198  2mulicn  11200  2muline0  11201  halfcl  11202  half0  11204  2halves  11205  halfaddsub  11210  div4p1lem1div2  11232  3halfnz  11400  zneo  11404  nneo  11405  zeo  11407  7p3e10  11547  4t4e16  11577  6t3e18  11586  7t7e49  11597  8t5e40  11601  8t5e40OLD  11602  9t9e81  11614  decbin0  11626  decbin2  11627  halfthird  11629  fztpval  12341  fz0tp  12378  fz0to4untppr  12380  fzo0to3tp  12492  fzo1to4tp  12494  expubnd  12858  sq2  12897  sq4e2t8  12899  cu2  12900  subsq2  12910  binom2sub  12918  binom3  12922  zesq  12924  fac2  13003  fac3  13004  faclbnd2  13015  faclbnd4lem1  13017  faclbnd4lem3  13019  faclbnd4lem4  13020  faclbnd5  13022  bcn2  13043  4bc2eq6  13053  swrd2lsw  13624  crre  13783  addcj  13817  imval2  13820  sqrlem7  13918  absmax  13998  rddif  14009  sqreulem  14028  amgm2  14038  abs3lemi  14078  iseraltlem2  14342  ackbijnn  14480  climcndslem1  14501  climcndslem2  14502  arisum  14512  arisum2  14513  geo2sum2  14525  geo2lim  14526  geoihalfsum  14534  bpoly2  14708  bpoly3  14709  bpoly4  14710  fsumcube  14711  efcllem  14728  ege2le3  14740  efgt0  14753  tanval2  14783  tanval3  14784  efi4p  14787  efival  14802  sinadd  14814  cosadd  14815  sinmul  14822  cos2tsin  14829  ef01bndlem  14834  cos01bnd  14836  cos1bnd  14837  cos2bnd  14838  cos01gt0  14841  sin02gt0  14842  sin4lt0  14845  znnenlem  14860  sqr2irrlem  14897  odd2np1lem  14983  odd2np1  14984  opoe  15006  omoe  15007  opeo  15008  omeo  15009  nno  15017  nn0o  15018  flodddiv4  15056  bits0  15069  bitsfzolem  15075  0bits  15080  bitsinv1  15083  sadcadd  15099  smumullem  15133  6gcd4e2  15174  3lcm2e6woprm  15247  6lcm4e12  15248  pythagtriplem1  15440  pythagtriplem12  15450  pythagtriplem14  15452  pythagtriplem15  15453  pythagtriplem16  15454  pythagtriplem17  15455  iserodd  15459  prmreclem5  15543  prmreclem6  15544  4sqlem11  15578  4sqlem12  15579  prmo2  15663  prmo3  15664  dec5dvds  15687  dec2nprm  15690  decexp2  15698  2exp6  15714  2exp8  15715  2exp16  15716  7prm  15736  11prm  15741  13prm  15742  37prm  15747  43prm  15748  83prm  15749  139prm  15750  163prm  15751  317prm  15752  631prm  15753  1259lem1  15757  1259lem2  15758  1259lem3  15759  1259lem4  15760  1259lem5  15761  1259prm  15762  2503lem1  15763  2503lem2  15764  2503lem3  15765  4001lem1  15767  4001lem2  15768  4001lem3  15769  4001lem4  15770  4001prm  15771  psgnunilem2  17831  efgtlen  18055  efgredleme  18072  frgpnabllem1  18192  lt6abl  18212  htpycc  22682  pcoval2  22719  pcocn  22720  pcohtpylem  22722  pcopt  22725  pcopt2  22726  pcoass  22727  pcorevlem  22729  csbren  23085  minveclem2  23100  ovolunlem1a  23166  ovolunlem1  23167  vitalilem4  23281  mbfi1fseqlem5  23387  dvmptre  23633  dvsincos  23643  aaliou3lem2  23997  aaliou3lem3  23998  aaliou3lem8  23999  coscn  24098  sinhalfpilem  24114  cospi  24123  ef2pi  24128  ef2kpi  24129  efper  24130  sinperlem  24131  sin2kpi  24134  cos2kpi  24135  sin2pim  24136  cos2pim  24137  sinhalfpip  24143  sinhalfpim  24144  coshalfpip  24145  coshalfpim  24146  sincosq3sgn  24151  sincosq4sgn  24152  tangtx  24156  sinq12gt0  24158  sincosq1eq  24163  sincos4thpi  24164  sincos6thpi  24166  sincos3rdpi  24167  pige3  24168  abssinper  24169  coskpi  24171  sineq0  24172  coseq1  24173  efeq1  24174  efif1olem4  24190  eflogeq  24247  tanarg  24264  cxpsqrtlem  24343  cxpsqrt  24344  logsqrt  24345  root1eq1  24391  cxpeq  24393  ang180lem2  24435  ang180lem3  24436  quad2  24461  1cubrlem  24463  1cubr  24464  dcubic2  24466  dcubic1  24467  dcubic  24468  mcubic  24469  cubic2  24470  cubic  24471  dquartlem1  24473  dquartlem2  24474  dquart  24475  quart1lem  24477  quart1  24478  quartlem1  24479  quartlem2  24480  quartlem3  24481  quart  24483  sinasin  24511  asinsin  24514  atancj  24532  efiatan  24534  efiatan2  24539  2efiatan  24540  tanatan  24541  atantan  24545  atanbndlem  24547  atans2  24553  dvatan  24557  atantayl2  24560  leibpilem1  24562  leibpilem2  24563  log2cnv  24566  log2tlbnd  24567  log2ublem2  24569  log2ublem3  24570  log2ub  24571  birthday  24576  zetacvg  24636  basellem1  24702  basellem3  24704  basellem8  24709  basellem9  24710  cht3  24794  1sgm2ppw  24820  ppiub  24824  chtublem  24831  chtub  24832  perfect1  24848  perfectlem1  24849  perfectlem2  24850  perfect  24851  bcmax  24898  bcp1ctr  24899  bclbnd  24900  bpos1lem  24902  bpos1  24903  bposlem1  24904  bposlem2  24905  bposlem4  24907  bposlem5  24908  bposlem6  24909  bposlem8  24911  bposlem9  24912  lgsdir2lem2  24946  gausslemma2dlem6  24992  lgsquadlem1  25000  lgsquadlem2  25001  lgsquad2lem2  25005  m1lgs  25008  2lgslem3a  25016  2lgslem3b  25017  2lgslem3c  25018  2lgslem3d  25019  2lgsoddprmlem2  25029  2lgsoddprmlem3c  25032  2lgsoddprmlem3d  25033  rplogsumlem1  25068  dchrisum0fno1  25095  dchrisum0lem1  25100  dchrisum0lem2  25102  logdivsum  25117  mulog2sumlem3  25120  log2sumbnd  25128  selberglem1  25129  selberglem2  25130  selberg2  25135  selberg4lem1  25144  selberg3r  25153  pntpbnd1a  25169  pntpbnd2  25171  pntibndlem2  25175  pntlemk  25190  ax5seglem7  25710  axlowdimlem13  25729  elwspths2spth  26723  clwlkclwwlklem2a4  26759  numclwwlkovf2ex  27069  ex-fl  27152  ex-ceil  27153  ex-exp  27155  ex-fac  27156  ex-abs  27160  ex-ind-dvds  27166  ipidsq  27405  cncph  27514  ip0i  27520  ip1ilem  27521  ipdirilem  27524  minvecolem2  27571  hvsubcan2i  27761  norm-ii-i  27834  norm3lem  27846  normpar2i  27853  polid2i  27854  hhph  27875  mayete3i  28427  nmcexi  28725  opsqrlem6  28844  addltmulALT  29145  omssubadd  30135  oddpwdc  30189  fib5  30240  ballotlem2  30323  ballotth  30372  problem4  31262  problem5  31263  quad3  31264  cnndvlem1  32143  sin2h  32998  cos2h  32999  tan2h  33000  poimirlem29  33037  mblfinlem1  33045  mblfinlem2  33046  mblfinlem3  33047  itg2addnclem3  33062  dvasin  33095  areacirc  33104  heiborlem6  33214  rmxluc  36948  rmyluc  36949  jm2.17a  36974  jm2.18  37002  jm2.23  37010  jm3.1lem1  37031  proot1ex  37227  areaquad  37250  lhe4.4ex1a  37977  sineq0ALT  38623  coskpi2  39348  cosnegpi  39349  cosknegpi  39351  stoweidlem26  39518  wallispilem4  39560  wallispi  39562  wallispi2lem1  39563  stirlinglem8  39573  dirkerper  39588  dirkertrigeqlem3  39592  dirkertrigeq  39593  dirkeritg  39594  dirkercncflem1  39595  dirkercncflem2  39596  fourierdlem57  39655  fourierdlem58  39656  fourierdlem62  39660  fourierdlem76  39674  fourierdlem103  39701  fourierdlem104  39702  sqwvfourb  39721  fourierswlem  39722  fmtnoge3  40710  fmtnorec1  40717  fmtno0  40720  fmtno1  40721  fmtnorec3  40728  fmtnorec4  40729  fmtno5lem2  40734  fmtno5lem4  40736  257prm  40741  fmtnoprmfac2lem1  40746  fmtno4prmfac  40752  fmtno5faclem2  40760  fmtno5faclem3  40761  fmtno5fac  40762  2exp5  40775  139prmALT  40779  31prm  40780  2exp7  40782  127prm  40783  2exp11  40785  mod42tp1mod8  40787  lighneallem2  40791  lighneallem3  40792  lighneallem4a  40793  3exp4mod41  40801  41prothprmlem1  40802  41prothprmlem2  40803  41prothprm  40804  bits0ALTV  40858  0evenALTV  40867  6even  40888  8even  40890  perfectALTVlem1  40894  perfectALTVlem2  40895  perfectALTV  40896  nnsum3primes4  40934  bgoldbtbndlem1  40951  0nodd  41052  0even  41173  2even  41175  2zrngamgm  41181  2t6m3t4e0  41368  linevalexample  41427  zlmodzxzequap  41531  pw2m1lepw2m1  41553  nnlog2ge0lt1  41607  logbpw2m1  41608  nnpw2blen  41621  nnpw2pmod  41624  blen1  41625  blen2  41626  blennnt2  41630  nnolog2flm1  41631  0dig2nn0e  41653  0dig2nn0o  41654  nn0sumshdiglemA  41660  nn0sumshdiglemB  41661  nn0sumshdiglem1  41662  nn0sumshdiglem2  41663  sinhpcosh  41729
  Copyright terms: Public domain W3C validator