MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zcnd Unicode version

Theorem zcnd 10995
Description: An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
zred.1
Assertion
Ref Expression
zcnd

Proof of Theorem zcnd
StepHypRef Expression
1 zred.1 . . 3
21zred 10994 . 2
32recnd 9643 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cc 9511   cz 10889
This theorem is referenced by:  zsupss  11200  rpnnen1lem5  11241  fzm1  11787  fzrevral  11792  fzshftral  11795  nn0disj  11820  fzoss2  11853  fzosubel  11875  fzosubel3  11877  fzocatel  11880  fzosplitsnm1  11890  quoremz  11982  intfrac2  11985  intfracq  11986  flpmodeq  12001  moddiffl  12007  modmul1  12040  modmul12d  12041  uzrdgxfr  12077  fzen2  12079  monoord2  12138  seqf1olem1  12146  seqf1olem2  12147  seqz  12155  expaddzlem  12209  modexp  12301  bcm1k  12393  bcp1nk  12395  bcval5  12396  bcpasc  12399  hashfz  12485  hashfzo  12487  hashbclem  12501  seqcoll  12512  ccatval3  12597  ccatlid  12603  ccatass  12605  swrd0val  12648  swrdid  12652  swrd0fv  12666  swrdspsleq  12673  swrds1  12676  ccatswrd  12681  swrdswrd0  12687  spllen  12730  splfv1  12731  splfv2a  12732  revccat  12740  revrev  12741  cshwidxmod  12774  cshwidxm1  12777  cshweqrep  12789  2cshwcshw  12793  seqshft  12918  fzomaxdif  13176  climshft2  13405  iserex  13479  isercoll2  13491  serf0  13503  iseraltlem2  13505  iseraltlem3  13506  iseralt  13507  sumrblem  13533  fsumm1  13566  fsumsplitsnun  13570  fsump1  13571  fsumshftm  13596  fsumrev2  13597  telfsumo  13616  fsumparts  13620  binomlem  13641  isumshft  13651  isumsplit  13652  isum1p  13653  arisum  13671  cvgrat  13692  mertenslem1  13693  ntrivcvg  13706  ntrivcvgtail  13709  prodrblem  13736  fprodser  13756  fprodm1  13771  fprodp1  13773  fprodrev  13781  eirrlem  13937  sqr2irrlem  13981  dvds2ln  14014  dvdsadd2b  14028  fsumdvds  14029  fzocongeq  14040  dvdsexp  14042  dvdsmod  14043  odd2np1  14046  oddm1even  14047  oexpneg  14049  3dvds  14050  divalglem0  14051  divalglem4  14054  divalglem8  14058  divalgb  14062  divalgmod  14064  bitsp1  14081  bitsfzo  14085  bitsmod  14086  bitsinv1lem  14091  bitsf1  14096  sadaddlem  14116  bitsres  14123  bitsuz  14124  bitsshft  14125  smumullem  14142  modgcd  14174  bezoutlem1  14176  bezoutlem2  14177  bezoutlem3  14178  bezoutlem4  14179  dvdsmulgcd  14192  rplpwr  14194  mulgcddvds  14245  rpexp  14261  qmuldeneqnum  14280  numdensq  14287  qden1elz  14290  hashdvds  14305  phiprm  14307  eulerthlem2  14312  fermltl  14314  prmdiv  14315  prmdiveq  14316  odzdvds  14322  modprm0  14330  modprmn0modprm0  14332  pythagtriplem6  14345  pythagtriplem7  14346  pythagtriplem15  14353  pcpremul  14367  pceulem  14369  pczpre  14371  pcdiv  14376  pcqmul  14377  pcqdiv  14381  pcexp  14383  pcaddlem  14407  pcadd  14408  fldivp1  14416  pcfac  14418  pcbc  14419  prmpwdvds  14422  prmreclem4  14437  4sqlem5  14460  4sqlem8  14463  4sqlem9  14464  4sqlem10  14465  4sqlem11  14473  4sqlem14  14476  4sqlem16  14478  4sqlem17  14479  vdwapun  14492  vdwnnlem2  14514  prmlem0  14591  mulgsubcl  16156  mulgdirlem  16166  mulgdir  16167  mulgass  16172  mulgsubdir  16173  psgnunilem5  16519  psgnunilem2  16520  psgnunilem4  16522  m1expaddsub  16523  psgnuni  16524  odnncl  16569  odmulg  16578  odbezout  16580  sylow1lem1  16618  sylow2alem2  16638  efgsres  16756  efgredleme  16761  efgredlemc  16763  odadd1  16854  odadd2  16855  cyggeninv  16886  gsummptshft  16956  ablfacrp  17117  pgpfac1lem3  17128  srgbinomlem3  17193  srgbinomlem4  17194  zringmulg  18496  zrngmulg  18503  zringlpirlem1  18509  zringlpirlem3  18511  zlpirlem1  18514  zlpirlem3  18516  prmirredlem  18523  prmirredlemOLD  18526  zndvds0  18589  znf1o  18590  znunit  18602  cayhamlem1  19367  tgpmulg  20592  zdis  21321  uniioombllem3  21994  mbfi1fseqlem4  22125  dvexp3  22379  aareccl  22722  aalioulem1  22728  geolim3  22735  aaliou3lem2  22739  aaliou3lem6  22744  ulmshft  22785  sineq0  22914  efif1olem2  22930  wilthlem1  23342  wilthlem2  23343  basellem3  23356  mumul  23455  musum  23467  musumsum  23468  muinv  23469  ppiub  23479  chtub  23487  logfac2  23492  chpchtsum  23494  dchrptlem1  23539  pcbcctr  23551  bcmono  23552  bposlem5  23563  bposlem6  23564  lgslem1  23571  lgsval2lem  23581  lgsval4a  23593  lgsneg  23594  lgsneg1  23595  lgsmod  23596  lgsdirprm  23604  lgsdir  23605  lgsdilem2  23606  lgsdi  23607  lgsne0  23608  lgsabs1  23609  lgssq  23610  lgssq2  23611  lgsdirnn0  23614  lgsdinn0  23615  lgsqrlem1  23616  lgseisenlem1  23624  lgseisenlem2  23625  lgseisenlem3  23626  lgseisenlem4  23627  lgsquadlem1  23629  lgsquad2lem1  23633  lgsquad3  23636  2sqlem3  23641  2sqlem4  23642  2sqlem8a  23646  2sqlem8  23647  2sqlem11  23650  2sqblem  23652  dchrisumlem1  23674  dchrmusum2  23679  dchrvmasumlem1  23680  dchrvmasum2lem  23681  mudivsum  23715  mulogsum  23717  mulog2sumlem2  23720  selberglem1  23730  selberglem3  23732  selberg  23733  pntpbnd2  23772  pntlemf  23790  padicabvcxp  23817  axlowdimlem14  24258  axlowdimlem16  24260  wlkdvspthlem  24609  fargshiftf1  24637  fargshiftfo  24638  clwwisshclww  24807  eupatrl  24968  gxmodid  25281  znsqcld  27561  fzspl  27598  bcm1n  27600  numdenneg  27608  divnumden2  27609  ltesubnnd  27612  2sqn0  27634  2sqmod  27636  archiabllem1  27737  archiabllem2c  27739  zrhnm  27950  cnzh  27951  rezh  27952  qqhval2lem  27962  qqhghm  27969  qqhrhm  27970  qqhnm  27971  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemic  28445  ballotlem1c  28446  ballotlemsgt1  28449  ballotlemsdom  28450  ballotlemsel1i  28451  ballotlemsf1o  28452  ballotlemsima  28454  ballotlemfrceq  28467  ballotlemfrcn0  28468  ballotlem1ri  28473  signsplypnf  28507  igamz  28590  divcnvlin  29118  fallfacval3  29134  fallfacfwd  29158  0fallfac  29159  binomfallfaclem2  29162  fallfacval4  29165  predfz  29283  fsumkthpow  29818  ltflcei  30043  fdc  30238  mettrifi  30250  caushft  30254  cntotbnd  30292  mzpsubmpt  30675  lzenom  30703  diophun  30707  eqrabdioph  30711  irrapxlem2  30759  irrapxlem3  30760  pellexlem6  30770  pell1234qrreccl  30790  pellfund14  30834  rmxyneg  30856  rmxyadd  30857  rmxp1  30868  rmxm1  30870  rmym1  30871  rmxluc  30872  rmyluc  30873  rmyluc2  30874  rmxdbl  30875  rmydbl  30876  congadd  30904  congsub  30908  congabseq  30912  acongrep  30918  acongeq  30921  jm2.18  30930  jm2.19lem1  30931  jm2.19lem2  30932  jm2.19lem3  30933  jm2.22  30937  jm2.23  30938  jm2.20nn  30939  jm2.25  30941  jm2.26lem3  30943  jm2.27c  30949  hashgcdlem  31157  lcmid  31215  nzss  31222  hashnzfz  31225  hashnzfz2  31226  hashnzfzclim  31227  uzmptshftfval  31251  fzisoeu  31500  fperiodmul  31504  fmul01lt1lem2  31579  sumnnodd  31636  dvdsn1add  31736  dvnmul  31740  dvnprodlem1  31743  stoweidlem11  31793  stoweidlem26  31808  dirkertrigeqlem1  31880  dirkertrigeqlem2  31881  dirkertrigeqlem3  31882  dirkertrigeq  31883  dirkeritg  31884  fourierdlem26  31915  fourierdlem48  31937  fourierdlem49  31938  fourierdlem79  31968  fourierdlem91  31980  fourierdlem103  31992  fourierdlem104  31993  fouriersw  32014  etransclem1  32018  etransclem4  32021  etransclem8  32025  etransclem9  32026  etransclem15  32032  etransclem17  32034  etransclem18  32035  etransclem20  32037  etransclem21  32038  etransclem22  32039  etransclem23  32040  etransclem24  32041  etransclem25  32042  etransclem35  32052  etransclem38  32055  etransclem41  32058  etransclem44  32061  etransclem45  32062  etransclem46  32063  etransclem47  32064  etransclem48  32065  2elfz2melfz  32334  fsumsplitsndif  32346  2zrngamnd  32747  2zrngacmnd  32748  2zrngagrp  32749  2zrngALT  32754  2zrngnmlid  32755  2zrngnmlid2  32757  ztprmneprm  32936  altgsumbcALT  32942  sineq0ALT  33737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-resscn 9570
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-neg 9831  df-z 10890
  Copyright terms: Public domain W3C validator