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

Theorem zcnd 11312
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 11311 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 9921 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cc 9787  cz 11207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-resscn 9846
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-iota 5751  df-fv 5795  df-ov 6527  df-neg 10117  df-z 11208
This theorem is referenced by:  zsupss  11606  rpnnen1lem5  11647  rpnnen1lem5OLD  11653  fzm1  12241  fzrevral  12246  fzshftral  12249  nn0disj  12276  predfz  12285  fzoss2  12317  fzo0addelr  12342  fzosubel  12346  fzosubel3  12348  fzocatel  12351  fzosplitsnm1  12361  elfzom1elp1fzo1  12386  2tnp1ge0ge0  12444  quoremz  12468  intfrac2  12471  intfracq  12472  flpmodeq  12487  moddiffl  12495  modmul1  12537  modmul12d  12538  modfzo0difsn  12556  modsumfzodifsn  12557  addmodlteq  12559  uzrdgxfr  12580  fzen2  12582  monoord2  12646  seqf1olem1  12654  seqf1olem2  12655  seqz  12663  expaddzlem  12717  modexp  12813  sqoddm1div8  12842  bcm1k  12916  bcp1nk  12918  bcval5  12919  bcpasc  12922  hashfz  13023  hashfzo  13025  hashfzp1  13027  hashbclem  13042  seqcoll  13054  ccatval3  13159  ccatlid  13165  ccatass  13167  ccatalpha  13171  swrd0val  13216  swrdid  13223  swrd0fv  13234  swrdfv2  13241  swrds1  13246  ccatswrd  13251  swrdswrd0  13257  spllen  13299  splfv1  13300  splfv2a  13301  revccat  13309  revrev  13310  cshwidxmod  13343  cshwidxm1  13347  cshweqrep  13361  2cshwcshw  13365  cshimadifsn0  13370  seqshft  13616  fzomaxdif  13874  climshft2  14104  iserex  14178  isercoll2  14190  serf0  14202  iseraltlem2  14204  iseraltlem3  14205  iseralt  14206  sumrblem  14232  fsumm1  14267  fsumsplitsnun  14271  fsump1  14272  fsumshftm  14298  fsumrev2  14299  telfsumo  14318  fsumparts  14322  binomlem  14343  isumshft  14353  isumsplit  14354  isum1p  14355  arisum  14374  cvgrat  14397  mertenslem1  14398  ntrivcvg  14411  ntrivcvgtail  14414  prodrblem  14441  fprodser  14461  fprodm1  14479  fprodp1  14481  fprodrev  14489  fprodmodd  14510  fallfacval3  14525  fallfacfwd  14549  0fallfac  14550  binomfallfaclem2  14553  fallfacval4  14556  fsumkthpow  14569  eirrlem  14714  sqr2irrlem  14759  dvds2ln  14795  dvdsadd2b  14809  fsumdvds  14811  fzocongeq  14827  addmodlteqALT  14828  dvdsexp  14830  dvdsmod  14831  3dvds  14833  3dvdsOLD  14834  fprodfvdvdsd  14839  odd2np1  14846  oddm1even  14848  oexpneg  14850  mod2eq1n2dvds  14852  mulsucdiv2z  14858  zob  14864  ltoddhalfle  14866  sumodd  14892  pwp1fsum  14895  divalglem0  14897  divalglem4  14900  divalglem8  14904  divalgb  14908  divalgmod  14910  divalgmodOLD  14911  modremain  14913  flodddiv4  14918  bitsp1  14934  bitsfzo  14938  bitsmod  14939  bitsinv1lem  14944  bitsf1  14949  sadaddlem  14969  bitsres  14976  bitsuz  14977  bitsshft  14978  smumullem  14995  modgcd  15034  bezoutlem1  15037  bezoutlem2  15038  bezoutlem3  15039  bezoutlem4  15040  dvdsmulgcd  15055  rplpwr  15057  lcmid  15103  absprodnn  15112  mulgcddvds  15150  divgcdcoprm0  15160  cncongr1  15162  cncongr2  15163  rpexp  15213  qmuldeneqnum  15236  numdensq  15243  qden1elz  15246  hashdvds  15261  phiprm  15263  eulerthlem2  15268  fermltl  15270  prmdiv  15271  prmdiveq  15272  hashgcdlem  15274  odzdvds  15281  vfermltlALT  15288  modprm0  15291  modprmn0modprm0  15293  pythagtriplem6  15307  pythagtriplem7  15308  pythagtriplem15  15315  pcpremul  15329  pceulem  15331  pczpre  15333  pcdiv  15338  pcqmul  15339  pcqdiv  15343  pcexp  15345  pcaddlem  15373  pcadd  15374  fldivp1  15382  pcfac  15384  pcbc  15385  prmpwdvds  15389  prmreclem4  15404  4sqlem5  15427  4sqlem8  15430  4sqlem9  15431  4sqlem10  15432  4sqlem11  15440  4sqlem14  15443  4sqlem16  15445  4sqlem17  15446  vdwapun  15459  vdwnnlem2  15481  prmop1  15523  prmdvdsprmo  15527  prmgaplem7  15542  prmlem0  15593  mulgsubcl  17321  mulgdirlem  17338  mulgdir  17339  mulgass  17345  mulgmodid  17347  mulgsubdir  17348  psgnunilem5  17680  psgnunilem2  17681  psgnunilem4  17683  m1expaddsub  17684  psgnuni  17685  odnncl  17730  odmulg  17739  odbezout  17741  sylow1lem1  17779  sylow2alem2  17799  efgsres  17917  efgredleme  17922  efgredlemc  17924  odadd1  18017  odadd2  18018  cyggeninv  18051  gsummptshft  18102  ablfacrp  18231  pgpfac1lem3  18242  srgbinomlem3  18308  srgbinomlem4  18309  zringmulg  19588  zringlpirlem1  19594  zringlpirlem3  19596  prmirredlem  19602  zndvds0  19660  znf1o  19661  znunit  19673  cayhamlem1  20429  tgpmulg  21646  zdis  22356  uniioombllem3  23073  mbfi1fseqlem4  23205  dvexp3  23459  aareccl  23799  aalioulem1  23805  geolim3  23812  aaliou3lem2  23816  aaliou3lem6  23821  ulmshft  23862  sineq0  23991  efif1olem2  24007  igamz  24488  wilthlem1  24508  wilthlem2  24509  basellem3  24523  mumul  24621  musum  24631  musumsum  24632  muinv  24633  ppiub  24643  chtub  24651  logfac2  24656  chpchtsum  24658  dchrptlem1  24703  pcbcctr  24715  bcmono  24716  bposlem5  24727  bposlem6  24728  lgslem1  24736  lgsval2lem  24746  lgsval4a  24758  lgsneg  24760  lgsneg1  24761  lgsmod  24762  lgsdirprm  24770  lgsdir  24771  lgsdilem2  24772  lgsdi  24773  lgsne0  24774  lgsabs1  24775  lgssq  24776  lgssq2  24777  lgsmulsqcoprm  24782  lgsdirnn0  24783  lgsdinn0  24784  lgsqrlem1  24785  gausslemma2dlem1a  24804  gausslemma2dlem1  24805  gausslemma2dlem4  24808  gausslemma2dlem5a  24809  gausslemma2dlem5  24810  gausslemma2dlem6  24811  gausslemma2d  24813  lgseisenlem1  24814  lgseisenlem2  24815  lgseisenlem3  24816  lgseisenlem4  24817  lgsquadlem1  24819  lgsquad2lem1  24823  lgsquad3  24826  2lgslem1b  24831  2lgsoddprmlem2  24848  2sqlem3  24859  2sqlem4  24860  2sqlem8a  24864  2sqlem8  24865  2sqlem11  24868  2sqblem  24870  dchrisumlem1  24892  dchrmusum2  24897  dchrvmasumlem1  24898  dchrvmasum2lem  24899  mudivsum  24933  mulogsum  24935  mulog2sumlem2  24938  selberglem1  24948  selberglem3  24950  selberg  24951  pntpbnd2  24990  pntlemf  25008  padicabvcxp  25035  axlowdimlem14  25550  axlowdimlem16  25552  wlkdvspthlem  25900  fargshiftf1  25928  fargshiftfo  25929  clwwisshclww  26098  eupatrl  26258  znsqcld  28703  fzspl  28741  bcm1n  28744  numdenneg  28753  divnumden2  28754  ltesubnnd  28758  2sqn0  28780  2sqmod  28782  archiabllem1  28881  archiabllem2c  28883  zrhnm  29144  cnzh  29145  rezh  29146  qqhval2lem  29156  qqhghm  29163  qqhrhm  29164  qqhnm  29165  ballotlemfc0  29684  ballotlemfcc  29685  ballotlemic  29698  ballotlem1c  29699  ballotlemsgt1  29702  ballotlemsdom  29703  ballotlemsel1i  29704  ballotlemsf1o  29705  ballotlemsima  29707  ballotlemfrceq  29720  ballotlemfrcn0  29721  ballotlem1ri  29726  signsplypnf  29756  divcnvlin  30674  fwddifnp1  31245  knoppndvlem2  31477  knoppndvlem7  31482  knoppndvlem14  31489  knoppndvlem16  31491  ltflcei  32367  poimirlem1  32380  poimirlem2  32381  poimirlem7  32386  poimirlem16  32395  poimirlem17  32396  poimirlem19  32398  poimirlem20  32399  poimirlem24  32403  poimirlem31  32410  poimirlem32  32411  fdc  32511  mettrifi  32523  caushft  32527  cntotbnd  32565  mzpsubmpt  36124  lzenom  36151  diophun  36155  eqrabdioph  36159  irrapxlem2  36205  irrapxlem3  36206  pellexlem6  36216  pell1234qrreccl  36236  pellfund14  36280  rmxyneg  36303  rmxyadd  36304  rmxp1  36315  rmxm1  36317  rmym1  36318  rmxluc  36319  rmyluc  36320  rmyluc2  36321  rmxdbl  36322  rmydbl  36323  congadd  36351  congsub  36355  congabseq  36359  acongrep  36365  acongeq  36368  jm2.18  36373  jm2.19lem1  36374  jm2.19lem2  36375  jm2.19lem3  36376  jm2.22  36380  jm2.23  36381  jm2.20nn  36382  jm2.25  36384  jm2.26lem3  36386  jm2.27c  36392  nzss  37338  hashnzfz  37341  hashnzfz2  37342  hashnzfzclim  37343  uzmptshftfval  37367  sineq0ALT  37995  fzisoeu  38255  fperiodmul  38259  fmul01lt1lem2  38453  sumnnodd  38498  dvdsn1add  38630  dvnmul  38634  dvnprodlem1  38637  stoweidlem11  38705  stoweidlem26  38720  dirkertrigeqlem1  38792  dirkertrigeqlem2  38793  dirkertrigeqlem3  38794  dirkertrigeq  38795  dirkeritg  38796  fourierdlem26  38827  fourierdlem48  38848  fourierdlem49  38849  fourierdlem79  38879  fourierdlem91  38891  fourierdlem103  38903  fourierdlem104  38904  fouriersw  38925  etransclem1  38929  etransclem4  38932  etransclem8  38936  etransclem9  38937  etransclem15  38943  etransclem17  38945  etransclem18  38946  etransclem20  38948  etransclem21  38949  etransclem22  38950  etransclem23  38951  etransclem24  38952  etransclem25  38953  etransclem35  38963  etransclem38  38966  etransclem41  38969  etransclem44  38972  etransclem45  38973  etransclem46  38974  etransclem47  38975  etransclem48  38976  iccpartgtprec  39760  pwdif  39841  mod42tp1mod8  39859  sfprmdvdsmersenne  39860  lighneallem3  39864  lighneallem4b  39866  modexp2m1d  39869  dfodd6  39890  onego  39899  m1expoddALTV  39901  zofldiv2ALTV  39914  oddflALTV  39915  oexpnegALTV  39928  omoeALTV  39936  omeoALTV  39937  epoo  39952  emoo  39953  epee  39954  emee  39955  evensumeven  39956  bgoldbst  40002  sgoldbaltlem2  40004  nnsum3primesprm  40008  nnsum4primesodd  40014  nnsum4primesoddALTV  40015  nnsum4primeseven  40018  nnsum4primesevenALTV  40019  bgoldbtbndlem2  40024  bgoldbtbndlem4  40026  bgoldbtbnd  40027  pfxfv  40064  ccatpfx  40074  pfxccatin12lem2  40089  2elfz2melfz  40179  fsumsplitsndif  40219  pthdadjvtx  40935  crctcsh1wlkn0lem4  41015  crctcsh1wlkn0lem5  41016  crctcshlem4  41022  crctcsh  41026  clwwisshclwws  41234  eucrctshift  41410  2zrngamnd  41730  2zrngacmnd  41731  2zrngagrp  41732  2zrngALT  41737  2zrngnmlid  41738  2zrngnmlid2  41740  ztprmneprm  41917  altgsumbcALT  41923  fldivmod  42106  m1modmmod  42109  zofldiv2  42118  fllogbd  42151  nnpw2blen  42171  blen1b  42179  blennngt2o2  42183  blennn0e2  42185  dig2nn1st  42196  dignn0flhalflem1  42206
  Copyright terms: Public domain W3C validator