Theorem zcnd 12729

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

Step	Hyp	Ref	Expression
1		zred.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℤ)
2	1	zred 12728	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 11264	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11125  ℤcz 12618

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-resscn 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-neg 11471  df-z 12619

This theorem is used by:  zsupss  12989  rpnnen1lem5  13034  fzm1  13665  fzrevral  13670  fzshftral  13673  nn0disj  13702  predfz  13711  fzoss2  13746  elfzo0suble  13765  fzo0addelr  13778  elfzoext  13781  fzosubel  13783  fzosubel3  13785  fzocatel  13788  fzosplitsnm1  13799  elfzom1elp1fzo1  13826  fzom1ne1  13844  2tnp1ge0ge0  13893  quoremz  13919  intfrac2  13922  intfracq  13923  flpmodeq  13938  moddiffl  13946  modmul1  13991  modmul12d  13992  modfzo0difsn  14010  modsumfzodifsn  14011  addmodlteq  14013  uzrdgxfr  14034  fzen2  14036  monoord2  14100  seqf1olem1  14108  seqf1olem2  14109  seqz  14117  expaddzlem  14172  znsqcld  14229  modexp  14305  sqoddm1div8  14310  bcm1k  14382  bcp1nk  14384  bcval5  14385  bcpasc  14388  hashfz  14495  hashfzo  14497  hashfzp1  14499  hashbclem  14520  seqcoll  14532  ccatval3  14647  ccatlid  14655  ccatass  14657  ccatf1  14659  ccatalpha  14663  swrdfv0  14720  swrdf1  14722  swrdrn3  14725  swrdfv2  14734  swrds1  14739  ccatswrd  14741  pfxfv  14755  ccatpfx  14773  swrdpfx  14779  pfxccatin12lem2  14803  spllen  14826  revccat  14838  revrev  14839  revpfxsfxrev  14840  swrdrevpfx  14841  cshwidxmod  14877  cshwidxm1  14881  cshweqrep  14895  2cshwcshw  14899  cshimadifsn0  14904  swrds2m  15015  seqshft  15161  fzomaxdif  15434  climshft2  15672  iserex  15747  isercoll2  15759  serf0  15771  iseraltlem2  15773  iseraltlem3  15774  iseralt  15775  sumrblem  15800  fsumm1  15840  fsumsplitsnun  15844  fsump1  15845  fsumshftm  15870  fsumrev2  15871  telfsumo  15892  fsumparts  15896  binomlem  15921  isumshft  15931  isumsplit  15932  isum1p  15933  arisum  15952  pwdif  15960  cvgrat  15975  mertenslem1  15976  ntrivcvg  15989  ntrivcvgtail  15992  prodrblem  16019  fprodser  16039  fprodm1  16057  fprodp1  16059  fprodrev  16067  fprodmodd  16087  fallfacval3  16102  fallfacfwd  16125  0fallfac  16126  binomfallfaclem2  16129  fallfacval4  16132  fsumkthpow  16145  eirrlem  16295  sqrt2irrlem  16339  addmulmodb  16358  dvds2ln  16382  dvdsadd2b  16399  fsumdvds  16401  fzocongeq  16417  addmodlteqALT  16418  dvdsexp  16421  dvdsmod  16422  3dvds  16424  fprodfvdvdsd  16427  odd2np1  16434  oddm1even  16436  oexpneg  16438  mod2eq1n2dvds  16440  mulsucdiv2z  16446  zob  16452  ltoddhalfle  16454  sumodd  16481  pwp1fsum  16484  divalglem0  16486  divalglem4  16489  divalglem8  16493  divalgb  16497  divalgmod  16499  modremain  16501  flodddiv4  16508  bitsp1  16524  bitsfzo  16528  bitsmod  16529  bitsinv1lem  16534  bitsf1  16539  sadaddlem  16559  bitsres  16566  bitsuz  16567  bitsshft  16568  smumullem  16585  modgcd  16625  gcdmultipled  16627  dvdsgcdidd  16630  bezoutlem1  16632  bezoutlem2  16633  bezoutlem3  16634  bezoutlem4  16635  dvdsmulgcd  16649  rplpwr  16651  lcmid  16702  absprodnn  16711  mulgcddvds  16748  divgcdcoprm0  16758  cncongr1  16760  cncongr2  16761  dvdszzq  16815  rpexp  16816  prmdvdsbc  16820  qmuldeneqnum  16841  numdensq  16848  qden1elz  16851  numdenexp  16854  hashdvds  16869  phiprm  16871  eulerthlem2  16876  fermltl  16878  prmdiv  16879  prmdiveq  16880  hashgcdlem  16882  odzdvds  16890  vfermltlALT  16897  modprm0  16900  modprmn0modprm0  16902  pythagtriplem6  16916  pythagtriplem7  16917  pythagtriplem15  16924  pcpremul  16938  pceulem  16940  pczpre  16942  pcdiv  16947  pcqmul  16948  pcqdiv  16952  pcexp  16954  pcaddlem  16983  pcadd  16984  fldivp1  16992  pcfac  16994  pcbc  16995  prmpwdvds  16999  prmreclem4  17014  4sqlem5  17037  4sqlem8  17040  4sqlem9  17041  4sqlem10  17042  4sqlem11  17050  4sqlem14  17053  4sqlem16  17055  4sqlem17  17056  vdwapun  17069  vdwnnlem2  17091  prmop1  17133  prmdvdsprmo  17137  prmgaplem7  17152  prmlem0  17200  chnlt  18714  mulgsubcl  19214  mulgdirlem  19231  mulgdir  19232  mulgass  19237  mulgmodid  19239  mulgsubdir  19240  psgnunilem5  19624  psgnunilem2  19625  psgnunilem4  19627  m1expaddsub  19628  psgnuni  19629  odnncl  19675  odmulg  19686  odbezout  19688  sylow1lem1  19728  sylow2alem2  19748  efgsres  19868  efgredleme  19873  efgredlemc  19875  odadd1  19978  odadd2  19979  cyggeninv  20013  gsummptshft  20066  ablfacrp  20198  pgpfac1lem3  20209  fincygsubgodd  20244  srgbinomlem3  20370  srgbinomlem4  20371  zringmulg  21672  zringlpirlem1  21678  zringlpirlem3  21680  prmirredlem  21688  fermltlchr  21745  zndvds0  21766  znf1o  21767  znunit  21779  cayhamlem1  23094  tgpmulg  24322  zdis  25046  uniioombllem3  25816  mbfi1fseqlem4  25949  dvexp3  26208  aareccl  26565  aalioulem1  26571  geolim3  26578  aaliou3lem2  26582  aaliou3lem6  26587  ulmshft  26629  sineq0  26764  efif1olem2  26783  igamz  27287  wilthlem1  27307  wilthlem2  27308  basellem3  27322  mumul  27420  musum  27430  musumsum  27431  muinv  27432  ppiub  27443  chtub  27451  logfac2  27456  chpchtsum  27458  dchrptlem1  27503  pcbcctr  27515  bcmono  27516  bposlem5  27527  bposlem6  27528  lgslem1  27536  lgsval2lem  27546  lgsval4a  27558  lgsneg  27560  lgsneg1  27561  lgsmod  27562  lgsdirprm  27570  lgsdir  27571  lgsdilem2  27572  lgsdi  27573  lgsne0  27574  lgsabs1  27575  lgssq  27576  lgssq2  27577  lgsmulsqcoprm  27582  lgsdirnn0  27583  lgsdinn0  27584  lgsqrlem1  27585  gausslemma2dlem1a  27604  gausslemma2dlem1  27605  gausslemma2dlem4  27608  gausslemma2dlem5a  27609  gausslemma2dlem5  27610  gausslemma2dlem6  27611  gausslemma2d  27613  lgseisenlem1  27614  lgseisenlem2  27615  lgseisenlem3  27616  lgseisenlem4  27617  lgsquadlem1  27619  lgsquad2lem1  27623  lgsquad3  27626  2lgslem1b  27631  2lgsoddprmlem2  27648  2sqlem3  27659  2sqlem4  27660  2sqlem8a  27664  2sqlem8  27665  2sqlem11  27668  2sqblem  27670  2sqn0  27673  2sqmod  27675  dchrisumlem1  27728  dchrmusum2  27733  dchrvmasumlem1  27734  dchrvmasum2lem  27735  mudivsum  27769  mulogsum  27771  mulog2sumlem2  27774  selberglem1  27784  selberglem3  27786  selberg  27787  pntpbnd2  27826  pntlemf  27844  padicabvcxp  27871  axlowdimlem14  29415  axlowdimlem16  29417  revwlk  30149  swrdwlk  30150  pthdadjvtx  30195  crctcshwlkn0lem4  30284  crctcshwlkn0lem5  30285  crctcshlem4  30291  crctcsh  30295  clwwlkccatlem  30462  clwwisshclwws  30488  eucrctshift  30726  fzm1ne1  33262  fzspl  33263  bcm1n  33269  elq2  33285  znumd  33286  zdend  33287  numdenneg  33288  divnumden2  33289  ltesubnnd  33296  cshwrnid  33404  gsumzrsum  33508  gsummulsubdishift1  33511  cycpmco2lem3  33571  cycpmco2lem4  33572  cycpmco2lem5  33573  cycpmco2lem6  33574  cycpmco2  33576  archiabllem1  33636  archiabllem2c  33638  elrgspnlem1  33685  elrgspnlem2  33686  znfermltl  33804  zringidom  33964  zringfrac  33967  esplyindfv  34089  zconstr  34277  cos9thpiminplylem2  34296  zrhnm  34480  cnzh  34481  rezh  34482  zrhcntr  34492  qqhval2lem  34494  qqhghm  34501  qqhrhm  34502  qqhnm  34503  ballotlemfc0  35007  ballotlemfcc  35008  ballotlemic  35021  ballotlem1c  35022  ballotlemsgt1  35025  ballotlemsdom  35026  ballotlemsel1i  35027  ballotlemsf1o  35028  ballotlemsima  35030  ballotlemfrceq  35043  ballotlemfrcn0  35044  ballotlem1ri  35049  signsplypnf  35061  itgexpif  35117  fsum2dsub  35118  breprexplemc  35143  vtsprod  35150  circlemeth  35151  divcnvlin  36315  fwddifnp1  36748  knoppndvlem2  37213  knoppndvlem7  37218  knoppndvlem14  37225  knoppndvlem16  37227  ltflcei  38365  poimirlem1  38373  poimirlem2  38374  poimirlem7  38379  poimirlem16  38388  poimirlem17  38389  poimirlem19  38391  poimirlem20  38392  poimirlem24  38396  poimirlem31  38403  poimirlem32  38404  fdc  38498  mettrifi  38510  caushft  38514  cntotbnd  38549  fzsplitnd  42851  lcmineqlem6  42903  lcmineqlem18  42915  aks4d1p1p1  42932  aks4d1p8d3  42955  aks4d1p8  42956  primrootscoprmpow  42968  posbezout  42969  primrootscoprbij  42971  primrootspoweq0  42975  hashscontpow1  42990  aks6d1c3  42992  aks6d1c4  42993  aks6d1c5lem1  43005  aks6d1c5lem2  43007  sticksstones10  43024  sticksstones12a  43026  sticksstones12  43027  aks6d1c6lem3  43041  unitscyglem2  43065  unitscyglem4  43067  sumcubes  43191  oexpreposd  43200  exp11d  43204  dvdsexpb  43213  mzpsubmpt  43591  lzenom  43618  diophun  43621  eqrabdioph  43625  irrapxlem2  43667  irrapxlem3  43668  pellexlem6  43678  pell1234qrreccl  43698  pellfund14  43742  rmxyneg  43764  rmxyadd  43765  rmxp1  43776  rmxm1  43778  rmym1  43779  rmxluc  43780  rmyluc  43781  rmyluc2  43782  rmxdbl  43783  rmydbl  43784  congadd  43810  congsub  43814  congabseq  43818  acongrep  43824  acongeq  43827  jm2.18  43832  jm2.19lem1  43833  jm2.19lem2  43834  jm2.19lem3  43835  jm2.22  43839  jm2.23  43840  jm2.20nn  43841  jm2.25  43843  jm2.26lem3  43845  jm2.27c  43851  nzss  45144  hashnzfz  45147  hashnzfz2  45148  hashnzfzclim  45149  uzmptshftfval  45173  sineq0ALT  45762  fzisoeu  46136  fperiodmul  46140  monoord2xrv  46314  fmul01lt1lem2  46418  sumnnodd  46463  dvdsn1add  46770  dvnmul  46774  dvnprodlem1  46777  stoweidlem11  46842  stoweidlem26  46857  dirkertrigeqlem1  46929  dirkertrigeqlem2  46930  dirkertrigeqlem3  46931  dirkertrigeq  46932  dirkeritg  46933  fourierdlem26  46964  fourierdlem48  46985  fourierdlem49  46986  fourierdlem79  47016  fourierdlem91  47028  fourierdlem103  47040  fourierdlem104  47041  fouriersw  47062  etransclem1  47066  etransclem4  47069  etransclem8  47073  etransclem9  47074  etransclem15  47080  etransclem17  47082  etransclem18  47083  etransclem20  47085  etransclem21  47086  etransclem22  47087  etransclem23  47088  etransclem24  47089  etransclem25  47090  etransclem35  47100  etransclem38  47103  etransclem41  47106  etransclem44  47109  etransclem45  47110  etransclem46  47111  etransclem47  47112  etransclem48  47113  chnerlem2  47714  2elfz2melfz  48209  ceilbi  48228  flmrecm1  48234  fldivmod  48235  submodaddmod  48238  zplusmodne  48240  m1modne  48245  minusmod5ne  48246  submodlt  48247  minusmodnep2tmod  48250  m1modmmod  48255  modmkpkne  48258  modmknepk  48259  mod2addne  48261  modm2nep1  48263  modm1nep2  48265  modm1nem2  48266  2timesltsq  48269  fsumsplitsndif  48272  iccpartgtprec  48323  fargshiftf1  48344  fargshiftfo  48345  nprmmul3  48432  mod42tp1mod8  48508  sfprmdvdsmersenne  48509  lighneallem3  48513  lighneallem4b  48515  modexp2m1d  48518  nprmdvdsfacm1lem1  48526  ppivalnnprm  48531  dfodd6  48556  onego  48565  m1expoddALTV  48567  zofldiv2ALTV  48581  oddflALTV  48582  oexpnegALTV  48596  omoeALTV  48604  omeoALTV  48605  epoo  48622  emoo  48623  epee  48624  emee  48625  evensumeven  48626  evenltle  48636  even3prm2  48638  mogoldbblem  48639  fppr2odd  48650  fpprwppr  48658  fpprwpprb  48659  sbgoldbst  48697  sbgoldbaltlem2  48699  sgoldbeven3prm  48702  nnsum3primesprm  48709  nnsum4primesodd  48715  nnsum4primesoddALTV  48716  nnsum4primeseven  48719  nnsum4primesevenALTV  48720  bgoldbtbndlem2  48725  bgoldbtbndlem4  48727  bgoldbtbnd  48728  gpgedgvtx1  48981  gpgvtxedg0  48982  gpgvtxedg1  48983  gpg5nbgrvtx13starlem2  48991  gpg3nbgrvtx0  48995  pgnbgreunbgrlem2lem1  49033  pgnbgreunbgrlem2lem2  49034  pgnbgreunbgrlem2lem3  49035  2zrngamnd  49165  2zrngacmnd  49166  2zrngagrp  49167  2zrngALT  49172  2zrngnmlid  49173  2zrngnmlid2  49175  ztprmneprm  49280  altgsumbcALT  49286  zofldiv2  49464  fllogbd  49493  nnpw2blen  49513  blen1b  49521  blennngt2o2  49525  blennn0e2  49527  dig2nn1st  49538  dignn0flhalflem1  49548