Theorem zcnd 12817

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 12816	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 11350	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11211  ℤcz 12706

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-resscn 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6501  df-fv 6555  df-ov 7433  df-neg 11557  df-z 12707

This theorem is used by:  zsupss  13077  rpnnen1lem5  13122  fzm1  13754  fzrevral  13759  fzshftral  13762  nn0disj  13791  predfz  13800  fzoss2  13835  elfzo0suble  13854  fzo0addelr  13867  elfzoext  13870  fzosubel  13872  fzosubel3  13874  fzocatel  13877  fzosplitsnm1  13888  elfzom1elp1fzo1  13915  fzom1ne1  13933  2tnp1ge0ge0  13982  quoremz  14008  intfrac2  14011  intfracq  14012  flpmodeq  14027  moddiffl  14035  modmul1  14080  modmul12d  14081  modfzo0difsn  14099  modsumfzodifsn  14100  addmodlteq  14102  uzrdgxfr  14123  fzen2  14125  monoord2  14189  seqf1olem1  14197  seqf1olem2  14198  seqz  14206  expaddzlem  14261  znsqcld  14318  modexp  14395  sqoddm1div8  14400  bcm1k  14472  bcp1nk  14474  bcval5  14475  bcpasc  14478  hashfz  14585  hashfzo  14587  hashfzp1  14589  hashbclem  14610  seqcoll  14622  ccatval3  14737  ccatlid  14745  ccatass  14747  ccatf1  14749  ccatalpha  14753  swrdfv0  14811  swrdf1  14813  swrdrn3  14816  swrdfv2  14825  swrds1  14830  ccatswrd  14832  pfxfv  14846  ccatpfx  14864  swrdpfx  14870  pfxccatin12lem2  14894  spllen  14917  revccat  14929  revrev  14930  revpfxsfxrev  14931  swrdrevpfx  14932  cshwidxmod  14968  cshwidxm1  14972  cshweqrep  14986  2cshwcshw  14990  cshimadifsn0  14995  swrds2m  15107  seqshft  15253  fzomaxdif  15526  climshft2  15764  iserex  15839  isercoll2  15851  serf0  15863  iseraltlem2  15865  iseraltlem3  15866  iseralt  15867  sumrblem  15892  fsumm1  15932  fsumsplitsnun  15936  fsump1  15937  fsumshftm  15962  fsumrev2  15963  telfsumo  15984  fsumparts  15988  binomlem  16013  isumshft  16023  isumsplit  16024  isum1p  16025  arisum  16044  pwdif  16052  cvgrat  16067  mertenslem1  16068  ntrivcvg  16081  ntrivcvgtail  16084  prodrblem  16111  fprodser  16131  fprodm1  16149  fprodp1  16151  fprodrev  16159  fprodmodd  16179  fallfacval3  16194  fallfacfwd  16217  0fallfac  16218  binomfallfaclem2  16221  fallfacval4  16224  fsumkthpow  16237  eirrlem  16387  sqrt2irrlem  16431  addmulmodb  16450  dvds2ln  16474  dvdsadd2b  16491  fsumdvds  16493  fzocongeq  16509  addmodlteqALT  16510  dvdsexp  16513  dvdsmod  16514  3dvds  16516  fprodfvdvdsd  16519  odd2np1  16526  oddm1even  16528  oexpneg  16530  mod2eq1n2dvds  16532  mulsucdiv2z  16538  zob  16544  ltoddhalfle  16546  sumodd  16573  pwp1fsum  16576  divalglem0  16578  divalglem4  16581  divalglem8  16585  divalgb  16589  divalgmod  16591  modremain  16593  flodddiv4  16600  bitsp1  16616  bitsfzo  16620  bitsmod  16621  bitsinv1lem  16626  bitsf1  16631  sadaddlem  16651  bitsres  16658  bitsuz  16659  bitsshft  16660  smumullem  16677  modgcd  16720  gcdmultipled  16722  dvdsgcdidd  16725  bezoutlem1  16727  bezoutlem2  16728  bezoutlem3  16729  bezoutlem4  16730  dvdsmulgcd  16745  rplpwr  16747  lcmid  16799  absprodnn  16808  mulgcddvds  16845  divgcdcoprm0  16855  cncongr1  16857  cncongr2  16858  dvdszzq  16912  rpexp  16913  prmdvdsbc  16917  qmuldeneqnum  16938  numdensq  16945  qden1elz  16948  numdenexp  16952  hashdvds  16967  phiprm  16969  eulerthlem2  16974  fermltl  16976  prmdiv  16977  prmdiveq  16978  hashgcdlem  16980  odzdvds  16988  vfermltlALT  16995  modprm0  16998  modprmn0modprm0  17000  pythagtriplem6  17014  pythagtriplem7  17015  pythagtriplem15  17022  pcpremul  17036  pceulem  17038  pczpre  17040  pcdiv  17045  pcqmul  17046  pcqdiv  17050  pcexp  17052  pcaddlem  17081  pcadd  17082  fldivp1  17090  pcfac  17092  pcbc  17093  prmpwdvds  17097  prmreclem4  17112  4sqlem5  17135  4sqlem8  17138  4sqlem9  17139  4sqlem10  17140  4sqlem11  17148  4sqlem14  17151  4sqlem16  17153  4sqlem17  17154  vdwapun  17167  vdwnnlem2  17189  prmop1  17231  prmdvdsprmo  17235  prmgaplem7  17250  prmlem0  17298  chnlt  18812  mulgsubcl  19313  mulgdirlem  19330  mulgdir  19331  mulgass  19336  mulgmodid  19338  mulgsubdir  19339  psgnunilem5  19723  psgnunilem2  19724  psgnunilem4  19726  m1expaddsub  19727  psgnuni  19728  odnncl  19774  odmulg  19785  odbezout  19787  sylow1lem1  19827  sylow2alem2  19847  efgsres  19967  efgredleme  19972  efgredlemc  19974  odadd1  20077  odadd2  20078  cyggeninv  20112  gsummptshft  20165  ablfacrp  20297  pgpfac1lem3  20308  fincygsubgodd  20343  srgbinomlem3  20469  srgbinomlem4  20470  zringmulg  21777  zringlpirlem1  21783  zringlpirlem3  21785  prmirredlem  21793  fermltlchr  21850  zndvds0  21871  znf1o  21872  znunit  21884  cayhamlem1  23199  tgpmulg  24427  zdis  25151  uniioombllem3  25921  mbfi1fseqlem4  26054  dvexp3  26313  aareccl  26668  aalioulem1  26674  geolim3  26681  aaliou3lem2  26685  aaliou3lem6  26690  ulmshft  26732  sineq0  26867  efif1olem2  26886  igamz  27390  wilthlem1  27410  wilthlem2  27411  basellem3  27425  mumul  27523  musum  27533  musumsum  27534  muinv  27535  ppiub  27546  chtub  27554  logfac2  27559  chpchtsum  27561  dchrptlem1  27606  pcbcctr  27618  bcmono  27619  bposlem5  27630  bposlem6  27631  lgslem1  27639  lgsval2lem  27649  lgsval4a  27661  lgsneg  27663  lgsneg1  27664  lgsmod  27665  lgsdirprm  27673  lgsdir  27674  lgsdilem2  27675  lgsdi  27676  lgsne0  27677  lgsabs1  27678  lgssq  27679  lgssq2  27680  lgsmulsqcoprm  27685  lgsdirnn0  27686  lgsdinn0  27687  lgsqrlem1  27688  gausslemma2dlem1a  27707  gausslemma2dlem1  27708  gausslemma2dlem4  27711  gausslemma2dlem5a  27712  gausslemma2dlem5  27713  gausslemma2dlem6  27714  gausslemma2d  27716  lgseisenlem1  27717  lgseisenlem2  27718  lgseisenlem3  27719  lgseisenlem4  27720  lgsquadlem1  27722  lgsquad2lem1  27726  lgsquad3  27729  2lgslem1b  27734  2lgsoddprmlem2  27751  2sqlem3  27762  2sqlem4  27763  2sqlem8a  27767  2sqlem8  27768  2sqlem11  27771  2sqblem  27773  2sqn0  27776  2sqmod  27778  dchrisumlem1  27831  dchrmusum2  27836  dchrvmasumlem1  27837  dchrvmasum2lem  27838  mudivsum  27872  mulogsum  27874  mulog2sumlem2  27877  selberglem1  27887  selberglem3  27889  selberg  27890  pntpbnd2  27929  pntlemf  27947  padicabvcxp  27974  axlowdimlem14  29548  axlowdimlem16  29550  revwlk  30282  swrdwlk  30283  pthdadjvtx  30328  crctcshwlkn0lem4  30417  crctcshwlkn0lem5  30418  crctcshlem4  30424  crctcsh  30428  clwwlkccatlem  30595  clwwisshclwws  30621  eucrctshift  30859  fzm1ne1  33436  fzspl  33437  bcm1n  33443  elq2  33459  znumd  33460  zdend  33461  numdenneg  33462  divnumden2  33463  ltesubnnd  33470  cshwrnid  33578  gsumzrsum  33682  gsummulsubdishift1  33685  cycpmco2lem3  33745  cycpmco2lem4  33746  cycpmco2lem5  33747  cycpmco2lem6  33748  cycpmco2  33750  archiabllem1  33810  archiabllem2c  33812  elrgspnlem1  33859  elrgspnlem2  33860  znfermltl  33978  zringidom  34139  zringfrac  34142  esplyindfv  34264  zconstr  34452  cos9thpiminplylem2  34471  zrhnm  34655  cnzh  34656  rezh  34657  zrhcntr  34667  qqhval2lem  34669  qqhghm  34676  qqhrhm  34677  qqhnm  34678  ballotlemfc0  35181  ballotlemfcc  35182  ballotlemic  35195  ballotlem1c  35196  ballotlemsgt1  35199  ballotlemsdom  35200  ballotlemsel1i  35201  ballotlemsf1o  35202  ballotlemsima  35204  ballotlemfrceq  35217  ballotlemfrcn0  35218  ballotlem1ri  35223  signsplypnf  35235  itgexpif  35291  fsum2dsub  35292  breprexplemc  35317  vtsprod  35324  circlemeth  35325  divcnvlin  36628  fwddifnp1  37060  knoppndvlem2  37509  knoppndvlem7  37514  knoppndvlem14  37521  knoppndvlem16  37523  ltflcei  38674  poimirlem1  38682  poimirlem2  38683  poimirlem7  38688  poimirlem16  38697  poimirlem17  38698  poimirlem19  38700  poimirlem20  38701  poimirlem24  38705  poimirlem31  38712  poimirlem32  38713  fdc  38822  mettrifi  38834  caushft  38838  cntotbnd  38873  fzsplitnd  43175  lcmineqlem6  43227  lcmineqlem18  43239  aks4d1p1p1  43256  aks4d1p8d3  43279  aks4d1p8  43280  primrootscoprmpow  43292  posbezout  43293  primrootscoprbij  43295  primrootspoweq0  43299  hashscontpow1  43314  aks6d1c3  43316  aks6d1c4  43317  aks6d1c5lem1  43329  aks6d1c5lem2  43331  sticksstones10  43348  sticksstones12a  43350  sticksstones12  43351  aks6d1c6lem3  43365  unitscyglem2  43389  unitscyglem4  43391  sumcubes  43513  oexpreposd  43522  exp11d  43526  dvdsexpb  43530  mzpsubmpt  43897  lzenom  43924  diophun  43927  eqrabdioph  43931  irrapxlem2  43973  irrapxlem3  43974  pellexlem6  43984  pell1234qrreccl  44004  pellfund14  44048  rmxyneg  44070  rmxyadd  44071  rmxp1  44082  rmxm1  44084  rmym1  44085  rmxluc  44086  rmyluc  44087  rmyluc2  44088  rmxdbl  44089  rmydbl  44090  congadd  44116  congsub  44120  congabseq  44124  acongrep  44130  acongeq  44133  jm2.18  44138  jm2.19lem1  44139  jm2.19lem2  44140  jm2.19lem3  44141  jm2.22  44145  jm2.23  44146  jm2.20nn  44147  jm2.25  44149  jm2.26lem3  44151  jm2.27c  44157  nzss  45444  hashnzfz  45447  hashnzfz2  45448  hashnzfzclim  45449  uzmptshftfval  45473  sineq0ALT  46061  fzisoeu  46458  fperiodmul  46462  monoord2xrv  46635  fmul01lt1lem2  46739  sumnnodd  46784  dvdsn1add  47091  dvnmul  47095  dvnprodlem1  47098  stoweidlem11  47163  stoweidlem26  47178  dirkertrigeqlem1  47250  dirkertrigeqlem2  47251  dirkertrigeqlem3  47252  dirkertrigeq  47253  dirkeritg  47254  fourierdlem26  47285  fourierdlem48  47306  fourierdlem49  47307  fourierdlem79  47337  fourierdlem91  47349  fourierdlem103  47361  fourierdlem104  47362  fouriersw  47383  etransclem1  47387  etransclem4  47390  etransclem8  47394  etransclem9  47395  etransclem15  47401  etransclem17  47403  etransclem18  47404  etransclem20  47406  etransclem21  47407  etransclem22  47408  etransclem23  47409  etransclem24  47410  etransclem25  47411  etransclem35  47421  etransclem38  47424  etransclem41  47427  etransclem44  47430  etransclem45  47431  etransclem46  47432  etransclem47  47433  etransclem48  47434  chnerlem2  48035  2elfz2melfz  48530  ceilbi  48549  flmrecm1  48555  fldivmod  48556  submodaddmod  48559  zplusmodne  48561  m1modne  48566  minusmod5ne  48567  submodlt  48568  minusmodnep2tmod  48571  m1modmmod  48576  modmkpkne  48579  modmknepk  48580  mod2addne  48582  modm2nep1  48584  modm1nep2  48586  modm1nem2  48587  2timesltsq  48590  fsumsplitsndif  48593  iccpartgtprec  48644  fargshiftf1  48665  fargshiftfo  48666  nprmmul3  48753  mod42tp1mod8  48829  sfprmdvdsmersenne  48830  lighneallem3  48834  lighneallem4b  48836  modexp2m1d  48839  nprmdvdsfacm1lem1  48847  ppivalnnprm  48852  dfodd6  48877  onego  48886  m1expoddALTV  48888  zofldiv2ALTV  48902  oddflALTV  48903  oexpnegALTV  48917  omoeALTV  48925  omeoALTV  48926  epoo  48943  emoo  48944  epee  48945  emee  48946  evensumeven  48947  evenltle  48957  even3prm2  48959  mogoldbblem  48960  fppr2odd  48971  fpprwppr  48979  fpprwpprb  48980  sbgoldbst  49018  sbgoldbaltlem2  49020  sgoldbeven3prm  49023  nnsum3primesprm  49030  nnsum4primesodd  49036  nnsum4primesoddALTV  49037  nnsum4primeseven  49040  nnsum4primesevenALTV  49041  bgoldbtbndlem2  49046  bgoldbtbndlem4  49048  bgoldbtbnd  49049  gpgedgvtx1  49302  gpgvtxedg0  49303  gpgvtxedg1  49304  gpg5nbgrvtx13starlem2  49312  gpg3nbgrvtx0  49316  pgnbgreunbgrlem2lem1  49354  pgnbgreunbgrlem2lem2  49355  pgnbgreunbgrlem2lem3  49356  2zrngamnd  49486  2zrngacmnd  49487  2zrngagrp  49488  2zrngALT  49493  2zrngnmlid  49494  2zrngnmlid2  49496  ztprmneprm  49601  altgsumbcALT  49607  zofldiv2  49785  fllogbd  49814  nnpw2blen  49834  blen1b  49842  blennngt2o2  49846  blennn0e2  49848  dig2nn1st  49859  dignn0flhalflem1  49869