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

Theorem zcnd 12541
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 12540 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 11117 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cc 10983  cz 12433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-resscn 11042
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-iota 6444  df-fv 6500  df-ov 7353  df-neg 11322  df-z 12434
This theorem is referenced by:  zsupss  12791  rpnnen1lem5  12835  fzm1  13450  fzrevral  13455  fzshftral  13458  nn0disj  13486  predfz  13495  fzoss2  13529  fzo0addelr  13556  fzosubel  13560  fzosubel3  13562  fzocatel  13565  fzosplitsnm1  13576  elfzom1elp1fzo1  13601  2tnp1ge0ge0  13663  quoremz  13689  intfrac2  13692  intfracq  13693  flpmodeq  13708  moddiffl  13716  modmul1  13758  modmul12d  13759  modfzo0difsn  13777  modsumfzodifsn  13778  addmodlteq  13780  uzrdgxfr  13801  fzen2  13803  monoord2  13868  seqf1olem1  13876  seqf1olem2  13877  seqz  13885  expaddzlem  13940  znsqcld  13994  modexp  14067  sqoddm1div8  14072  bcm1k  14143  bcp1nk  14145  bcval5  14146  bcpasc  14149  hashfz  14255  hashfzo  14257  hashfzp1  14259  hashbclem  14277  seqcoll  14291  ccatval3  14395  ccatlid  14402  ccatass  14404  ccatalpha  14409  swrdfv0  14469  swrdfv2  14481  swrds1  14486  ccatswrd  14488  pfxfv  14502  ccatpfx  14521  swrdpfx  14527  pfxccatin12lem2  14551  spllen  14574  revccat  14586  revrev  14587  cshwidxmod  14623  cshwidxm1  14627  cshweqrep  14641  2cshwcshw  14646  cshimadifsn0  14651  swrds2m  14762  seqshft  14904  fzomaxdif  15163  climshft2  15399  iserex  15476  isercoll2  15488  serf0  15500  iseraltlem2  15502  iseraltlem3  15503  iseralt  15504  sumrblem  15531  fsumm1  15571  fsumsplitsnun  15575  fsump1  15576  fsumshftm  15601  fsumrev2  15602  telfsumo  15622  fsumparts  15626  binomlem  15649  isumshft  15659  isumsplit  15660  isum1p  15661  arisum  15680  pwdif  15688  cvgrat  15703  mertenslem1  15704  ntrivcvg  15717  ntrivcvgtail  15720  prodrblem  15747  fprodser  15767  fprodm1  15785  fprodp1  15787  fprodrev  15795  fprodmodd  15815  fallfacval3  15830  fallfacfwd  15854  0fallfac  15855  binomfallfaclem2  15858  fallfacval4  15861  fsumkthpow  15874  eirrlem  16021  sqrt2irrlem  16065  dvds2ln  16106  dvdsadd2b  16123  fsumdvds  16125  fzocongeq  16141  addmodlteqALT  16142  dvdsexp  16145  dvdsmod  16146  3dvds  16148  fprodfvdvdsd  16151  odd2np1  16158  oddm1even  16160  oexpneg  16162  mod2eq1n2dvds  16164  mulsucdiv2z  16170  zob  16176  ltoddhalfle  16178  sumodd  16205  pwp1fsum  16208  divalglem0  16210  divalglem4  16213  divalglem8  16217  divalgb  16221  divalgmod  16223  modremain  16225  flodddiv4  16230  bitsp1  16246  bitsfzo  16250  bitsmod  16251  bitsinv1lem  16256  bitsf1  16261  sadaddlem  16281  bitsres  16288  bitsuz  16289  bitsshft  16290  smumullem  16307  modgcd  16348  gcdmultipled  16350  dvdsgcdidd  16353  bezoutlem1  16355  bezoutlem2  16356  bezoutlem3  16357  bezoutlem4  16358  dvdsmulgcd  16371  rplpwr  16373  lcmid  16420  absprodnn  16429  mulgcddvds  16466  divgcdcoprm0  16476  cncongr1  16478  cncongr2  16479  rpexp  16533  qmuldeneqnum  16557  numdensq  16564  qden1elz  16567  hashdvds  16582  phiprm  16584  eulerthlem2  16589  fermltl  16591  prmdiv  16592  prmdiveq  16593  hashgcdlem  16595  odzdvds  16602  vfermltlALT  16609  modprm0  16612  modprmn0modprm0  16614  pythagtriplem6  16628  pythagtriplem7  16629  pythagtriplem15  16636  pcpremul  16650  pceulem  16652  pczpre  16654  pcdiv  16659  pcqmul  16660  pcqdiv  16664  pcexp  16666  pcaddlem  16695  pcadd  16696  fldivp1  16704  pcfac  16706  pcbc  16707  prmpwdvds  16711  prmreclem4  16726  4sqlem5  16749  4sqlem8  16752  4sqlem9  16753  4sqlem10  16754  4sqlem11  16762  4sqlem14  16765  4sqlem16  16767  4sqlem17  16768  vdwapun  16781  vdwnnlem2  16803  prmop1  16845  prmdvdsprmo  16849  prmgaplem7  16864  prmlem0  16913  mulgsubcl  18824  mulgdirlem  18840  mulgdir  18841  mulgass  18846  mulgmodid  18848  mulgsubdir  18849  psgnunilem5  19209  psgnunilem2  19210  psgnunilem4  19212  m1expaddsub  19213  psgnuni  19214  odnncl  19260  odmulg  19270  odbezout  19272  sylow1lem1  19310  sylow2alem2  19330  efgsres  19450  efgredleme  19455  efgredlemc  19457  odadd1  19556  odadd2  19557  cyggeninv  19590  gsummptshft  19643  ablfacrp  19775  pgpfac1lem3  19786  fincygsubgodd  19821  srgbinomlem3  19884  srgbinomlem4  19885  zringmulg  20801  zringlpirlem1  20807  zringlpirlem3  20809  prmirredlem  20817  zndvds0  20881  znf1o  20882  znunit  20894  cayhamlem1  22138  tgpmulg  23367  zdis  24102  uniioombllem3  24872  mbfi1fseqlem4  25006  dvexp3  25265  aareccl  25609  aalioulem1  25615  geolim3  25622  aaliou3lem2  25626  aaliou3lem6  25631  ulmshft  25672  sineq0  25803  efif1olem2  25822  igamz  26320  wilthlem1  26340  wilthlem2  26341  basellem3  26355  mumul  26453  musum  26463  musumsum  26464  muinv  26465  ppiub  26475  chtub  26483  logfac2  26488  chpchtsum  26490  dchrptlem1  26535  pcbcctr  26547  bcmono  26548  bposlem5  26559  bposlem6  26560  lgslem1  26568  lgsval2lem  26578  lgsval4a  26590  lgsneg  26592  lgsneg1  26593  lgsmod  26594  lgsdirprm  26602  lgsdir  26603  lgsdilem2  26604  lgsdi  26605  lgsne0  26606  lgsabs1  26607  lgssq  26608  lgssq2  26609  lgsmulsqcoprm  26614  lgsdirnn0  26615  lgsdinn0  26616  lgsqrlem1  26617  gausslemma2dlem1a  26636  gausslemma2dlem1  26637  gausslemma2dlem4  26640  gausslemma2dlem5a  26641  gausslemma2dlem5  26642  gausslemma2dlem6  26643  gausslemma2d  26645  lgseisenlem1  26646  lgseisenlem2  26647  lgseisenlem3  26648  lgseisenlem4  26649  lgsquadlem1  26651  lgsquad2lem1  26655  lgsquad3  26658  2lgslem1b  26663  2lgsoddprmlem2  26680  2sqlem3  26691  2sqlem4  26692  2sqlem8a  26696  2sqlem8  26697  2sqlem11  26700  2sqblem  26702  2sqn0  26705  2sqmod  26707  dchrisumlem1  26760  dchrmusum2  26765  dchrvmasumlem1  26766  dchrvmasum2lem  26767  mudivsum  26801  mulogsum  26803  mulog2sumlem2  26806  selberglem1  26816  selberglem3  26818  selberg  26819  pntpbnd2  26858  pntlemf  26876  padicabvcxp  26903  axlowdimlem14  27703  axlowdimlem16  27705  pthdadjvtx  28477  crctcshwlkn0lem4  28557  crctcshwlkn0lem5  28558  crctcshlem4  28564  crctcsh  28568  clwwlkccatlem  28732  clwwisshclwws  28758  eucrctshift  28986  fzm1ne1  31487  fzspl  31488  bcm1n  31493  fzom1ne1  31499  dvdszzq  31506  prmdvdsbc  31507  numdenneg  31508  divnumden2  31509  ltesubnnd  31513  ccatf1  31600  swrdrn3  31604  swrdf1  31605  cshwrnid  31610  cycpmco2lem3  31772  cycpmco2lem4  31773  cycpmco2lem5  31774  cycpmco2lem6  31775  cycpmco2  31777  archiabllem1  31824  archiabllem2c  31826  fermltlchr  31948  znfermltl  31949  zrhnm  32324  cnzh  32325  rezh  32326  qqhval2lem  32336  qqhghm  32343  qqhrhm  32344  qqhnm  32345  ballotlemfc0  32866  ballotlemfcc  32867  ballotlemic  32880  ballotlem1c  32881  ballotlemsgt1  32884  ballotlemsdom  32885  ballotlemsel1i  32886  ballotlemsf1o  32887  ballotlemsima  32889  ballotlemfrceq  32902  ballotlemfrcn0  32903  ballotlem1ri  32908  signsplypnf  32936  itgexpif  32993  fsum2dsub  32994  breprexplemc  33019  vtsprod  33026  circlemeth  33027  revpfxsfxrev  33483  swrdrevpfx  33484  revwlk  33492  swrdwlk  33494  divcnvlin  34096  fwddifnp1  34646  knoppndvlem2  34872  knoppndvlem7  34877  knoppndvlem14  34884  knoppndvlem16  34886  ltflcei  35962  poimirlem1  35975  poimirlem2  35976  poimirlem7  35981  poimirlem16  35990  poimirlem17  35991  poimirlem19  35993  poimirlem20  35994  poimirlem24  35998  poimirlem31  36005  poimirlem32  36006  fdc  36100  mettrifi  36112  caushft  36116  cntotbnd  36151  fzsplitnd  40336  lcmineqlem6  40387  lcmineqlem18  40399  aks4d1p1p1  40416  aks4d1p8d3  40439  aks4d1p8  40440  sticksstones10  40459  sticksstones12a  40461  sticksstones12  40462  metakunt12  40484  metakunt15  40487  metakunt16  40488  metakunt28  40500  oexpreposd  40676  exp11d  40680  numdenexp  40692  dvdsexpb  40697  mzpsubmpt  40932  lzenom  40959  diophun  40962  eqrabdioph  40966  irrapxlem2  41012  irrapxlem3  41013  pellexlem6  41023  pell1234qrreccl  41043  pellfund14  41087  rmxyneg  41110  rmxyadd  41111  rmxp1  41122  rmxm1  41124  rmym1  41125  rmxluc  41126  rmyluc  41127  rmyluc2  41128  rmxdbl  41129  rmydbl  41130  congadd  41156  congsub  41160  congabseq  41164  acongrep  41170  acongeq  41173  jm2.18  41178  jm2.19lem1  41179  jm2.19lem2  41180  jm2.19lem3  41181  jm2.22  41185  jm2.23  41186  jm2.20nn  41187  jm2.25  41189  jm2.26lem3  41191  jm2.27c  41197  nzss  42362  hashnzfz  42365  hashnzfz2  42366  hashnzfzclim  42367  uzmptshftfval  42391  sineq0ALT  42984  fzisoeu  43293  fperiodmul  43297  monoord2xrv  43478  fmul01lt1lem2  43581  sumnnodd  43626  dvdsn1add  43935  dvnmul  43939  dvnprodlem1  43942  stoweidlem11  44007  stoweidlem26  44022  dirkertrigeqlem1  44094  dirkertrigeqlem2  44095  dirkertrigeqlem3  44096  dirkertrigeq  44097  dirkeritg  44098  fourierdlem26  44129  fourierdlem48  44150  fourierdlem49  44151  fourierdlem79  44181  fourierdlem91  44193  fourierdlem103  44205  fourierdlem104  44206  fouriersw  44227  etransclem1  44231  etransclem4  44234  etransclem8  44238  etransclem9  44239  etransclem15  44245  etransclem17  44247  etransclem18  44248  etransclem20  44250  etransclem21  44251  etransclem22  44252  etransclem23  44253  etransclem24  44254  etransclem25  44255  etransclem35  44265  etransclem38  44268  etransclem41  44271  etransclem44  44274  etransclem45  44275  etransclem46  44276  etransclem47  44277  etransclem48  44278  2elfz2melfz  45305  fsumsplitsndif  45320  iccpartgtprec  45367  fargshiftf1  45388  fargshiftfo  45389  mod42tp1mod8  45549  sfprmdvdsmersenne  45550  lighneallem3  45554  lighneallem4b  45556  modexp2m1d  45559  dfodd6  45584  onego  45593  m1expoddALTV  45595  zofldiv2ALTV  45609  oddflALTV  45610  oexpnegALTV  45624  omoeALTV  45632  omeoALTV  45633  epoo  45650  emoo  45651  epee  45652  emee  45653  evensumeven  45654  evenltle  45664  even3prm2  45666  mogoldbblem  45667  fppr2odd  45678  fpprwppr  45686  fpprwpprb  45687  sbgoldbst  45725  sbgoldbaltlem2  45727  sgoldbeven3prm  45730  nnsum3primesprm  45737  nnsum4primesodd  45743  nnsum4primesoddALTV  45744  nnsum4primeseven  45747  nnsum4primesevenALTV  45748  bgoldbtbndlem2  45753  bgoldbtbndlem4  45755  bgoldbtbnd  45756  2zrngamnd  45994  2zrngacmnd  45995  2zrngagrp  45996  2zrngALT  46001  2zrngnmlid  46002  2zrngnmlid2  46004  ztprmneprm  46178  altgsumbcALT  46184  fldivmod  46359  m1modmmod  46362  zofldiv2  46372  fllogbd  46401  nnpw2blen  46421  blen1b  46429  blennngt2o2  46433  blennn0e2  46435  dig2nn1st  46446  dignn0flhalflem1  46456
  Copyright terms: Public domain W3C validator