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

Theorem zcnd 11745
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 11744 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 10350 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2158  cc 10216  cz 11639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-resscn 10275
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-rex 3101  df-rab 3104  df-v 3392  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4627  df-br 4841  df-iota 6061  df-fv 6106  df-ov 6874  df-neg 10551  df-z 11640
This theorem is referenced by:  zsupss  11992  rpnnen1lem5  12033  fzm1  12639  fzrevral  12644  fzshftral  12647  nn0disj  12675  predfz  12684  fzoss2  12716  fzo0addelr  12743  fzosubel  12747  fzosubel3  12749  fzocatel  12752  fzosplitsnm1  12763  elfzom1elp1fzo1  12788  2tnp1ge0ge0  12850  quoremz  12874  intfrac2  12877  intfracq  12878  flpmodeq  12893  moddiffl  12901  modmul1  12943  modmul12d  12944  modfzo0difsn  12962  modsumfzodifsn  12963  addmodlteq  12965  uzrdgxfr  12986  fzen2  12988  monoord2  13051  seqf1olem1  13059  seqf1olem2  13060  seqz  13068  expaddzlem  13122  modexp  13218  sqoddm1div8  13247  bcm1k  13318  bcp1nk  13320  bcval5  13321  bcpasc  13324  hashfz  13427  hashfzo  13429  hashfzp1  13431  hashbclem  13449  seqcoll  13461  ccatval3  13572  ccatlid  13579  ccatass  13581  ccatalpha  13586  swrd0val  13640  swrdfv0  13644  swrdid  13648  swrd0fv  13659  swrdfv2  13666  swrds1  13671  ccatswrd  13676  swrdswrd0  13682  spllen  13725  splfv1  13726  splfv2a  13727  revccat  13735  revrev  13736  cshwidxmod  13769  cshwidxm1  13773  cshweqrep  13787  2cshwcshw  13791  cshimadifsn0  13796  swrds2m  13906  seqshft  14044  fzomaxdif  14302  climshft2  14532  iserex  14606  isercoll2  14618  serf0  14630  iseraltlem2  14632  iseraltlem3  14633  iseralt  14634  sumrblem  14661  fsumm1  14699  fsumsplitsnun  14703  fsumsplitsnunOLD  14705  fsump1  14706  fsumshftm  14731  fsumrev2  14732  telfsumo  14752  fsumparts  14756  binomlem  14779  isumshft  14789  isumsplit  14790  isum1p  14791  arisum  14810  cvgrat  14832  mertenslem1  14833  ntrivcvg  14846  ntrivcvgtail  14849  prodrblem  14876  fprodser  14896  fprodm1  14914  fprodp1  14916  fprodrev  14924  fprodmodd  14944  fallfacval3  14959  fallfacfwd  14983  0fallfac  14984  binomfallfaclem2  14987  fallfacval4  14990  fsumkthpow  15003  eirrlem  15148  sqrt2irrlem  15193  sqrt2irrlemOLD  15194  dvds2ln  15233  dvdsadd2b  15247  fsumdvds  15249  fzocongeq  15265  addmodlteqALT  15266  dvdsexp  15268  dvdsmod  15269  3dvds  15271  fprodfvdvdsd  15274  odd2np1  15281  oddm1even  15283  oexpneg  15285  mod2eq1n2dvds  15287  mulsucdiv2z  15293  zob  15299  ltoddhalfle  15301  sumodd  15327  pwp1fsum  15330  divalglem0  15332  divalglem4  15335  divalglem8  15339  divalgb  15343  divalgmod  15345  modremain  15347  flodddiv4  15352  bitsp1  15368  bitsfzo  15372  bitsmod  15373  bitsinv1lem  15378  bitsf1  15383  sadaddlem  15403  bitsres  15410  bitsuz  15411  bitsshft  15412  smumullem  15429  modgcd  15468  bezoutlem1  15471  bezoutlem2  15472  bezoutlem3  15473  bezoutlem4  15474  dvdsmulgcd  15489  rplpwr  15491  lcmid  15537  absprodnn  15546  mulgcddvds  15583  divgcdcoprm0  15593  cncongr1  15595  cncongr2  15596  rpexp  15645  qmuldeneqnum  15668  numdensq  15675  qden1elz  15678  hashdvds  15693  phiprm  15695  eulerthlem2  15700  fermltl  15702  prmdiv  15703  prmdiveq  15704  hashgcdlem  15706  odzdvds  15713  vfermltlALT  15720  modprm0  15723  modprmn0modprm0  15725  pythagtriplem6  15739  pythagtriplem7  15740  pythagtriplem15  15747  pcpremul  15761  pceulem  15763  pczpre  15765  pcdiv  15770  pcqmul  15771  pcqdiv  15775  pcexp  15777  pcaddlem  15805  pcadd  15806  fldivp1  15814  pcfac  15816  pcbc  15817  prmpwdvds  15821  prmreclem4  15836  4sqlem5  15859  4sqlem8  15862  4sqlem9  15863  4sqlem10  15864  4sqlem11  15872  4sqlem14  15875  4sqlem16  15877  4sqlem17  15878  vdwapun  15891  vdwnnlem2  15913  prmop1  15955  prmdvdsprmo  15959  prmgaplem7  15974  prmlem0  16020  mulgsubcl  17756  mulgdirlem  17771  mulgdir  17772  mulgass  17777  mulgmodid  17779  mulgsubdir  17780  psgnunilem5  18111  psgnunilem2  18112  psgnunilem4  18114  m1expaddsub  18115  psgnuni  18116  odnncl  18161  odmulg  18170  odbezout  18172  sylow1lem1  18210  sylow2alem2  18230  efgsres  18348  efgredleme  18353  efgredlemc  18355  odadd1  18448  odadd2  18449  cyggeninv  18482  gsummptshft  18533  ablfacrp  18663  pgpfac1lem3  18674  srgbinomlem3  18740  srgbinomlem4  18741  zringmulg  20030  zringlpirlem1  20036  zringlpirlem3  20038  prmirredlem  20045  zndvds0  20102  znf1o  20103  znunit  20115  cayhamlem1  20880  tgpmulg  22106  zdis  22828  uniioombllem3  23562  mbfi1fseqlem4  23695  dvexp3  23951  aareccl  24291  aalioulem1  24297  geolim3  24304  aaliou3lem2  24308  aaliou3lem6  24313  ulmshft  24354  sineq0  24484  efif1olem2  24500  igamz  24984  wilthlem1  25004  wilthlem2  25005  basellem3  25019  mumul  25117  musum  25127  musumsum  25128  muinv  25129  ppiub  25139  chtub  25147  logfac2  25152  chpchtsum  25154  dchrptlem1  25199  pcbcctr  25211  bcmono  25212  bposlem5  25223  bposlem6  25224  lgslem1  25232  lgsval2lem  25242  lgsval4a  25254  lgsneg  25256  lgsneg1  25257  lgsmod  25258  lgsdirprm  25266  lgsdir  25267  lgsdilem2  25268  lgsdi  25269  lgsne0  25270  lgsabs1  25271  lgssq  25272  lgssq2  25273  lgsmulsqcoprm  25278  lgsdirnn0  25279  lgsdinn0  25280  lgsqrlem1  25281  gausslemma2dlem1a  25300  gausslemma2dlem1  25301  gausslemma2dlem4  25304  gausslemma2dlem5a  25305  gausslemma2dlem5  25306  gausslemma2dlem6  25307  gausslemma2d  25309  lgseisenlem1  25310  lgseisenlem2  25311  lgseisenlem3  25312  lgseisenlem4  25313  lgsquadlem1  25315  lgsquad2lem1  25319  lgsquad3  25322  2lgslem1b  25327  2lgsoddprmlem2  25344  2sqlem3  25355  2sqlem4  25356  2sqlem8a  25360  2sqlem8  25361  2sqlem11  25364  2sqblem  25366  dchrisumlem1  25388  dchrmusum2  25393  dchrvmasumlem1  25394  dchrvmasum2lem  25395  mudivsum  25429  mulogsum  25431  mulog2sumlem2  25434  selberglem1  25444  selberglem3  25446  selberg  25447  pntpbnd2  25486  pntlemf  25504  padicabvcxp  25531  axlowdimlem14  26045  axlowdimlem16  26047  pthdadjvtx  26850  crctcshwlkn0lem4  26930  crctcshwlkn0lem5  26931  crctcshlem4  26937  crctcsh  26941  clwwlkccatlem  27128  clwwisshclwws  27154  eucrctshift  27412  znsqcld  29836  fzspl  29874  bcm1n  29878  numdenneg  29887  divnumden2  29888  ltesubnnd  29892  2sqn0  29968  2sqmod  29970  archiabllem1  30069  archiabllem2c  30071  zrhnm  30335  cnzh  30336  rezh  30337  qqhval2lem  30347  qqhghm  30354  qqhrhm  30355  qqhnm  30356  ballotlemfc0  30876  ballotlemfcc  30877  ballotlemic  30890  ballotlem1c  30891  ballotlemsgt1  30894  ballotlemsdom  30895  ballotlemsel1i  30896  ballotlemsf1o  30897  ballotlemsima  30899  ballotlemfrceq  30912  ballotlemfrcn0  30913  ballotlem1ri  30918  signsplypnf  30949  itgexpif  31006  fsum2dsub  31007  breprexplemc  31032  vtsprod  31039  circlemeth  31040  divcnvlin  31937  fwddifnp1  32590  knoppndvlem2  32818  knoppndvlem7  32823  knoppndvlem14  32830  knoppndvlem16  32832  ltflcei  33707  poimirlem1  33720  poimirlem2  33721  poimirlem7  33726  poimirlem16  33735  poimirlem17  33736  poimirlem19  33738  poimirlem20  33739  poimirlem24  33743  poimirlem31  33750  poimirlem32  33751  fdc  33849  mettrifi  33861  caushft  33865  cntotbnd  33903  mzpsubmpt  37805  lzenom  37832  diophun  37836  eqrabdioph  37840  irrapxlem2  37886  irrapxlem3  37887  pellexlem6  37897  pell1234qrreccl  37917  pellfund14  37961  rmxyneg  37983  rmxyadd  37984  rmxp1  37995  rmxm1  37997  rmym1  37998  rmxluc  37999  rmyluc  38000  rmyluc2  38001  rmxdbl  38002  rmydbl  38003  congadd  38031  congsub  38035  congabseq  38039  acongrep  38045  acongeq  38048  jm2.18  38053  jm2.19lem1  38054  jm2.19lem2  38055  jm2.19lem3  38056  jm2.22  38060  jm2.23  38061  jm2.20nn  38062  jm2.25  38064  jm2.26lem3  38066  jm2.27c  38072  nzss  39013  hashnzfz  39016  hashnzfz2  39017  hashnzfzclim  39018  uzmptshftfval  39042  sineq0ALT  39664  fzisoeu  39992  fperiodmul  39996  monoord2xrv  40190  fmul01lt1lem2  40294  sumnnodd  40339  dvdsn1add  40631  dvnmul  40635  dvnprodlem1  40638  stoweidlem11  40704  stoweidlem26  40719  dirkertrigeqlem1  40791  dirkertrigeqlem2  40792  dirkertrigeqlem3  40793  dirkertrigeq  40794  dirkeritg  40795  fourierdlem26  40826  fourierdlem48  40847  fourierdlem49  40848  fourierdlem79  40878  fourierdlem91  40890  fourierdlem103  40902  fourierdlem104  40903  fouriersw  40924  etransclem1  40928  etransclem4  40931  etransclem8  40935  etransclem9  40936  etransclem15  40942  etransclem17  40944  etransclem18  40945  etransclem20  40947  etransclem21  40948  etransclem22  40949  etransclem23  40950  etransclem24  40951  etransclem25  40952  etransclem35  40962  etransclem38  40965  etransclem41  40968  etransclem44  40971  etransclem45  40972  etransclem46  40973  etransclem47  40974  etransclem48  40975  2elfz2melfz  41900  fsumsplitsndif  41915  iccpartgtprec  41928  fargshiftf1  41949  fargshiftfo  41950  pfxfv  41971  ccatpfx  41981  pfxccatin12lem2  41996  pwdif  42073  mod42tp1mod8  42091  sfprmdvdsmersenne  42092  lighneallem3  42096  lighneallem4b  42098  modexp2m1d  42101  dfodd6  42122  onego  42131  m1expoddALTV  42133  zofldiv2ALTV  42146  oddflALTV  42147  oexpnegALTV  42160  omoeALTV  42168  omeoALTV  42169  epoo  42184  emoo  42185  epee  42186  emee  42187  evensumeven  42188  evenltle  42198  even3prm2  42200  mogoldbblem  42201  sbgoldbst  42238  sbgoldbaltlem2  42240  sgoldbeven3prm  42243  nnsum3primesprm  42250  nnsum4primesodd  42256  nnsum4primesoddALTV  42257  nnsum4primeseven  42260  nnsum4primesevenALTV  42261  bgoldbtbndlem2  42266  bgoldbtbndlem4  42268  bgoldbtbnd  42269  2zrngamnd  42506  2zrngacmnd  42507  2zrngagrp  42508  2zrngALT  42513  2zrngnmlid  42514  2zrngnmlid2  42516  ztprmneprm  42690  altgsumbcALT  42696  fldivmod  42878  m1modmmod  42881  zofldiv2  42890  fllogbd  42919  nnpw2blen  42939  blen1b  42947  blennngt2o2  42951  blennn0e2  42953  dig2nn1st  42964  dignn0flhalflem1  42974
  Copyright terms: Public domain W3C validator