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

Theorem zcnd 12067
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 12066 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 10647 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  cc 10513  cz 11960
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-resscn 10572
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-br 5043  df-iota 6290  df-fv 6339  df-ov 7136  df-neg 10851  df-z 11961
This theorem is referenced by:  zsupss  12316  rpnnen1lem5  12359  fzm1  12971  fzrevral  12976  fzshftral  12979  nn0disj  13007  predfz  13016  fzoss2  13049  fzo0addelr  13076  fzosubel  13080  fzosubel3  13082  fzocatel  13085  fzosplitsnm1  13096  elfzom1elp1fzo1  13121  2tnp1ge0ge0  13183  quoremz  13207  intfrac2  13210  intfracq  13211  flpmodeq  13226  moddiffl  13234  modmul1  13276  modmul12d  13277  modfzo0difsn  13295  modsumfzodifsn  13296  addmodlteq  13298  uzrdgxfr  13319  fzen2  13321  monoord2  13386  seqf1olem1  13394  seqf1olem2  13395  seqz  13403  expaddzlem  13457  znsqcld  13511  modexp  13584  sqoddm1div8  13589  bcm1k  13660  bcp1nk  13662  bcval5  13663  bcpasc  13666  hashfz  13773  hashfzo  13775  hashfzp1  13777  hashbclem  13795  seqcoll  13807  ccatval3  13913  ccatlid  13920  ccatass  13922  ccatalpha  13927  swrdfv0  13991  swrdfv2  14003  swrds1  14008  ccatswrd  14010  pfxfv  14024  ccatpfx  14043  swrdpfx  14049  pfxccatin12lem2  14073  spllen  14096  revccat  14108  revrev  14109  cshwidxmod  14145  cshwidxm1  14149  cshweqrep  14163  2cshwcshw  14167  cshimadifsn0  14172  swrds2m  14283  seqshft  14424  fzomaxdif  14683  climshft2  14919  iserex  14993  isercoll2  15005  serf0  15017  iseraltlem2  15019  iseraltlem3  15020  iseralt  15021  sumrblem  15048  fsumm1  15086  fsumsplitsnun  15090  fsump1  15091  fsumshftm  15116  fsumrev2  15117  telfsumo  15137  fsumparts  15141  binomlem  15164  isumshft  15174  isumsplit  15175  isum1p  15176  arisum  15195  pwdif  15203  cvgrat  15219  mertenslem1  15220  ntrivcvg  15233  ntrivcvgtail  15236  prodrblem  15263  fprodser  15283  fprodm1  15301  fprodp1  15303  fprodrev  15311  fprodmodd  15331  fallfacval3  15346  fallfacfwd  15370  0fallfac  15371  binomfallfaclem2  15374  fallfacval4  15377  fsumkthpow  15390  eirrlem  15537  sqrt2irrlem  15581  dvds2ln  15622  dvdsadd2b  15636  fsumdvds  15638  fzocongeq  15654  addmodlteqALT  15655  dvdsexp  15657  dvdsmod  15658  3dvds  15660  fprodfvdvdsd  15663  odd2np1  15670  oddm1even  15672  oexpneg  15674  mod2eq1n2dvds  15676  mulsucdiv2z  15682  zob  15688  ltoddhalfle  15690  sumodd  15717  pwp1fsum  15720  divalglem0  15722  divalglem4  15725  divalglem8  15729  divalgb  15733  divalgmod  15735  modremain  15737  flodddiv4  15742  bitsp1  15758  bitsfzo  15762  bitsmod  15763  bitsinv1lem  15768  bitsf1  15773  sadaddlem  15793  bitsres  15800  bitsuz  15801  bitsshft  15802  smumullem  15819  modgcd  15858  gcdmultipled  15860  dvdsgcdidd  15863  bezoutlem1  15865  bezoutlem2  15866  bezoutlem3  15867  bezoutlem4  15868  dvdsmulgcd  15883  rplpwr  15885  lcmid  15931  absprodnn  15940  mulgcddvds  15977  divgcdcoprm0  15987  cncongr1  15989  cncongr2  15990  rpexp  16042  qmuldeneqnum  16065  numdensq  16072  qden1elz  16075  hashdvds  16090  phiprm  16092  eulerthlem2  16097  fermltl  16099  prmdiv  16100  prmdiveq  16101  hashgcdlem  16103  odzdvds  16110  vfermltlALT  16117  modprm0  16120  modprmn0modprm0  16122  pythagtriplem6  16136  pythagtriplem7  16137  pythagtriplem15  16144  pcpremul  16158  pceulem  16160  pczpre  16162  pcdiv  16167  pcqmul  16168  pcqdiv  16172  pcexp  16174  pcaddlem  16202  pcadd  16203  fldivp1  16211  pcfac  16213  pcbc  16214  prmpwdvds  16218  prmreclem4  16233  4sqlem5  16256  4sqlem8  16259  4sqlem9  16260  4sqlem10  16261  4sqlem11  16269  4sqlem14  16272  4sqlem16  16274  4sqlem17  16275  vdwapun  16288  vdwnnlem2  16310  prmop1  16352  prmdvdsprmo  16356  prmgaplem7  16371  prmlem0  16418  mulgsubcl  18221  mulgdirlem  18237  mulgdir  18238  mulgass  18243  mulgmodid  18245  mulgsubdir  18246  psgnunilem5  18601  psgnunilem2  18602  psgnunilem4  18604  m1expaddsub  18605  psgnuni  18606  odnncl  18652  odmulg  18662  odbezout  18664  sylow1lem1  18702  sylow2alem2  18722  efgsres  18843  efgredleme  18848  efgredlemc  18850  odadd1  18947  odadd2  18948  cyggeninv  18981  gsummptshft  19035  ablfacrp  19167  pgpfac1lem3  19178  fincygsubgodd  19213  srgbinomlem3  19271  srgbinomlem4  19272  zringmulg  20601  zringlpirlem1  20607  zringlpirlem3  20609  prmirredlem  20616  zndvds0  20673  znf1o  20674  znunit  20686  cayhamlem1  21450  tgpmulg  22677  zdis  23400  uniioombllem3  24168  mbfi1fseqlem4  24301  dvexp3  24560  aareccl  24901  aalioulem1  24907  geolim3  24914  aaliou3lem2  24918  aaliou3lem6  24923  ulmshft  24964  sineq0  25095  efif1olem2  25114  igamz  25612  wilthlem1  25632  wilthlem2  25633  basellem3  25647  mumul  25745  musum  25755  musumsum  25756  muinv  25757  ppiub  25767  chtub  25775  logfac2  25780  chpchtsum  25782  dchrptlem1  25827  pcbcctr  25839  bcmono  25840  bposlem5  25851  bposlem6  25852  lgslem1  25860  lgsval2lem  25870  lgsval4a  25882  lgsneg  25884  lgsneg1  25885  lgsmod  25886  lgsdirprm  25894  lgsdir  25895  lgsdilem2  25896  lgsdi  25897  lgsne0  25898  lgsabs1  25899  lgssq  25900  lgssq2  25901  lgsmulsqcoprm  25906  lgsdirnn0  25907  lgsdinn0  25908  lgsqrlem1  25909  gausslemma2dlem1a  25928  gausslemma2dlem1  25929  gausslemma2dlem4  25932  gausslemma2dlem5a  25933  gausslemma2dlem5  25934  gausslemma2dlem6  25935  gausslemma2d  25937  lgseisenlem1  25938  lgseisenlem2  25939  lgseisenlem3  25940  lgseisenlem4  25941  lgsquadlem1  25943  lgsquad2lem1  25947  lgsquad3  25950  2lgslem1b  25955  2lgsoddprmlem2  25972  2sqlem3  25983  2sqlem4  25984  2sqlem8a  25988  2sqlem8  25989  2sqlem11  25992  2sqblem  25994  2sqn0  25997  2sqmod  25999  dchrisumlem1  26052  dchrmusum2  26057  dchrvmasumlem1  26058  dchrvmasum2lem  26059  mudivsum  26093  mulogsum  26095  mulog2sumlem2  26098  selberglem1  26108  selberglem3  26110  selberg  26111  pntpbnd2  26150  pntlemf  26168  padicabvcxp  26195  axlowdimlem14  26728  axlowdimlem16  26730  pthdadjvtx  27498  crctcshwlkn0lem4  27578  crctcshwlkn0lem5  27579  crctcshlem4  27585  crctcsh  27589  clwwlkccatlem  27753  clwwisshclwws  27779  eucrctshift  28007  fzm1ne1  30499  fzspl  30500  bcm1n  30505  fzom1ne1  30511  dvdszzq  30518  prmdvdsbc  30519  numdenneg  30520  divnumden2  30521  ltesubnnd  30525  ccatf1  30612  swrdrn3  30616  swrdf1  30617  cshwrnid  30622  cycpmco2lem3  30778  cycpmco2lem4  30779  cycpmco2lem5  30780  cycpmco2lem6  30781  cycpmco2  30783  archiabllem1  30830  archiabllem2c  30832  zrhnm  31218  cnzh  31219  rezh  31220  qqhval2lem  31230  qqhghm  31237  qqhrhm  31238  qqhnm  31239  ballotlemfc0  31758  ballotlemfcc  31759  ballotlemic  31772  ballotlem1c  31773  ballotlemsgt1  31776  ballotlemsdom  31777  ballotlemsel1i  31778  ballotlemsf1o  31779  ballotlemsima  31781  ballotlemfrceq  31794  ballotlemfrcn0  31795  ballotlem1ri  31800  signsplypnf  31828  itgexpif  31885  fsum2dsub  31886  breprexplemc  31911  vtsprod  31918  circlemeth  31919  revpfxsfxrev  32370  swrdrevpfx  32371  revwlk  32379  swrdwlk  32381  divcnvlin  32972  fwddifnp1  33634  knoppndvlem2  33860  knoppndvlem7  33865  knoppndvlem14  33872  knoppndvlem16  33874  ltflcei  34921  poimirlem1  34934  poimirlem2  34935  poimirlem7  34940  poimirlem16  34949  poimirlem17  34950  poimirlem19  34952  poimirlem20  34953  poimirlem24  34957  poimirlem31  34964  poimirlem32  34965  fdc  35059  mettrifi  35071  caushft  35075  cntotbnd  35110  lcmineqlem6  39186  lcmineqlem18  39198  oexpreposd  39299  numdenexp  39306  exp11d  39309  mzpsubmpt  39477  lzenom  39504  diophun  39507  eqrabdioph  39511  irrapxlem2  39557  irrapxlem3  39558  pellexlem6  39568  pell1234qrreccl  39588  pellfund14  39632  rmxyneg  39654  rmxyadd  39655  rmxp1  39666  rmxm1  39668  rmym1  39669  rmxluc  39670  rmyluc  39671  rmyluc2  39672  rmxdbl  39673  rmydbl  39674  congadd  39700  congsub  39704  congabseq  39708  acongrep  39714  acongeq  39717  jm2.18  39722  jm2.19lem1  39723  jm2.19lem2  39724  jm2.19lem3  39725  jm2.22  39729  jm2.23  39730  jm2.20nn  39731  jm2.25  39733  jm2.26lem3  39735  jm2.27c  39741  nzss  40804  hashnzfz  40807  hashnzfz2  40808  hashnzfzclim  40809  uzmptshftfval  40833  sineq0ALT  41426  fzisoeu  41721  fperiodmul  41725  monoord2xrv  41914  fmul01lt1lem2  42018  sumnnodd  42063  dvdsn1add  42372  dvnmul  42376  dvnprodlem1  42379  stoweidlem11  42444  stoweidlem26  42459  dirkertrigeqlem1  42531  dirkertrigeqlem2  42532  dirkertrigeqlem3  42533  dirkertrigeq  42534  dirkeritg  42535  fourierdlem26  42566  fourierdlem48  42587  fourierdlem49  42588  fourierdlem79  42618  fourierdlem91  42630  fourierdlem103  42642  fourierdlem104  42643  fouriersw  42664  etransclem1  42668  etransclem4  42671  etransclem8  42675  etransclem9  42676  etransclem15  42682  etransclem17  42684  etransclem18  42685  etransclem20  42687  etransclem21  42688  etransclem22  42689  etransclem23  42690  etransclem24  42691  etransclem25  42692  etransclem35  42702  etransclem38  42705  etransclem41  42708  etransclem44  42711  etransclem45  42712  etransclem46  42713  etransclem47  42714  etransclem48  42715  2elfz2melfz  43666  fsumsplitsndif  43681  iccpartgtprec  43728  fargshiftf1  43749  fargshiftfo  43750  mod42tp1mod8  43912  sfprmdvdsmersenne  43913  lighneallem3  43917  lighneallem4b  43919  modexp2m1d  43922  dfodd6  43947  onego  43956  m1expoddALTV  43958  zofldiv2ALTV  43972  oddflALTV  43973  oexpnegALTV  43987  omoeALTV  43995  omeoALTV  43996  epoo  44013  emoo  44014  epee  44015  emee  44016  evensumeven  44017  evenltle  44027  even3prm2  44029  mogoldbblem  44030  fppr2odd  44041  fpprwppr  44049  fpprwpprb  44050  sbgoldbst  44088  sbgoldbaltlem2  44090  sgoldbeven3prm  44093  nnsum3primesprm  44100  nnsum4primesodd  44106  nnsum4primesoddALTV  44107  nnsum4primeseven  44110  nnsum4primesevenALTV  44111  bgoldbtbndlem2  44116  bgoldbtbndlem4  44118  bgoldbtbnd  44119  2zrngamnd  44357  2zrngacmnd  44358  2zrngagrp  44359  2zrngALT  44364  2zrngnmlid  44365  2zrngnmlid2  44367  ztprmneprm  44540  altgsumbcALT  44546  fldivmod  44723  m1modmmod  44726  zofldiv2  44736  fllogbd  44765  nnpw2blen  44785  blen1b  44793  blennngt2o2  44797  blennn0e2  44799  dig2nn1st  44810  dignn0flhalflem1  44820
  Copyright terms: Public domain W3C validator