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

Theorem zcnd 12077
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 12076 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 10658 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cc 10524  cz 11970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-resscn 10583
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148  df-neg 10862  df-z 11971
This theorem is referenced by:  zsupss  12326  rpnnen1lem5  12370  fzm1  12977  fzrevral  12982  fzshftral  12985  nn0disj  13013  predfz  13022  fzoss2  13055  fzo0addelr  13082  fzosubel  13086  fzosubel3  13088  fzocatel  13091  fzosplitsnm1  13102  elfzom1elp1fzo1  13127  2tnp1ge0ge0  13189  quoremz  13213  intfrac2  13216  intfracq  13217  flpmodeq  13232  moddiffl  13240  modmul1  13282  modmul12d  13283  modfzo0difsn  13301  modsumfzodifsn  13302  addmodlteq  13304  uzrdgxfr  13325  fzen2  13327  monoord2  13391  seqf1olem1  13399  seqf1olem2  13400  seqz  13408  expaddzlem  13462  znsqcld  13516  modexp  13589  sqoddm1div8  13594  bcm1k  13665  bcp1nk  13667  bcval5  13668  bcpasc  13671  hashfz  13778  hashfzo  13780  hashfzp1  13782  hashbclem  13800  seqcoll  13812  ccatval3  13923  ccatlid  13930  ccatass  13932  ccatalpha  13937  swrdfv0  14001  swrdfv2  14013  swrds1  14018  ccatswrd  14020  pfxfv  14034  ccatpfx  14053  swrdpfx  14059  pfxccatin12lem2  14083  spllen  14106  revccat  14118  revrev  14119  cshwidxmod  14155  cshwidxm1  14159  cshweqrep  14173  2cshwcshw  14177  cshimadifsn0  14182  swrds2m  14293  seqshft  14434  fzomaxdif  14693  climshft2  14929  iserex  15003  isercoll2  15015  serf0  15027  iseraltlem2  15029  iseraltlem3  15030  iseralt  15031  sumrblem  15058  fsumm1  15096  fsumsplitsnun  15100  fsump1  15101  fsumshftm  15126  fsumrev2  15127  telfsumo  15147  fsumparts  15151  binomlem  15174  isumshft  15184  isumsplit  15185  isum1p  15186  arisum  15205  pwdif  15213  cvgrat  15229  mertenslem1  15230  ntrivcvg  15243  ntrivcvgtail  15246  prodrblem  15273  fprodser  15293  fprodm1  15311  fprodp1  15313  fprodrev  15321  fprodmodd  15341  fallfacval3  15356  fallfacfwd  15380  0fallfac  15381  binomfallfaclem2  15384  fallfacval4  15387  fsumkthpow  15400  eirrlem  15547  sqrt2irrlem  15591  dvds2ln  15632  dvdsadd2b  15646  fsumdvds  15648  fzocongeq  15664  addmodlteqALT  15665  dvdsexp  15667  dvdsmod  15668  3dvds  15670  fprodfvdvdsd  15673  odd2np1  15680  oddm1even  15682  oexpneg  15684  mod2eq1n2dvds  15686  mulsucdiv2z  15692  zob  15698  ltoddhalfle  15700  sumodd  15729  pwp1fsum  15732  divalglem0  15734  divalglem4  15737  divalglem8  15741  divalgb  15745  divalgmod  15747  modremain  15749  flodddiv4  15754  bitsp1  15770  bitsfzo  15774  bitsmod  15775  bitsinv1lem  15780  bitsf1  15785  sadaddlem  15805  bitsres  15812  bitsuz  15813  bitsshft  15814  smumullem  15831  modgcd  15870  gcdmultipled  15872  dvdsgcdidd  15875  bezoutlem1  15877  bezoutlem2  15878  bezoutlem3  15879  bezoutlem4  15880  dvdsmulgcd  15895  rplpwr  15897  lcmid  15943  absprodnn  15952  mulgcddvds  15989  divgcdcoprm0  15999  cncongr1  16001  cncongr2  16002  rpexp  16054  qmuldeneqnum  16077  numdensq  16084  qden1elz  16087  hashdvds  16102  phiprm  16104  eulerthlem2  16109  fermltl  16111  prmdiv  16112  prmdiveq  16113  hashgcdlem  16115  odzdvds  16122  vfermltlALT  16129  modprm0  16132  modprmn0modprm0  16134  pythagtriplem6  16148  pythagtriplem7  16149  pythagtriplem15  16156  pcpremul  16170  pceulem  16172  pczpre  16174  pcdiv  16179  pcqmul  16180  pcqdiv  16184  pcexp  16186  pcaddlem  16214  pcadd  16215  fldivp1  16223  pcfac  16225  pcbc  16226  prmpwdvds  16230  prmreclem4  16245  4sqlem5  16268  4sqlem8  16271  4sqlem9  16272  4sqlem10  16273  4sqlem11  16281  4sqlem14  16284  4sqlem16  16286  4sqlem17  16287  vdwapun  16300  vdwnnlem2  16322  prmop1  16364  prmdvdsprmo  16368  prmgaplem7  16383  prmlem0  16429  mulgsubcl  18182  mulgdirlem  18198  mulgdir  18199  mulgass  18204  mulgmodid  18206  mulgsubdir  18207  psgnunilem5  18553  psgnunilem2  18554  psgnunilem4  18556  m1expaddsub  18557  psgnuni  18558  odnncl  18604  odmulg  18614  odbezout  18616  sylow1lem1  18654  sylow2alem2  18674  efgsres  18795  efgredleme  18800  efgredlemc  18802  odadd1  18899  odadd2  18900  cyggeninv  18933  gsummptshft  18987  ablfacrp  19119  pgpfac1lem3  19130  fincygsubgodd  19165  srgbinomlem3  19223  srgbinomlem4  19224  zringmulg  20555  zringlpirlem1  20561  zringlpirlem3  20563  prmirredlem  20570  zndvds0  20627  znf1o  20628  znunit  20640  cayhamlem1  21404  tgpmulg  22631  zdis  23353  uniioombllem3  24115  mbfi1fseqlem4  24248  dvexp3  24504  aareccl  24844  aalioulem1  24850  geolim3  24857  aaliou3lem2  24861  aaliou3lem6  24866  ulmshft  24907  sineq0  25038  efif1olem2  25054  igamz  25553  wilthlem1  25573  wilthlem2  25574  basellem3  25588  mumul  25686  musum  25696  musumsum  25697  muinv  25698  ppiub  25708  chtub  25716  logfac2  25721  chpchtsum  25723  dchrptlem1  25768  pcbcctr  25780  bcmono  25781  bposlem5  25792  bposlem6  25793  lgslem1  25801  lgsval2lem  25811  lgsval4a  25823  lgsneg  25825  lgsneg1  25826  lgsmod  25827  lgsdirprm  25835  lgsdir  25836  lgsdilem2  25837  lgsdi  25838  lgsne0  25839  lgsabs1  25840  lgssq  25841  lgssq2  25842  lgsmulsqcoprm  25847  lgsdirnn0  25848  lgsdinn0  25849  lgsqrlem1  25850  gausslemma2dlem1a  25869  gausslemma2dlem1  25870  gausslemma2dlem4  25873  gausslemma2dlem5a  25874  gausslemma2dlem5  25875  gausslemma2dlem6  25876  gausslemma2d  25878  lgseisenlem1  25879  lgseisenlem2  25880  lgseisenlem3  25881  lgseisenlem4  25882  lgsquadlem1  25884  lgsquad2lem1  25888  lgsquad3  25891  2lgslem1b  25896  2lgsoddprmlem2  25913  2sqlem3  25924  2sqlem4  25925  2sqlem8a  25929  2sqlem8  25930  2sqlem11  25933  2sqblem  25935  2sqn0  25938  2sqmod  25940  dchrisumlem1  25993  dchrmusum2  25998  dchrvmasumlem1  25999  dchrvmasum2lem  26000  mudivsum  26034  mulogsum  26036  mulog2sumlem2  26039  selberglem1  26049  selberglem3  26051  selberg  26052  pntpbnd2  26091  pntlemf  26109  padicabvcxp  26136  axlowdimlem14  26669  axlowdimlem16  26671  pthdadjvtx  27439  crctcshwlkn0lem4  27519  crctcshwlkn0lem5  27520  crctcshlem4  27526  crctcsh  27530  clwwlkccatlem  27695  clwwisshclwws  27721  eucrctshift  27950  fzm1ne1  30439  fzspl  30440  bcm1n  30445  fzom1ne1  30451  dvdszzq  30458  prmdvdsbc  30459  numdenneg  30460  divnumden2  30461  ltesubnnd  30466  ccatf1  30553  swrdrn3  30557  swrdf1  30558  cshwrnid  30563  cycpmco2lem3  30698  cycpmco2lem4  30699  cycpmco2lem5  30700  cycpmco2lem6  30701  cycpmco2  30703  archiabllem1  30750  archiabllem2c  30752  zrhnm  31110  cnzh  31111  rezh  31112  qqhval2lem  31122  qqhghm  31129  qqhrhm  31130  qqhnm  31131  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemic  31664  ballotlem1c  31665  ballotlemsgt1  31668  ballotlemsdom  31669  ballotlemsel1i  31670  ballotlemsf1o  31671  ballotlemsima  31673  ballotlemfrceq  31686  ballotlemfrcn0  31687  ballotlem1ri  31692  signsplypnf  31720  itgexpif  31777  fsum2dsub  31778  breprexplemc  31803  vtsprod  31810  circlemeth  31811  revpfxsfxrev  32260  swrdrevpfx  32261  revwlk  32269  swrdwlk  32271  divcnvlin  32862  fwddifnp1  33524  knoppndvlem2  33750  knoppndvlem7  33755  knoppndvlem14  33762  knoppndvlem16  33764  ltflcei  34762  poimirlem1  34775  poimirlem2  34776  poimirlem7  34781  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem24  34798  poimirlem31  34805  poimirlem32  34806  fdc  34903  mettrifi  34915  caushft  34919  cntotbnd  34957  oexpreposd  39059  numdenexp  39066  exp11d  39069  mzpsubmpt  39220  lzenom  39247  diophun  39250  eqrabdioph  39254  irrapxlem2  39300  irrapxlem3  39301  pellexlem6  39311  pell1234qrreccl  39331  pellfund14  39375  rmxyneg  39397  rmxyadd  39398  rmxp1  39409  rmxm1  39411  rmym1  39412  rmxluc  39413  rmyluc  39414  rmyluc2  39415  rmxdbl  39416  rmydbl  39417  congadd  39443  congsub  39447  congabseq  39451  acongrep  39457  acongeq  39460  jm2.18  39465  jm2.19lem1  39466  jm2.19lem2  39467  jm2.19lem3  39468  jm2.22  39472  jm2.23  39473  jm2.20nn  39474  jm2.25  39476  jm2.26lem3  39478  jm2.27c  39484  nzss  40529  hashnzfz  40532  hashnzfz2  40533  hashnzfzclim  40534  uzmptshftfval  40558  sineq0ALT  41151  fzisoeu  41447  fperiodmul  41451  monoord2xrv  41640  fmul01lt1lem2  41746  sumnnodd  41791  dvdsn1add  42104  dvnmul  42108  dvnprodlem1  42111  stoweidlem11  42177  stoweidlem26  42192  dirkertrigeqlem1  42264  dirkertrigeqlem2  42265  dirkertrigeqlem3  42266  dirkertrigeq  42267  dirkeritg  42268  fourierdlem26  42299  fourierdlem48  42320  fourierdlem49  42321  fourierdlem79  42351  fourierdlem91  42363  fourierdlem103  42375  fourierdlem104  42376  fouriersw  42397  etransclem1  42401  etransclem4  42404  etransclem8  42408  etransclem9  42409  etransclem15  42415  etransclem17  42417  etransclem18  42418  etransclem20  42420  etransclem21  42421  etransclem22  42422  etransclem23  42423  etransclem24  42424  etransclem25  42425  etransclem35  42435  etransclem38  42438  etransclem41  42441  etransclem44  42444  etransclem45  42445  etransclem46  42446  etransclem47  42447  etransclem48  42448  2elfz2melfz  43399  fsumsplitsndif  43414  iccpartgtprec  43427  fargshiftf1  43448  fargshiftfo  43449  mod42tp1mod8  43614  sfprmdvdsmersenne  43615  lighneallem3  43619  lighneallem4b  43621  modexp2m1d  43624  dfodd6  43649  onego  43658  m1expoddALTV  43660  zofldiv2ALTV  43674  oddflALTV  43675  oexpnegALTV  43689  omoeALTV  43697  omeoALTV  43698  epoo  43715  emoo  43716  epee  43717  emee  43718  evensumeven  43719  evenltle  43729  even3prm2  43731  mogoldbblem  43732  fppr2odd  43743  fpprwppr  43751  fpprwpprb  43752  sbgoldbst  43790  sbgoldbaltlem2  43792  sgoldbeven3prm  43795  nnsum3primesprm  43802  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  bgoldbtbndlem2  43818  bgoldbtbndlem4  43820  bgoldbtbnd  43821  2zrngamnd  44110  2zrngacmnd  44111  2zrngagrp  44112  2zrngALT  44117  2zrngnmlid  44118  2zrngnmlid2  44120  ztprmneprm  44293  altgsumbcALT  44299  fldivmod  44476  m1modmmod  44479  zofldiv2  44489  fllogbd  44518  nnpw2blen  44538  blen1b  44546  blennngt2o2  44550  blennn0e2  44552  dig2nn1st  44563  dignn0flhalflem1  44573
  Copyright terms: Public domain W3C validator