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

Theorem zcnd 11468
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 11467 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 10053 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  cc 9919  cz 11362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-resscn 9978
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-ov 6638  df-neg 10254  df-z 11363
This theorem is referenced by:  zsupss  11762  rpnnen1lem5  11803  rpnnen1lem5OLD  11809  fzm1  12404  fzrevral  12409  fzshftral  12412  nn0disj  12439  predfz  12448  fzoss2  12480  fzo0addelr  12506  fzosubel  12510  fzosubel3  12512  fzocatel  12515  fzosplitsnm1  12526  elfzom1elp1fzo1  12552  2tnp1ge0ge0  12613  quoremz  12637  intfrac2  12640  intfracq  12641  flpmodeq  12656  moddiffl  12664  modmul1  12706  modmul12d  12707  modfzo0difsn  12725  modsumfzodifsn  12726  addmodlteq  12728  uzrdgxfr  12749  fzen2  12751  monoord2  12815  seqf1olem1  12823  seqf1olem2  12824  seqz  12832  expaddzlem  12886  modexp  12982  sqoddm1div8  13011  bcm1k  13085  bcp1nk  13087  bcval5  13088  bcpasc  13091  hashfz  13197  hashfzo  13199  hashfzp1  13201  hashbclem  13219  seqcoll  13231  ccatval3  13346  ccatlid  13352  ccatass  13354  ccatalpha  13358  swrd0val  13403  swrdid  13410  swrd0fv  13421  swrdfv2  13428  swrds1  13433  ccatswrd  13438  swrdswrd0  13444  spllen  13486  splfv1  13487  splfv2a  13488  revccat  13496  revrev  13497  cshwidxmod  13530  cshwidxm1  13534  cshweqrep  13548  2cshwcshw  13552  cshimadifsn0  13557  seqshft  13806  fzomaxdif  14064  climshft2  14294  iserex  14368  isercoll2  14380  serf0  14392  iseraltlem2  14394  iseraltlem3  14395  iseralt  14396  sumrblem  14423  fsumm1  14461  fsumsplitsnun  14465  fsumsplitsnunOLD  14467  fsump1  14468  fsumshftm  14494  fsumrev2  14495  telfsumo  14515  fsumparts  14519  binomlem  14542  isumshft  14552  isumsplit  14553  isum1p  14554  arisum  14573  cvgrat  14596  mertenslem1  14597  ntrivcvg  14610  ntrivcvgtail  14613  prodrblem  14640  fprodser  14660  fprodm1  14678  fprodp1  14680  fprodrev  14688  fprodmodd  14709  fallfacval3  14724  fallfacfwd  14748  0fallfac  14749  binomfallfaclem2  14752  fallfacval4  14755  fsumkthpow  14768  eirrlem  14913  sqrt2irrlem  14958  sqrt2irrlemOLD  14959  dvds2ln  14995  dvdsadd2b  15009  fsumdvds  15011  fzocongeq  15027  addmodlteqALT  15028  dvdsexp  15030  dvdsmod  15031  3dvds  15033  3dvdsOLD  15034  fprodfvdvdsd  15039  odd2np1  15046  oddm1even  15048  oexpneg  15050  mod2eq1n2dvds  15052  mulsucdiv2z  15058  zob  15064  ltoddhalfle  15066  sumodd  15092  pwp1fsum  15095  divalglem0  15097  divalglem4  15100  divalglem8  15104  divalgb  15108  divalgmod  15110  divalgmodOLD  15111  modremain  15113  flodddiv4  15118  bitsp1  15134  bitsfzo  15138  bitsmod  15139  bitsinv1lem  15144  bitsf1  15149  sadaddlem  15169  bitsres  15176  bitsuz  15177  bitsshft  15178  smumullem  15195  modgcd  15234  bezoutlem1  15237  bezoutlem2  15238  bezoutlem3  15239  bezoutlem4  15240  dvdsmulgcd  15255  rplpwr  15257  lcmid  15303  absprodnn  15312  mulgcddvds  15350  divgcdcoprm0  15360  cncongr1  15362  cncongr2  15363  rpexp  15413  qmuldeneqnum  15436  numdensq  15443  qden1elz  15446  hashdvds  15461  phiprm  15463  eulerthlem2  15468  fermltl  15470  prmdiv  15471  prmdiveq  15472  hashgcdlem  15474  odzdvds  15481  vfermltlALT  15488  modprm0  15491  modprmn0modprm0  15493  pythagtriplem6  15507  pythagtriplem7  15508  pythagtriplem15  15515  pcpremul  15529  pceulem  15531  pczpre  15533  pcdiv  15538  pcqmul  15539  pcqdiv  15543  pcexp  15545  pcaddlem  15573  pcadd  15574  fldivp1  15582  pcfac  15584  pcbc  15585  prmpwdvds  15589  prmreclem4  15604  4sqlem5  15627  4sqlem8  15630  4sqlem9  15631  4sqlem10  15632  4sqlem11  15640  4sqlem14  15643  4sqlem16  15645  4sqlem17  15646  vdwapun  15659  vdwnnlem2  15681  prmop1  15723  prmdvdsprmo  15727  prmgaplem7  15742  prmlem0  15793  mulgsubcl  17536  mulgdirlem  17553  mulgdir  17554  mulgass  17560  mulgmodid  17562  mulgsubdir  17563  psgnunilem5  17895  psgnunilem2  17896  psgnunilem4  17898  m1expaddsub  17899  psgnuni  17900  odnncl  17945  odmulg  17954  odbezout  17956  sylow1lem1  17994  sylow2alem2  18014  efgsres  18132  efgredleme  18137  efgredlemc  18139  odadd1  18232  odadd2  18233  cyggeninv  18266  gsummptshft  18317  ablfacrp  18446  pgpfac1lem3  18457  srgbinomlem3  18523  srgbinomlem4  18524  zringmulg  19807  zringlpirlem1  19813  zringlpirlem3  19815  prmirredlem  19822  zndvds0  19880  znf1o  19881  znunit  19893  cayhamlem1  20652  tgpmulg  21878  zdis  22600  uniioombllem3  23334  mbfi1fseqlem4  23466  dvexp3  23722  aareccl  24062  aalioulem1  24068  geolim3  24075  aaliou3lem2  24079  aaliou3lem6  24084  ulmshft  24125  sineq0  24254  efif1olem2  24270  igamz  24755  wilthlem1  24775  wilthlem2  24776  basellem3  24790  mumul  24888  musum  24898  musumsum  24899  muinv  24900  ppiub  24910  chtub  24918  logfac2  24923  chpchtsum  24925  dchrptlem1  24970  pcbcctr  24982  bcmono  24983  bposlem5  24994  bposlem6  24995  lgslem1  25003  lgsval2lem  25013  lgsval4a  25025  lgsneg  25027  lgsneg1  25028  lgsmod  25029  lgsdirprm  25037  lgsdir  25038  lgsdilem2  25039  lgsdi  25040  lgsne0  25041  lgsabs1  25042  lgssq  25043  lgssq2  25044  lgsmulsqcoprm  25049  lgsdirnn0  25050  lgsdinn0  25051  lgsqrlem1  25052  gausslemma2dlem1a  25071  gausslemma2dlem1  25072  gausslemma2dlem4  25075  gausslemma2dlem5a  25076  gausslemma2dlem5  25077  gausslemma2dlem6  25078  gausslemma2d  25080  lgseisenlem1  25081  lgseisenlem2  25082  lgseisenlem3  25083  lgseisenlem4  25084  lgsquadlem1  25086  lgsquad2lem1  25090  lgsquad3  25093  2lgslem1b  25098  2lgsoddprmlem2  25115  2sqlem3  25126  2sqlem4  25127  2sqlem8a  25131  2sqlem8  25132  2sqlem11  25135  2sqblem  25137  dchrisumlem1  25159  dchrmusum2  25164  dchrvmasumlem1  25165  dchrvmasum2lem  25166  mudivsum  25200  mulogsum  25202  mulog2sumlem2  25205  selberglem1  25215  selberglem3  25217  selberg  25218  pntpbnd2  25257  pntlemf  25275  padicabvcxp  25302  axlowdimlem14  25816  axlowdimlem16  25818  pthdadjvtx  26607  crctcshwlkn0lem4  26686  crctcshwlkn0lem5  26687  crctcshlem4  26693  crctcsh  26697  clwwisshclwws  26908  eucrctshift  27083  znsqcld  29486  fzspl  29524  bcm1n  29528  numdenneg  29537  divnumden2  29538  ltesubnnd  29542  2sqn0  29620  2sqmod  29622  archiabllem1  29721  archiabllem2c  29723  zrhnm  29987  cnzh  29988  rezh  29989  qqhval2lem  29999  qqhghm  30006  qqhrhm  30007  qqhnm  30008  ballotlemfc0  30528  ballotlemfcc  30529  ballotlemic  30542  ballotlem1c  30543  ballotlemsgt1  30546  ballotlemsdom  30547  ballotlemsel1i  30548  ballotlemsf1o  30549  ballotlemsima  30551  ballotlemfrceq  30564  ballotlemfrcn0  30565  ballotlem1ri  30570  signsplypnf  30601  itgexpif  30658  fsum2dsub  30659  breprexplemc  30684  vtsprod  30691  circlemeth  30692  divcnvlin  31593  fwddifnp1  32247  knoppndvlem2  32479  knoppndvlem7  32484  knoppndvlem14  32491  knoppndvlem16  32493  ltflcei  33368  poimirlem1  33381  poimirlem2  33382  poimirlem7  33387  poimirlem16  33396  poimirlem17  33397  poimirlem19  33399  poimirlem20  33400  poimirlem24  33404  poimirlem31  33411  poimirlem32  33412  fdc  33512  mettrifi  33524  caushft  33528  cntotbnd  33566  mzpsubmpt  37125  lzenom  37152  diophun  37156  eqrabdioph  37160  irrapxlem2  37206  irrapxlem3  37207  pellexlem6  37217  pell1234qrreccl  37237  pellfund14  37281  rmxyneg  37304  rmxyadd  37305  rmxp1  37316  rmxm1  37318  rmym1  37319  rmxluc  37320  rmyluc  37321  rmyluc2  37322  rmxdbl  37323  rmydbl  37324  congadd  37352  congsub  37356  congabseq  37360  acongrep  37366  acongeq  37369  jm2.18  37374  jm2.19lem1  37375  jm2.19lem2  37376  jm2.19lem3  37377  jm2.22  37381  jm2.23  37382  jm2.20nn  37383  jm2.25  37385  jm2.26lem3  37387  jm2.27c  37393  nzss  38336  hashnzfz  38339  hashnzfz2  38340  hashnzfzclim  38341  uzmptshftfval  38365  sineq0ALT  38993  fzisoeu  39327  fperiodmul  39331  fmul01lt1lem2  39617  sumnnodd  39662  dvdsn1add  39917  dvnmul  39921  dvnprodlem1  39924  stoweidlem11  39991  stoweidlem26  40006  dirkertrigeqlem1  40078  dirkertrigeqlem2  40079  dirkertrigeqlem3  40080  dirkertrigeq  40081  dirkeritg  40082  fourierdlem26  40113  fourierdlem48  40134  fourierdlem49  40135  fourierdlem79  40165  fourierdlem91  40177  fourierdlem103  40189  fourierdlem104  40190  fouriersw  40211  etransclem1  40215  etransclem4  40218  etransclem8  40222  etransclem9  40223  etransclem15  40229  etransclem17  40231  etransclem18  40232  etransclem20  40234  etransclem21  40235  etransclem22  40236  etransclem23  40237  etransclem24  40238  etransclem25  40239  etransclem35  40249  etransclem38  40252  etransclem41  40255  etransclem44  40258  etransclem45  40259  etransclem46  40260  etransclem47  40261  etransclem48  40262  2elfz2melfz  41091  fsumsplitsndif  41107  iccpartgtprec  41120  fargshiftf1  41141  fargshiftfo  41142  pfxfv  41164  ccatpfx  41174  pfxccatin12lem2  41189  pwdif  41266  mod42tp1mod8  41284  sfprmdvdsmersenne  41285  lighneallem3  41289  lighneallem4b  41291  modexp2m1d  41294  dfodd6  41315  onego  41324  m1expoddALTV  41326  zofldiv2ALTV  41339  oddflALTV  41340  oexpnegALTV  41353  omoeALTV  41361  omeoALTV  41362  epoo  41377  emoo  41378  epee  41379  emee  41380  evensumeven  41381  evenltle  41391  even3prm2  41393  mogoldbblem  41394  sbgoldbst  41431  sbgoldbaltlem2  41433  sgoldbeven3prm  41436  nnsum3primesprm  41443  nnsum4primesodd  41449  nnsum4primesoddALTV  41450  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  bgoldbtbndlem2  41459  bgoldbtbndlem4  41461  bgoldbtbnd  41462  2zrngamnd  41706  2zrngacmnd  41707  2zrngagrp  41708  2zrngALT  41713  2zrngnmlid  41714  2zrngnmlid2  41716  ztprmneprm  41890  altgsumbcALT  41896  fldivmod  42078  m1modmmod  42081  zofldiv2  42090  fllogbd  42119  nnpw2blen  42139  blen1b  42147  blennngt2o2  42151  blennn0e2  42153  dig2nn1st  42164  dignn0flhalflem1  42174
  Copyright terms: Public domain W3C validator