Theorem zcnd 12701

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℂcc 11098  ℤcz 12591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-resscn 11157

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-neg 11444  df-z 12592

This theorem is referenced by:  zsupss  12961  rpnnen1lem5  13005  fzm1  13635  fzrevral  13640  fzshftral  13643  nn0disj  13672  predfz  13681  fzoss2  13716  elfzo0suble  13735  fzo0addelr  13748  elfzoext  13751  fzosubel  13753  fzosubel3  13755  fzocatel  13758  fzosplitsnm1  13769  elfzom1elp1fzo1  13796  fzom1ne1  13814  2tnp1ge0ge0  13862  quoremz  13888  intfrac2  13891  intfracq  13892  flpmodeq  13907  moddiffl  13915  modmul1  13960  modmul12d  13961  modfzo0difsn  13979  modsumfzodifsn  13980  addmodlteq  13982  uzrdgxfr  14003  fzen2  14005  monoord2  14069  seqf1olem1  14077  seqf1olem2  14078  seqz  14086  expaddzlem  14141  znsqcld  14198  modexp  14274  sqoddm1div8  14279  bcm1k  14351  bcp1nk  14353  bcval5  14354  bcpasc  14357  hashfz  14464  hashfzo  14466  hashfzp1  14468  hashbclem  14489  seqcoll  14501  ccatval3  14616  ccatlid  14624  ccatass  14626  ccatalpha  14631  swrdfv0  14687  swrdfv2  14699  swrds1  14704  ccatswrd  14706  pfxfv  14720  ccatpfx  14738  swrdpfx  14744  pfxccatin12lem2  14768  spllen  14791  revccat  14803  revrev  14804  cshwidxmod  14840  cshwidxm1  14844  cshweqrep  14858  2cshwcshw  14862  cshimadifsn0  14867  swrds2m  14978  seqshft  15122  fzomaxdif  15395  climshft2  15633  iserex  15708  isercoll2  15720  serf0  15732  iseraltlem2  15734  iseraltlem3  15735  iseralt  15736  sumrblem  15762  fsumm1  15802  fsumsplitsnun  15806  fsump1  15807  fsumshftm  15832  fsumrev2  15833  telfsumo  15854  fsumparts  15858  binomlem  15883  isumshft  15893  isumsplit  15894  isum1p  15895  arisum  15914  pwdif  15922  cvgrat  15937  mertenslem1  15938  ntrivcvg  15951  ntrivcvgtail  15954  prodrblem  15983  fprodser  16003  fprodm1  16021  fprodp1  16023  fprodrev  16031  fprodmodd  16051  fallfacval3  16066  fallfacfwd  16090  0fallfac  16091  binomfallfaclem2  16094  fallfacval4  16097  fsumkthpow  16110  eirrlem  16260  sqrt2irrlem  16304  addmulmodb  16323  dvds2ln  16347  dvdsadd2b  16364  fsumdvds  16366  fzocongeq  16382  addmodlteqALT  16383  dvdsexp  16386  dvdsmod  16387  3dvds  16389  fprodfvdvdsd  16392  odd2np1  16399  oddm1even  16401  oexpneg  16403  mod2eq1n2dvds  16405  mulsucdiv2z  16411  zob  16417  ltoddhalfle  16419  sumodd  16446  pwp1fsum  16449  divalglem0  16451  divalglem4  16454  divalglem8  16458  divalgb  16462  divalgmod  16464  modremain  16466  flodddiv4  16473  bitsp1  16489  bitsfzo  16493  bitsmod  16494  bitsinv1lem  16499  bitsf1  16504  sadaddlem  16524  bitsres  16531  bitsuz  16532  bitsshft  16533  smumullem  16550  modgcd  16590  gcdmultipled  16592  dvdsgcdidd  16595  bezoutlem1  16597  bezoutlem2  16598  bezoutlem3  16599  bezoutlem4  16600  dvdsmulgcd  16614  rplpwr  16616  lcmid  16667  absprodnn  16676  mulgcddvds  16713  divgcdcoprm0  16723  cncongr1  16725  cncongr2  16726  dvdszzq  16780  rpexp  16781  prmdvdsbc  16785  qmuldeneqnum  16806  numdensq  16813  qden1elz  16816  numdenexp  16819  hashdvds  16834  phiprm  16836  eulerthlem2  16841  fermltl  16843  prmdiv  16844  prmdiveq  16845  hashgcdlem  16847  odzdvds  16855  vfermltlALT  16862  modprm0  16865  modprmn0modprm0  16867  pythagtriplem6  16881  pythagtriplem7  16882  pythagtriplem15  16889  pcpremul  16903  pceulem  16905  pczpre  16907  pcdiv  16912  pcqmul  16913  pcqdiv  16917  pcexp  16919  pcaddlem  16948  pcadd  16949  fldivp1  16957  pcfac  16959  pcbc  16960  prmpwdvds  16964  prmreclem4  16979  4sqlem5  17002  4sqlem8  17005  4sqlem9  17006  4sqlem10  17007  4sqlem11  17015  4sqlem14  17018  4sqlem16  17020  4sqlem17  17021  vdwapun  17034  vdwnnlem2  17056  prmop1  17098  prmdvdsprmo  17102  prmgaplem7  17117  prmlem0  17165  chnlt  18679  mulgsubcl  19154  mulgdirlem  19171  mulgdir  19172  mulgass  19177  mulgmodid  19179  mulgsubdir  19180  psgnunilem5  19564  psgnunilem2  19565  psgnunilem4  19567  m1expaddsub  19568  psgnuni  19569  odnncl  19615  odmulg  19626  odbezout  19628  sylow1lem1  19668  sylow2alem2  19688  efgsres  19808  efgredleme  19813  efgredlemc  19815  odadd1  19918  odadd2  19919  cyggeninv  19953  gsummptshft  20006  ablfacrp  20138  pgpfac1lem3  20149  fincygsubgodd  20184  srgbinomlem3  20310  srgbinomlem4  20311  zringmulg  21575  zringlpirlem1  21581  zringlpirlem3  21583  prmirredlem  21591  fermltlchr  21648  zndvds0  21669  znf1o  21670  znunit  21682  cayhamlem1  22992  tgpmulg  24219  zdis  24943  uniioombllem3  25713  mbfi1fseqlem4  25846  dvexp3  26106  aareccl  26456  aalioulem1  26462  geolim3  26469  aaliou3lem2  26473  aaliou3lem6  26478  ulmshft  26519  sineq0  26655  efif1olem2  26674  igamz  27178  wilthlem1  27198  wilthlem2  27199  basellem3  27213  mumul  27311  musum  27321  musumsum  27322  muinv  27323  ppiub  27334  chtub  27342  logfac2  27347  chpchtsum  27349  dchrptlem1  27394  pcbcctr  27406  bcmono  27407  bposlem5  27418  bposlem6  27419  lgslem1  27427  lgsval2lem  27437  lgsval4a  27449  lgsneg  27451  lgsneg1  27452  lgsmod  27453  lgsdirprm  27461  lgsdir  27462  lgsdilem2  27463  lgsdi  27464  lgsne0  27465  lgsabs1  27466  lgssq  27467  lgssq2  27468  lgsmulsqcoprm  27473  lgsdirnn0  27474  lgsdinn0  27475  lgsqrlem1  27476  gausslemma2dlem1a  27495  gausslemma2dlem1  27496  gausslemma2dlem4  27499  gausslemma2dlem5a  27500  gausslemma2dlem5  27501  gausslemma2dlem6  27502  gausslemma2d  27504  lgseisenlem1  27505  lgseisenlem2  27506  lgseisenlem3  27507  lgseisenlem4  27508  lgsquadlem1  27510  lgsquad2lem1  27514  lgsquad3  27517  2lgslem1b  27522  2lgsoddprmlem2  27539  2sqlem3  27550  2sqlem4  27551  2sqlem8a  27555  2sqlem8  27556  2sqlem11  27559  2sqblem  27561  2sqn0  27564  2sqmod  27566  dchrisumlem1  27619  dchrmusum2  27624  dchrvmasumlem1  27625  dchrvmasum2lem  27626  mudivsum  27660  mulogsum  27662  mulog2sumlem2  27665  selberglem1  27675  selberglem3  27677  selberg  27678  pntpbnd2  27717  pntlemf  27735  padicabvcxp  27762  axlowdimlem14  29246  axlowdimlem16  29248  pthdadjvtx  30018  crctcshwlkn0lem4  30103  crctcshwlkn0lem5  30104  crctcshlem4  30110  crctcsh  30114  clwwlkccatlem  30281  clwwisshclwws  30307  eucrctshift  30535  fzm1ne1  33074  fzspl  33075  bcm1n  33081  elq2  33097  znumd  33098  zdend  33099  numdenneg  33100  divnumden2  33101  ltesubnnd  33108  ccatf1  33210  swrdrn3  33216  swrdf1  33217  cshwrnid  33222  gsumzrsum  33326  gsummulsubdishift1  33329  cycpmco2lem3  33389  cycpmco2lem4  33390  cycpmco2lem5  33391  cycpmco2lem6  33392  cycpmco2  33394  archiabllem1  33454  archiabllem2c  33456  elrgspnlem1  33503  elrgspnlem2  33504  znfermltl  33624  zringidom  33786  zringfrac  33789  esplyindfv  33911  zconstr  34099  cos9thpiminplylem2  34118  zrhnm  34302  cnzh  34303  rezh  34304  zrhcntr  34314  qqhval2lem  34316  qqhghm  34323  qqhrhm  34324  qqhnm  34325  ballotlemfc0  34828  ballotlemfcc  34829  ballotlemic  34842  ballotlem1c  34843  ballotlemsgt1  34846  ballotlemsdom  34847  ballotlemsel1i  34848  ballotlemsf1o  34849  ballotlemsima  34851  ballotlemfrceq  34864  ballotlemfrcn0  34865  ballotlem1ri  34870  signsplypnf  34882  itgexpif  34938  fsum2dsub  34939  breprexplemc  34964  vtsprod  34971  circlemeth  34972  revpfxsfxrev  35540  swrdrevpfx  35541  revwlk  35550  swrdwlk  35552  divcnvlin  36158  fwddifnp1  36590  knoppndvlem2  37025  knoppndvlem7  37030  knoppndvlem14  37037  knoppndvlem16  37039  ltflcei  38181  poimirlem1  38194  poimirlem2  38195  poimirlem7  38200  poimirlem16  38209  poimirlem17  38210  poimirlem19  38212  poimirlem20  38213  poimirlem24  38217  poimirlem31  38224  poimirlem32  38225  fdc  38318  mettrifi  38330  caushft  38334  cntotbnd  38369  fzsplitnd  42673  lcmineqlem6  42725  lcmineqlem18  42737  aks4d1p1p1  42754  aks4d1p8d3  42777  aks4d1p8  42778  primrootscoprmpow  42790  posbezout  42791  primrootscoprbij  42793  primrootspoweq0  42797  hashscontpow1  42812  aks6d1c3  42814  aks6d1c4  42815  aks6d1c5lem1  42827  aks6d1c5lem2  42829  sticksstones10  42846  sticksstones12a  42848  sticksstones12  42849  aks6d1c6lem3  42863  unitscyglem2  42887  unitscyglem4  42889  sumcubes  42998  oexpreposd  43007  exp11d  43011  dvdsexpb  43020  mzpsubmpt  43400  lzenom  43427  diophun  43430  eqrabdioph  43434  irrapxlem2  43476  irrapxlem3  43477  pellexlem6  43487  pell1234qrreccl  43507  pellfund14  43551  rmxyneg  43573  rmxyadd  43574  rmxp1  43585  rmxm1  43587  rmym1  43588  rmxluc  43589  rmyluc  43590  rmyluc2  43591  rmxdbl  43592  rmydbl  43593  congadd  43619  congsub  43623  congabseq  43627  acongrep  43633  acongeq  43636  jm2.18  43641  jm2.19lem1  43642  jm2.19lem2  43643  jm2.19lem3  43644  jm2.22  43648  jm2.23  43649  jm2.20nn  43650  jm2.25  43652  jm2.26lem3  43654  jm2.27c  43660  nzss  44953  hashnzfz  44956  hashnzfz2  44957  hashnzfzclim  44958  uzmptshftfval  44982  sineq0ALT  45571  fzisoeu  45945  fperiodmul  45949  monoord2xrv  46123  fmul01lt1lem2  46227  sumnnodd  46272  dvdsn1add  46579  dvnmul  46583  dvnprodlem1  46586  stoweidlem11  46651  stoweidlem26  46666  dirkertrigeqlem1  46738  dirkertrigeqlem2  46739  dirkertrigeqlem3  46740  dirkertrigeq  46741  dirkeritg  46742  fourierdlem26  46773  fourierdlem48  46794  fourierdlem49  46795  fourierdlem79  46825  fourierdlem91  46837  fourierdlem103  46849  fourierdlem104  46850  fouriersw  46871  etransclem1  46875  etransclem4  46878  etransclem8  46882  etransclem9  46883  etransclem15  46889  etransclem17  46891  etransclem18  46892  etransclem20  46894  etransclem21  46895  etransclem22  46896  etransclem23  46897  etransclem24  46898  etransclem25  46899  etransclem35  46909  etransclem38  46912  etransclem41  46915  etransclem44  46918  etransclem45  46919  etransclem46  46920  etransclem47  46921  etransclem48  46922  chnerlem2  47525  2elfz2melfz  47978  ceilbi  47997  flmrecm1  48003  fldivmod  48004  submodaddmod  48007  zplusmodne  48009  m1modne  48014  minusmod5ne  48015  submodlt  48016  minusmodnep2tmod  48019  m1modmmod  48024  modmkpkne  48027  modmknepk  48028  mod2addne  48030  modm2nep1  48032  modm1nep2  48034  modm1nem2  48035  2timesltsq  48038  fsumsplitsndif  48041  iccpartgtprec  48092  fargshiftf1  48113  fargshiftfo  48114  nprmmul3  48201  mod42tp1mod8  48277  sfprmdvdsmersenne  48278  lighneallem3  48282  lighneallem4b  48284  modexp2m1d  48287  nprmdvdsfacm1lem1  48295  ppivalnnprm  48300  dfodd6  48325  onego  48334  m1expoddALTV  48336  zofldiv2ALTV  48350  oddflALTV  48351  oexpnegALTV  48365  omoeALTV  48373  omeoALTV  48374  epoo  48391  emoo  48392  epee  48393  emee  48394  evensumeven  48395  evenltle  48405  even3prm2  48407  mogoldbblem  48408  fppr2odd  48419  fpprwppr  48427  fpprwpprb  48428  sbgoldbst  48466  sbgoldbaltlem2  48468  sgoldbeven3prm  48471  nnsum3primesprm  48478  nnsum4primesodd  48484  nnsum4primesoddALTV  48485  nnsum4primeseven  48488  nnsum4primesevenALTV  48489  bgoldbtbndlem2  48494  bgoldbtbndlem4  48496  bgoldbtbnd  48497  gpgedgvtx1  48750  gpgvtxedg0  48751  gpgvtxedg1  48752  gpg5nbgrvtx13starlem2  48760  gpg3nbgrvtx0  48764  pgnbgreunbgrlem2lem1  48802  pgnbgreunbgrlem2lem2  48803  pgnbgreunbgrlem2lem3  48804  2zrngamnd  48935  2zrngacmnd  48936  2zrngagrp  48937  2zrngALT  48942  2zrngnmlid  48943  2zrngnmlid2  48945  ztprmneprm  49046  altgsumbcALT  49052  zofldiv2  49230  fllogbd  49259  nnpw2blen  49279  blen1b  49287  blennngt2o2  49291  blennn0e2  49293  dig2nn1st  49304  dignn0flhalflem1  49314