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

Theorem zcnd 12542
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 12541 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 11117 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cc 10983  cz 12433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-resscn 11042
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-iota 6444  df-fv 6500  df-ov 7353  df-neg 11322  df-z 12434
This theorem is referenced by:  zsupss  12792  rpnnen1lem5  12836  fzm1  13451  fzrevral  13456  fzshftral  13459  nn0disj  13487  predfz  13496  fzoss2  13530  fzo0addelr  13557  fzosubel  13561  fzosubel3  13563  fzocatel  13566  fzosplitsnm1  13577  elfzom1elp1fzo1  13602  2tnp1ge0ge0  13664  quoremz  13690  intfrac2  13693  intfracq  13694  flpmodeq  13709  moddiffl  13717  modmul1  13759  modmul12d  13760  modfzo0difsn  13778  modsumfzodifsn  13779  addmodlteq  13781  uzrdgxfr  13802  fzen2  13804  monoord2  13869  seqf1olem1  13877  seqf1olem2  13878  seqz  13886  expaddzlem  13941  znsqcld  13995  modexp  14068  sqoddm1div8  14073  bcm1k  14144  bcp1nk  14146  bcval5  14147  bcpasc  14150  hashfz  14256  hashfzo  14258  hashfzp1  14260  hashbclem  14278  seqcoll  14292  ccatval3  14396  ccatlid  14403  ccatass  14405  ccatalpha  14410  swrdfv0  14470  swrdfv2  14482  swrds1  14487  ccatswrd  14489  pfxfv  14503  ccatpfx  14522  swrdpfx  14528  pfxccatin12lem2  14552  spllen  14575  revccat  14587  revrev  14588  cshwidxmod  14624  cshwidxm1  14628  cshweqrep  14642  2cshwcshw  14647  cshimadifsn0  14652  swrds2m  14763  seqshft  14905  fzomaxdif  15164  climshft2  15400  iserex  15477  isercoll2  15489  serf0  15501  iseraltlem2  15503  iseraltlem3  15504  iseralt  15505  sumrblem  15532  fsumm1  15572  fsumsplitsnun  15576  fsump1  15577  fsumshftm  15602  fsumrev2  15603  telfsumo  15623  fsumparts  15627  binomlem  15650  isumshft  15660  isumsplit  15661  isum1p  15662  arisum  15681  pwdif  15689  cvgrat  15704  mertenslem1  15705  ntrivcvg  15718  ntrivcvgtail  15721  prodrblem  15748  fprodser  15768  fprodm1  15786  fprodp1  15788  fprodrev  15796  fprodmodd  15816  fallfacval3  15831  fallfacfwd  15855  0fallfac  15856  binomfallfaclem2  15859  fallfacval4  15862  fsumkthpow  15875  eirrlem  16022  sqrt2irrlem  16066  dvds2ln  16107  dvdsadd2b  16124  fsumdvds  16126  fzocongeq  16142  addmodlteqALT  16143  dvdsexp  16146  dvdsmod  16147  3dvds  16149  fprodfvdvdsd  16152  odd2np1  16159  oddm1even  16161  oexpneg  16163  mod2eq1n2dvds  16165  mulsucdiv2z  16171  zob  16177  ltoddhalfle  16179  sumodd  16206  pwp1fsum  16209  divalglem0  16211  divalglem4  16214  divalglem8  16218  divalgb  16222  divalgmod  16224  modremain  16226  flodddiv4  16231  bitsp1  16247  bitsfzo  16251  bitsmod  16252  bitsinv1lem  16257  bitsf1  16262  sadaddlem  16282  bitsres  16289  bitsuz  16290  bitsshft  16291  smumullem  16308  modgcd  16349  gcdmultipled  16351  dvdsgcdidd  16354  bezoutlem1  16356  bezoutlem2  16357  bezoutlem3  16358  bezoutlem4  16359  dvdsmulgcd  16372  rplpwr  16374  lcmid  16421  absprodnn  16430  mulgcddvds  16467  divgcdcoprm0  16477  cncongr1  16479  cncongr2  16480  rpexp  16534  qmuldeneqnum  16558  numdensq  16565  qden1elz  16568  hashdvds  16583  phiprm  16585  eulerthlem2  16590  fermltl  16592  prmdiv  16593  prmdiveq  16594  hashgcdlem  16596  odzdvds  16603  vfermltlALT  16610  modprm0  16613  modprmn0modprm0  16615  pythagtriplem6  16629  pythagtriplem7  16630  pythagtriplem15  16637  pcpremul  16651  pceulem  16653  pczpre  16655  pcdiv  16660  pcqmul  16661  pcqdiv  16665  pcexp  16667  pcaddlem  16696  pcadd  16697  fldivp1  16705  pcfac  16707  pcbc  16708  prmpwdvds  16712  prmreclem4  16727  4sqlem5  16750  4sqlem8  16753  4sqlem9  16754  4sqlem10  16755  4sqlem11  16763  4sqlem14  16766  4sqlem16  16768  4sqlem17  16769  vdwapun  16782  vdwnnlem2  16804  prmop1  16846  prmdvdsprmo  16850  prmgaplem7  16865  prmlem0  16914  mulgsubcl  18825  mulgdirlem  18842  mulgdir  18843  mulgass  18848  mulgmodid  18850  mulgsubdir  18851  psgnunilem5  19211  psgnunilem2  19212  psgnunilem4  19214  m1expaddsub  19215  psgnuni  19216  odnncl  19262  odmulg  19273  odbezout  19275  sylow1lem1  19315  sylow2alem2  19335  efgsres  19455  efgredleme  19460  efgredlemc  19462  odadd1  19561  odadd2  19562  cyggeninv  19595  gsummptshft  19648  ablfacrp  19780  pgpfac1lem3  19791  fincygsubgodd  19826  srgbinomlem3  19889  srgbinomlem4  19890  zringmulg  20806  zringlpirlem1  20812  zringlpirlem3  20814  prmirredlem  20822  zndvds0  20886  znf1o  20887  znunit  20899  cayhamlem1  22143  tgpmulg  23372  zdis  24107  uniioombllem3  24877  mbfi1fseqlem4  25011  dvexp3  25270  aareccl  25614  aalioulem1  25620  geolim3  25627  aaliou3lem2  25631  aaliou3lem6  25636  ulmshft  25677  sineq0  25808  efif1olem2  25827  igamz  26325  wilthlem1  26345  wilthlem2  26346  basellem3  26360  mumul  26458  musum  26468  musumsum  26469  muinv  26470  ppiub  26480  chtub  26488  logfac2  26493  chpchtsum  26495  dchrptlem1  26540  pcbcctr  26552  bcmono  26553  bposlem5  26564  bposlem6  26565  lgslem1  26573  lgsval2lem  26583  lgsval4a  26595  lgsneg  26597  lgsneg1  26598  lgsmod  26599  lgsdirprm  26607  lgsdir  26608  lgsdilem2  26609  lgsdi  26610  lgsne0  26611  lgsabs1  26612  lgssq  26613  lgssq2  26614  lgsmulsqcoprm  26619  lgsdirnn0  26620  lgsdinn0  26621  lgsqrlem1  26622  gausslemma2dlem1a  26641  gausslemma2dlem1  26642  gausslemma2dlem4  26645  gausslemma2dlem5a  26646  gausslemma2dlem5  26647  gausslemma2dlem6  26648  gausslemma2d  26650  lgseisenlem1  26651  lgseisenlem2  26652  lgseisenlem3  26653  lgseisenlem4  26654  lgsquadlem1  26656  lgsquad2lem1  26660  lgsquad3  26663  2lgslem1b  26668  2lgsoddprmlem2  26685  2sqlem3  26696  2sqlem4  26697  2sqlem8a  26701  2sqlem8  26702  2sqlem11  26705  2sqblem  26707  2sqn0  26710  2sqmod  26712  dchrisumlem1  26765  dchrmusum2  26770  dchrvmasumlem1  26771  dchrvmasum2lem  26772  mudivsum  26806  mulogsum  26808  mulog2sumlem2  26811  selberglem1  26821  selberglem3  26823  selberg  26824  pntpbnd2  26863  pntlemf  26881  padicabvcxp  26908  axlowdimlem14  27709  axlowdimlem16  27711  pthdadjvtx  28483  crctcshwlkn0lem4  28563  crctcshwlkn0lem5  28564  crctcshlem4  28570  crctcsh  28574  clwwlkccatlem  28738  clwwisshclwws  28764  eucrctshift  28992  fzm1ne1  31493  fzspl  31494  bcm1n  31499  fzom1ne1  31505  dvdszzq  31512  prmdvdsbc  31513  numdenneg  31514  divnumden2  31515  ltesubnnd  31519  ccatf1  31606  swrdrn3  31610  swrdf1  31611  cshwrnid  31616  cycpmco2lem3  31778  cycpmco2lem4  31779  cycpmco2lem5  31780  cycpmco2lem6  31781  cycpmco2  31783  archiabllem1  31830  archiabllem2c  31832  fermltlchr  31954  znfermltl  31955  zrhnm  32330  cnzh  32331  rezh  32332  qqhval2lem  32342  qqhghm  32349  qqhrhm  32350  qqhnm  32351  ballotlemfc0  32872  ballotlemfcc  32873  ballotlemic  32886  ballotlem1c  32887  ballotlemsgt1  32890  ballotlemsdom  32891  ballotlemsel1i  32892  ballotlemsf1o  32893  ballotlemsima  32895  ballotlemfrceq  32908  ballotlemfrcn0  32909  ballotlem1ri  32914  signsplypnf  32942  itgexpif  32999  fsum2dsub  33000  breprexplemc  33025  vtsprod  33032  circlemeth  33033  revpfxsfxrev  33489  swrdrevpfx  33490  revwlk  33498  swrdwlk  33500  divcnvlin  34099  fwddifnp1  34681  knoppndvlem2  34907  knoppndvlem7  34912  knoppndvlem14  34919  knoppndvlem16  34921  ltflcei  35997  poimirlem1  36010  poimirlem2  36011  poimirlem7  36016  poimirlem16  36025  poimirlem17  36026  poimirlem19  36028  poimirlem20  36029  poimirlem24  36033  poimirlem31  36040  poimirlem32  36041  fdc  36135  mettrifi  36147  caushft  36151  cntotbnd  36186  fzsplitnd  40371  lcmineqlem6  40422  lcmineqlem18  40434  aks4d1p1p1  40451  aks4d1p8d3  40474  aks4d1p8  40475  sticksstones10  40494  sticksstones12a  40496  sticksstones12  40497  metakunt12  40519  metakunt15  40522  metakunt16  40523  metakunt28  40535  oexpreposd  40709  exp11d  40713  numdenexp  40725  dvdsexpb  40730  mzpsubmpt  40968  lzenom  40995  diophun  40998  eqrabdioph  41002  irrapxlem2  41048  irrapxlem3  41049  pellexlem6  41059  pell1234qrreccl  41079  pellfund14  41123  rmxyneg  41146  rmxyadd  41147  rmxp1  41158  rmxm1  41160  rmym1  41161  rmxluc  41162  rmyluc  41163  rmyluc2  41164  rmxdbl  41165  rmydbl  41166  congadd  41192  congsub  41196  congabseq  41200  acongrep  41206  acongeq  41209  jm2.18  41214  jm2.19lem1  41215  jm2.19lem2  41216  jm2.19lem3  41217  jm2.22  41221  jm2.23  41222  jm2.20nn  41223  jm2.25  41225  jm2.26lem3  41227  jm2.27c  41233  nzss  42398  hashnzfz  42401  hashnzfz2  42402  hashnzfzclim  42403  uzmptshftfval  42427  sineq0ALT  43020  fzisoeu  43329  fperiodmul  43333  monoord2xrv  43514  fmul01lt1lem2  43617  sumnnodd  43662  dvdsn1add  43971  dvnmul  43975  dvnprodlem1  43978  stoweidlem11  44043  stoweidlem26  44058  dirkertrigeqlem1  44130  dirkertrigeqlem2  44131  dirkertrigeqlem3  44132  dirkertrigeq  44133  dirkeritg  44134  fourierdlem26  44165  fourierdlem48  44186  fourierdlem49  44187  fourierdlem79  44217  fourierdlem91  44229  fourierdlem103  44241  fourierdlem104  44242  fouriersw  44263  etransclem1  44267  etransclem4  44270  etransclem8  44274  etransclem9  44275  etransclem15  44281  etransclem17  44283  etransclem18  44284  etransclem20  44286  etransclem21  44287  etransclem22  44288  etransclem23  44289  etransclem24  44290  etransclem25  44291  etransclem35  44301  etransclem38  44304  etransclem41  44307  etransclem44  44310  etransclem45  44311  etransclem46  44312  etransclem47  44313  etransclem48  44314  2elfz2melfz  45341  fsumsplitsndif  45356  iccpartgtprec  45403  fargshiftf1  45424  fargshiftfo  45425  mod42tp1mod8  45585  sfprmdvdsmersenne  45586  lighneallem3  45590  lighneallem4b  45592  modexp2m1d  45595  dfodd6  45620  onego  45629  m1expoddALTV  45631  zofldiv2ALTV  45645  oddflALTV  45646  oexpnegALTV  45660  omoeALTV  45668  omeoALTV  45669  epoo  45686  emoo  45687  epee  45688  emee  45689  evensumeven  45690  evenltle  45700  even3prm2  45702  mogoldbblem  45703  fppr2odd  45714  fpprwppr  45722  fpprwpprb  45723  sbgoldbst  45761  sbgoldbaltlem2  45763  sgoldbeven3prm  45766  nnsum3primesprm  45773  nnsum4primesodd  45779  nnsum4primesoddALTV  45780  nnsum4primeseven  45783  nnsum4primesevenALTV  45784  bgoldbtbndlem2  45789  bgoldbtbndlem4  45791  bgoldbtbnd  45792  2zrngamnd  46030  2zrngacmnd  46031  2zrngagrp  46032  2zrngALT  46037  2zrngnmlid  46038  2zrngnmlid2  46040  ztprmneprm  46214  altgsumbcALT  46220  fldivmod  46395  m1modmmod  46398  zofldiv2  46408  fllogbd  46437  nnpw2blen  46457  blen1b  46465  blennngt2o2  46469  blennn0e2  46471  dig2nn1st  46482  dignn0flhalflem1  46492
  Copyright terms: Public domain W3C validator