Theorem zcnd 12680

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

Syntax hints:   → wi 4   ∈ wcel 2144  ℂcc 11073  ℤcz 12570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-resscn 11132

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-iota 6479  df-fv 6531  df-ov 7401  df-neg 11419  df-z 12571

This theorem is referenced by:  zsupss  12940  rpnnen1lem5  12984  fzm1  13614  fzrevral  13619  fzshftral  13622  nn0disj  13651  predfz  13660  fzoss2  13695  elfzo0suble  13714  fzo0addelr  13727  elfzoext  13730  fzosubel  13732  fzosubel3  13734  fzocatel  13737  fzosplitsnm1  13748  elfzom1elp1fzo1  13775  fzom1ne1  13793  2tnp1ge0ge0  13841  quoremz  13867  intfrac2  13870  intfracq  13871  flpmodeq  13886  moddiffl  13894  modmul1  13939  modmul12d  13940  modfzo0difsn  13958  modsumfzodifsn  13959  addmodlteq  13961  uzrdgxfr  13982  fzen2  13984  monoord2  14048  seqf1olem1  14056  seqf1olem2  14057  seqz  14065  expaddzlem  14120  znsqcld  14177  modexp  14253  sqoddm1div8  14258  bcm1k  14330  bcp1nk  14332  bcval5  14333  bcpasc  14336  hashfz  14442  hashfzo  14444  hashfzp1  14446  hashbclem  14467  seqcoll  14479  ccatval3  14594  ccatlid  14602  ccatass  14604  ccatalpha  14609  swrdfv0  14665  swrdfv2  14677  swrds1  14682  ccatswrd  14684  pfxfv  14698  ccatpfx  14716  swrdpfx  14722  pfxccatin12lem2  14746  spllen  14769  revccat  14781  revrev  14782  cshwidxmod  14818  cshwidxm1  14822  cshweqrep  14836  2cshwcshw  14840  cshimadifsn0  14845  swrds2m  14956  seqshft  15100  fzomaxdif  15373  climshft2  15611  iserex  15686  isercoll2  15698  serf0  15710  iseraltlem2  15712  iseraltlem3  15713  iseralt  15714  sumrblem  15740  fsumm1  15780  fsumsplitsnun  15784  fsump1  15785  fsumshftm  15810  fsumrev2  15811  telfsumo  15832  fsumparts  15836  binomlem  15861  isumshft  15871  isumsplit  15872  isum1p  15873  arisum  15892  pwdif  15900  cvgrat  15915  mertenslem1  15916  ntrivcvg  15929  ntrivcvgtail  15932  prodrblem  15961  fprodser  15981  fprodm1  15999  fprodp1  16001  fprodrev  16009  fprodmodd  16029  fallfacval3  16044  fallfacfwd  16068  0fallfac  16069  binomfallfaclem2  16072  fallfacval4  16075  fsumkthpow  16088  eirrlem  16238  sqrt2irrlem  16282  addmulmodb  16301  dvds2ln  16325  dvdsadd2b  16342  fsumdvds  16344  fzocongeq  16360  addmodlteqALT  16361  dvdsexp  16364  dvdsmod  16365  3dvds  16367  fprodfvdvdsd  16370  odd2np1  16377  oddm1even  16379  oexpneg  16381  mod2eq1n2dvds  16383  mulsucdiv2z  16389  zob  16395  ltoddhalfle  16397  sumodd  16424  pwp1fsum  16427  divalglem0  16429  divalglem4  16432  divalglem8  16436  divalgb  16440  divalgmod  16442  modremain  16444  flodddiv4  16451  bitsp1  16467  bitsfzo  16471  bitsmod  16472  bitsinv1lem  16477  bitsf1  16482  sadaddlem  16502  bitsres  16509  bitsuz  16510  bitsshft  16511  smumullem  16528  modgcd  16568  gcdmultipled  16570  dvdsgcdidd  16573  bezoutlem1  16575  bezoutlem2  16576  bezoutlem3  16577  bezoutlem4  16578  dvdsmulgcd  16592  rplpwr  16594  lcmid  16645  absprodnn  16654  mulgcddvds  16691  divgcdcoprm0  16701  cncongr1  16703  cncongr2  16704  dvdszzq  16758  rpexp  16759  prmdvdsbc  16763  qmuldeneqnum  16784  numdensq  16791  qden1elz  16794  numdenexp  16797  hashdvds  16812  phiprm  16814  eulerthlem2  16819  fermltl  16821  prmdiv  16822  prmdiveq  16823  hashgcdlem  16825  odzdvds  16833  vfermltlALT  16840  modprm0  16843  modprmn0modprm0  16845  pythagtriplem6  16859  pythagtriplem7  16860  pythagtriplem15  16867  pcpremul  16881  pceulem  16883  pczpre  16885  pcdiv  16890  pcqmul  16891  pcqdiv  16895  pcexp  16897  pcaddlem  16926  pcadd  16927  fldivp1  16935  pcfac  16937  pcbc  16938  prmpwdvds  16942  prmreclem4  16957  4sqlem5  16980  4sqlem8  16983  4sqlem9  16984  4sqlem10  16985  4sqlem11  16993  4sqlem14  16996  4sqlem16  16998  4sqlem17  16999  vdwapun  17012  vdwnnlem2  17034  prmop1  17076  prmdvdsprmo  17080  prmgaplem7  17095  prmlem0  17143  chnlt  18657  mulgsubcl  19132  mulgdirlem  19149  mulgdir  19150  mulgass  19155  mulgmodid  19157  mulgsubdir  19158  psgnunilem5  19536  psgnunilem2  19537  psgnunilem4  19539  m1expaddsub  19540  psgnuni  19541  odnncl  19587  odmulg  19598  odbezout  19600  sylow1lem1  19640  sylow2alem2  19660  efgsres  19780  efgredleme  19785  efgredlemc  19787  odadd1  19890  odadd2  19891  cyggeninv  19925  gsummptshft  19978  ablfacrp  20110  pgpfac1lem3  20121  fincygsubgodd  20156  srgbinomlem3  20280  srgbinomlem4  20281  zringmulg  21510  zringlpirlem1  21516  zringlpirlem3  21518  prmirredlem  21526  fermltlchr  21583  zndvds0  21604  znf1o  21605  znunit  21617  cayhamlem1  22928  tgpmulg  24155  zdis  24879  uniioombllem3  25649  mbfi1fseqlem4  25782  dvexp3  26042  aareccl  26392  aalioulem1  26398  geolim3  26405  aaliou3lem2  26409  aaliou3lem6  26414  ulmshft  26455  sineq0  26591  efif1olem2  26610  igamz  27114  wilthlem1  27134  wilthlem2  27135  basellem3  27149  mumul  27247  musum  27257  musumsum  27258  muinv  27259  ppiub  27270  chtub  27278  logfac2  27283  chpchtsum  27285  dchrptlem1  27330  pcbcctr  27342  bcmono  27343  bposlem5  27354  bposlem6  27355  lgslem1  27363  lgsval2lem  27373  lgsval4a  27385  lgsneg  27387  lgsneg1  27388  lgsmod  27389  lgsdirprm  27397  lgsdir  27398  lgsdilem2  27399  lgsdi  27400  lgsne0  27401  lgsabs1  27402  lgssq  27403  lgssq2  27404  lgsmulsqcoprm  27409  lgsdirnn0  27410  lgsdinn0  27411  lgsqrlem1  27412  gausslemma2dlem1a  27431  gausslemma2dlem1  27432  gausslemma2dlem4  27435  gausslemma2dlem5a  27436  gausslemma2dlem5  27437  gausslemma2dlem6  27438  gausslemma2d  27440  lgseisenlem1  27441  lgseisenlem2  27442  lgseisenlem3  27443  lgseisenlem4  27444  lgsquadlem1  27446  lgsquad2lem1  27450  lgsquad3  27453  2lgslem1b  27458  2lgsoddprmlem2  27475  2sqlem3  27486  2sqlem4  27487  2sqlem8a  27491  2sqlem8  27492  2sqlem11  27495  2sqblem  27497  2sqn0  27500  2sqmod  27502  dchrisumlem1  27555  dchrmusum2  27560  dchrvmasumlem1  27561  dchrvmasum2lem  27562  mudivsum  27596  mulogsum  27598  mulog2sumlem2  27601  selberglem1  27611  selberglem3  27613  selberg  27614  pntpbnd2  27653  pntlemf  27671  padicabvcxp  27698  axlowdimlem14  29158  axlowdimlem16  29160  pthdadjvtx  29930  crctcshwlkn0lem4  30015  crctcshwlkn0lem5  30016  crctcshlem4  30022  crctcsh  30026  clwwlkccatlem  30193  clwwisshclwws  30219  eucrctshift  30447  fzm1ne1  32992  fzspl  32993  bcm1n  32999  elq2  33016  znumd  33017  zdend  33018  numdenneg  33019  divnumden2  33020  ltesubnnd  33027  ccatf1  33129  swrdrn3  33135  swrdf1  33136  cshwrnid  33141  gsumzrsum  33247  gsummulsubdishift1  33250  cycpmco2lem3  33310  cycpmco2lem4  33311  cycpmco2lem5  33312  cycpmco2lem6  33313  cycpmco2  33315  archiabllem1  33375  archiabllem2c  33377  elrgspnlem1  33425  elrgspnlem2  33426  znfermltl  33554  zringidom  33749  zringfrac  33752  esplyindfv  33875  zconstr  34063  cos9thpiminplylem2  34082  zrhnm  34266  cnzh  34267  rezh  34268  zrhcntr  34278  qqhval2lem  34280  qqhghm  34287  qqhrhm  34288  qqhnm  34289  ballotlemfc0  34792  ballotlemfcc  34793  ballotlemic  34806  ballotlem1c  34807  ballotlemsgt1  34810  ballotlemsdom  34811  ballotlemsel1i  34812  ballotlemsf1o  34813  ballotlemsima  34815  ballotlemfrceq  34828  ballotlemfrcn0  34829  ballotlem1ri  34834  signsplypnf  34846  itgexpif  34902  fsum2dsub  34903  breprexplemc  34928  vtsprod  34935  circlemeth  34936  revpfxsfxrev  35470  swrdrevpfx  35471  revwlk  35480  swrdwlk  35482  divcnvlin  36088  fwddifnp1  36520  knoppndvlem2  36956  knoppndvlem7  36961  knoppndvlem14  36968  knoppndvlem16  36970  ltflcei  38112  poimirlem1  38125  poimirlem2  38126  poimirlem7  38131  poimirlem16  38140  poimirlem17  38141  poimirlem19  38143  poimirlem20  38144  poimirlem24  38148  poimirlem31  38155  poimirlem32  38156  fdc  38249  mettrifi  38261  caushft  38265  cntotbnd  38300  fzsplitnd  42604  lcmineqlem6  42656  lcmineqlem18  42668  aks4d1p1p1  42685  aks4d1p8d3  42708  aks4d1p8  42709  primrootscoprmpow  42721  posbezout  42722  primrootscoprbij  42724  primrootspoweq0  42728  hashscontpow1  42743  aks6d1c3  42745  aks6d1c4  42746  aks6d1c5lem1  42758  aks6d1c5lem2  42760  sticksstones10  42777  sticksstones12a  42779  sticksstones12  42780  aks6d1c6lem3  42794  unitscyglem2  42818  unitscyglem4  42820  sumcubes  42927  oexpreposd  42936  exp11d  42940  dvdsexpb  42949  mzpsubmpt  43329  lzenom  43356  diophun  43359  eqrabdioph  43363  irrapxlem2  43405  irrapxlem3  43406  pellexlem6  43416  pell1234qrreccl  43436  pellfund14  43480  rmxyneg  43502  rmxyadd  43503  rmxp1  43514  rmxm1  43516  rmym1  43517  rmxluc  43518  rmyluc  43519  rmyluc2  43520  rmxdbl  43521  rmydbl  43522  congadd  43548  congsub  43552  congabseq  43556  acongrep  43562  acongeq  43565  jm2.18  43570  jm2.19lem1  43571  jm2.19lem2  43572  jm2.19lem3  43573  jm2.22  43577  jm2.23  43578  jm2.20nn  43579  jm2.25  43581  jm2.26lem3  43583  jm2.27c  43589  nzss  44898  hashnzfz  44901  hashnzfz2  44902  hashnzfzclim  44903  uzmptshftfval  44927  sineq0ALT  45517  fzisoeu  45884  fperiodmul  45888  monoord2xrv  46062  fmul01lt1lem2  46166  sumnnodd  46211  dvdsn1add  46518  dvnmul  46522  dvnprodlem1  46525  stoweidlem11  46590  stoweidlem26  46605  dirkertrigeqlem1  46677  dirkertrigeqlem2  46678  dirkertrigeqlem3  46679  dirkertrigeq  46680  dirkeritg  46681  fourierdlem26  46712  fourierdlem48  46733  fourierdlem49  46734  fourierdlem79  46764  fourierdlem91  46776  fourierdlem103  46788  fourierdlem104  46789  fouriersw  46810  etransclem1  46814  etransclem4  46817  etransclem8  46821  etransclem9  46822  etransclem15  46828  etransclem17  46830  etransclem18  46831  etransclem20  46833  etransclem21  46834  etransclem22  46835  etransclem23  46836  etransclem24  46837  etransclem25  46838  etransclem35  46848  etransclem38  46851  etransclem41  46854  etransclem44  46857  etransclem45  46858  etransclem46  46859  etransclem47  46860  etransclem48  46861  chnerlem2  47464  2elfz2melfz  47917  ceilbi  47936  flmrecm1  47942  fldivmod  47943  submodaddmod  47946  zplusmodne  47948  m1modne  47953  minusmod5ne  47954  submodlt  47955  minusmodnep2tmod  47958  m1modmmod  47963  modmkpkne  47966  modmknepk  47967  mod2addne  47969  modm2nep1  47971  modm1nep2  47973  modm1nem2  47974  2timesltsq  47977  fsumsplitsndif  47980  iccpartgtprec  48031  fargshiftf1  48052  fargshiftfo  48053  nprmmul3  48140  mod42tp1mod8  48216  sfprmdvdsmersenne  48217  lighneallem3  48221  lighneallem4b  48223  modexp2m1d  48226  nprmdvdsfacm1lem1  48234  ppivalnnprm  48239  dfodd6  48264  onego  48273  m1expoddALTV  48275  zofldiv2ALTV  48289  oddflALTV  48290  oexpnegALTV  48304  omoeALTV  48312  omeoALTV  48313  epoo  48330  emoo  48331  epee  48332  emee  48333  evensumeven  48334  evenltle  48344  even3prm2  48346  mogoldbblem  48347  fppr2odd  48358  fpprwppr  48366  fpprwpprb  48367  sbgoldbst  48405  sbgoldbaltlem2  48407  sgoldbeven3prm  48410  nnsum3primesprm  48417  nnsum4primesodd  48423  nnsum4primesoddALTV  48424  nnsum4primeseven  48427  nnsum4primesevenALTV  48428  bgoldbtbndlem2  48433  bgoldbtbndlem4  48435  bgoldbtbnd  48436  gpgedgvtx1  48689  gpgvtxedg0  48690  gpgvtxedg1  48691  gpg5nbgrvtx13starlem2  48699  gpg3nbgrvtx0  48703  pgnbgreunbgrlem2lem1  48741  pgnbgreunbgrlem2lem2  48742  pgnbgreunbgrlem2lem3  48743  2zrngamnd  48874  2zrngacmnd  48875  2zrngagrp  48876  2zrngALT  48881  2zrngnmlid  48882  2zrngnmlid2  48884  ztprmneprm  48974  altgsumbcALT  48980  zofldiv2  49158  fllogbd  49187  nnpw2blen  49207  blen1b  49215  blennngt2o2  49219  blennn0e2  49221  dig2nn1st  49232  dignn0flhalflem1  49242