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

Theorem zcnd 11521
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 11520 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 10106 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cc 9972  cz 11415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-resscn 10031
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-neg 10307  df-z 11416
This theorem is referenced by:  zsupss  11815  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  fzm1  12458  fzrevral  12463  fzshftral  12466  nn0disj  12494  predfz  12503  fzoss2  12535  fzo0addelr  12562  fzosubel  12566  fzosubel3  12568  fzocatel  12571  fzosplitsnm1  12582  elfzom1elp1fzo1  12608  2tnp1ge0ge0  12670  quoremz  12694  intfrac2  12697  intfracq  12698  flpmodeq  12713  moddiffl  12721  modmul1  12763  modmul12d  12764  modfzo0difsn  12782  modsumfzodifsn  12783  addmodlteq  12785  uzrdgxfr  12806  fzen2  12808  monoord2  12872  seqf1olem1  12880  seqf1olem2  12881  seqz  12889  expaddzlem  12943  modexp  13039  sqoddm1div8  13068  bcm1k  13142  bcp1nk  13144  bcval5  13145  bcpasc  13148  hashfz  13252  hashfzo  13254  hashfzp1  13256  hashbclem  13274  seqcoll  13286  ccatval3  13397  ccatlid  13404  ccatass  13406  ccatalpha  13411  swrd0val  13466  swrdfv0  13470  swrdid  13474  swrd0fv  13485  swrdfv2  13492  swrds1  13497  ccatswrd  13502  swrdswrd0  13508  spllen  13551  splfv1  13552  splfv2a  13553  revccat  13561  revrev  13562  cshwidxmod  13595  cshwidxm1  13599  cshweqrep  13613  2cshwcshw  13617  cshimadifsn0  13622  seqshft  13869  fzomaxdif  14127  climshft2  14357  iserex  14431  isercoll2  14443  serf0  14455  iseraltlem2  14457  iseraltlem3  14458  iseralt  14459  sumrblem  14486  fsumm1  14524  fsumsplitsnun  14528  fsumsplitsnunOLD  14530  fsump1  14531  fsumshftm  14557  fsumrev2  14558  telfsumo  14578  fsumparts  14582  binomlem  14605  isumshft  14615  isumsplit  14616  isum1p  14617  arisum  14636  cvgrat  14659  mertenslem1  14660  ntrivcvg  14673  ntrivcvgtail  14676  prodrblem  14703  fprodser  14723  fprodm1  14741  fprodp1  14743  fprodrev  14751  fprodmodd  14772  fallfacval3  14787  fallfacfwd  14811  0fallfac  14812  binomfallfaclem2  14815  fallfacval4  14818  fsumkthpow  14831  eirrlem  14976  sqrt2irrlem  15021  sqrt2irrlemOLD  15022  dvds2ln  15061  dvdsadd2b  15075  fsumdvds  15077  fzocongeq  15093  addmodlteqALT  15094  dvdsexp  15096  dvdsmod  15097  3dvds  15099  3dvdsOLD  15100  fprodfvdvdsd  15105  odd2np1  15112  oddm1even  15114  oexpneg  15116  mod2eq1n2dvds  15118  mulsucdiv2z  15124  zob  15130  ltoddhalfle  15132  sumodd  15158  pwp1fsum  15161  divalglem0  15163  divalglem4  15166  divalglem8  15170  divalgb  15174  divalgmod  15176  divalgmodOLD  15177  modremain  15179  flodddiv4  15184  bitsp1  15200  bitsfzo  15204  bitsmod  15205  bitsinv1lem  15210  bitsf1  15215  sadaddlem  15235  bitsres  15242  bitsuz  15243  bitsshft  15244  smumullem  15261  modgcd  15300  bezoutlem1  15303  bezoutlem2  15304  bezoutlem3  15305  bezoutlem4  15306  dvdsmulgcd  15321  rplpwr  15323  lcmid  15369  absprodnn  15378  mulgcddvds  15416  divgcdcoprm0  15426  cncongr1  15428  cncongr2  15429  rpexp  15479  qmuldeneqnum  15502  numdensq  15509  qden1elz  15512  hashdvds  15527  phiprm  15529  eulerthlem2  15534  fermltl  15536  prmdiv  15537  prmdiveq  15538  hashgcdlem  15540  odzdvds  15547  vfermltlALT  15554  modprm0  15557  modprmn0modprm0  15559  pythagtriplem6  15573  pythagtriplem7  15574  pythagtriplem15  15581  pcpremul  15595  pceulem  15597  pczpre  15599  pcdiv  15604  pcqmul  15605  pcqdiv  15609  pcexp  15611  pcaddlem  15639  pcadd  15640  fldivp1  15648  pcfac  15650  pcbc  15651  prmpwdvds  15655  prmreclem4  15670  4sqlem5  15693  4sqlem8  15696  4sqlem9  15697  4sqlem10  15698  4sqlem11  15706  4sqlem14  15709  4sqlem16  15711  4sqlem17  15712  vdwapun  15725  vdwnnlem2  15747  prmop1  15789  prmdvdsprmo  15793  prmgaplem7  15808  prmlem0  15859  mulgsubcl  17602  mulgdirlem  17619  mulgdir  17620  mulgass  17626  mulgmodid  17628  mulgsubdir  17629  psgnunilem5  17960  psgnunilem2  17961  psgnunilem4  17963  m1expaddsub  17964  psgnuni  17965  odnncl  18010  odmulg  18019  odbezout  18021  sylow1lem1  18059  sylow2alem2  18079  efgsres  18197  efgredleme  18202  efgredlemc  18204  odadd1  18297  odadd2  18298  cyggeninv  18331  gsummptshft  18382  ablfacrp  18511  pgpfac1lem3  18522  srgbinomlem3  18588  srgbinomlem4  18589  zringmulg  19874  zringlpirlem1  19880  zringlpirlem3  19882  prmirredlem  19889  zndvds0  19947  znf1o  19948  znunit  19960  cayhamlem1  20719  tgpmulg  21944  zdis  22666  uniioombllem3  23399  mbfi1fseqlem4  23530  dvexp3  23786  aareccl  24126  aalioulem1  24132  geolim3  24139  aaliou3lem2  24143  aaliou3lem6  24148  ulmshft  24189  sineq0  24318  efif1olem2  24334  igamz  24819  wilthlem1  24839  wilthlem2  24840  basellem3  24854  mumul  24952  musum  24962  musumsum  24963  muinv  24964  ppiub  24974  chtub  24982  logfac2  24987  chpchtsum  24989  dchrptlem1  25034  pcbcctr  25046  bcmono  25047  bposlem5  25058  bposlem6  25059  lgslem1  25067  lgsval2lem  25077  lgsval4a  25089  lgsneg  25091  lgsneg1  25092  lgsmod  25093  lgsdirprm  25101  lgsdir  25102  lgsdilem2  25103  lgsdi  25104  lgsne0  25105  lgsabs1  25106  lgssq  25107  lgssq2  25108  lgsmulsqcoprm  25113  lgsdirnn0  25114  lgsdinn0  25115  lgsqrlem1  25116  gausslemma2dlem1a  25135  gausslemma2dlem1  25136  gausslemma2dlem4  25139  gausslemma2dlem5a  25140  gausslemma2dlem5  25141  gausslemma2dlem6  25142  gausslemma2d  25144  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgseisenlem4  25148  lgsquadlem1  25150  lgsquad2lem1  25154  lgsquad3  25157  2lgslem1b  25162  2lgsoddprmlem2  25179  2sqlem3  25190  2sqlem4  25191  2sqlem8a  25195  2sqlem8  25196  2sqlem11  25199  2sqblem  25201  dchrisumlem1  25223  dchrmusum2  25228  dchrvmasumlem1  25229  dchrvmasum2lem  25230  mudivsum  25264  mulogsum  25266  mulog2sumlem2  25269  selberglem1  25279  selberglem3  25281  selberg  25282  pntpbnd2  25321  pntlemf  25339  padicabvcxp  25366  axlowdimlem14  25880  axlowdimlem16  25882  pthdadjvtx  26682  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  crctcshlem4  26768  crctcsh  26772  clwwisshclwws  26972  eucrctshift  27221  clwwlkccatlem  27331  znsqcld  29640  fzspl  29678  bcm1n  29682  numdenneg  29691  divnumden2  29692  ltesubnnd  29696  2sqn0  29774  2sqmod  29776  archiabllem1  29875  archiabllem2c  29877  zrhnm  30141  cnzh  30142  rezh  30143  qqhval2lem  30153  qqhghm  30160  qqhrhm  30161  qqhnm  30162  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemic  30696  ballotlem1c  30697  ballotlemsgt1  30700  ballotlemsdom  30701  ballotlemsel1i  30702  ballotlemsf1o  30703  ballotlemsima  30705  ballotlemfrceq  30718  ballotlemfrcn0  30719  ballotlem1ri  30724  signsplypnf  30755  itgexpif  30812  fsum2dsub  30813  breprexplemc  30838  vtsprod  30845  circlemeth  30846  divcnvlin  31744  fwddifnp1  32397  knoppndvlem2  32629  knoppndvlem7  32634  knoppndvlem14  32641  knoppndvlem16  32643  ltflcei  33527  poimirlem1  33540  poimirlem2  33541  poimirlem7  33546  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem24  33563  poimirlem31  33570  poimirlem32  33571  fdc  33671  mettrifi  33683  caushft  33687  cntotbnd  33725  mzpsubmpt  37623  lzenom  37650  diophun  37654  eqrabdioph  37658  irrapxlem2  37704  irrapxlem3  37705  pellexlem6  37715  pell1234qrreccl  37735  pellfund14  37779  rmxyneg  37802  rmxyadd  37803  rmxp1  37814  rmxm1  37816  rmym1  37817  rmxluc  37818  rmyluc  37819  rmyluc2  37820  rmxdbl  37821  rmydbl  37822  congadd  37850  congsub  37854  congabseq  37858  acongrep  37864  acongeq  37867  jm2.18  37872  jm2.19lem1  37873  jm2.19lem2  37874  jm2.19lem3  37875  jm2.22  37879  jm2.23  37880  jm2.20nn  37881  jm2.25  37883  jm2.26lem3  37885  jm2.27c  37891  nzss  38833  hashnzfz  38836  hashnzfz2  38837  hashnzfzclim  38838  uzmptshftfval  38862  sineq0ALT  39487  fzisoeu  39828  fperiodmul  39832  monoord2xrv  40027  fmul01lt1lem2  40135  sumnnodd  40180  dvdsn1add  40472  dvnmul  40476  dvnprodlem1  40479  stoweidlem11  40546  stoweidlem26  40561  dirkertrigeqlem1  40633  dirkertrigeqlem2  40634  dirkertrigeqlem3  40635  dirkertrigeq  40636  dirkeritg  40637  fourierdlem26  40668  fourierdlem48  40689  fourierdlem49  40690  fourierdlem79  40720  fourierdlem91  40732  fourierdlem103  40744  fourierdlem104  40745  fouriersw  40766  etransclem1  40770  etransclem4  40773  etransclem8  40777  etransclem9  40778  etransclem15  40784  etransclem17  40786  etransclem18  40787  etransclem20  40789  etransclem21  40790  etransclem22  40791  etransclem23  40792  etransclem24  40793  etransclem25  40794  etransclem35  40804  etransclem38  40807  etransclem41  40810  etransclem44  40813  etransclem45  40814  etransclem46  40815  etransclem47  40816  etransclem48  40817  2elfz2melfz  41653  fsumsplitsndif  41668  iccpartgtprec  41681  fargshiftf1  41702  fargshiftfo  41703  pfxfv  41724  ccatpfx  41734  pfxccatin12lem2  41749  pwdif  41826  mod42tp1mod8  41844  sfprmdvdsmersenne  41845  lighneallem3  41849  lighneallem4b  41851  modexp2m1d  41854  dfodd6  41875  onego  41884  m1expoddALTV  41886  zofldiv2ALTV  41899  oddflALTV  41900  oexpnegALTV  41913  omoeALTV  41921  omeoALTV  41922  epoo  41937  emoo  41938  epee  41939  emee  41940  evensumeven  41941  evenltle  41951  even3prm2  41953  mogoldbblem  41954  sbgoldbst  41991  sbgoldbaltlem2  41993  sgoldbeven3prm  41996  nnsum3primesprm  42003  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbndlem2  42019  bgoldbtbndlem4  42021  bgoldbtbnd  42022  2zrngamnd  42266  2zrngacmnd  42267  2zrngagrp  42268  2zrngALT  42273  2zrngnmlid  42274  2zrngnmlid2  42276  ztprmneprm  42450  altgsumbcALT  42456  fldivmod  42638  m1modmmod  42641  zofldiv2  42650  fllogbd  42679  nnpw2blen  42699  blen1b  42707  blennngt2o2  42711  blennn0e2  42713  dig2nn1st  42724  dignn0flhalflem1  42734
  Copyright terms: Public domain W3C validator