Theorem zcnd 12634

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℤcz 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525

This theorem is referenced by:  zsupss  12887  rpnnen1lem5  12931  fzm1  13561  fzrevral  13566  fzshftral  13569  nn0disj  13598  predfz  13607  fzoss2  13642  elfzo0suble  13661  fzo0addelr  13674  elfzoext  13677  fzosubel  13679  fzosubel3  13681  fzocatel  13684  fzosplitsnm1  13695  elfzom1elp1fzo1  13722  fzom1ne1  13740  2tnp1ge0ge0  13788  quoremz  13814  intfrac2  13817  intfracq  13818  flpmodeq  13833  moddiffl  13841  modmul1  13886  modmul12d  13887  modfzo0difsn  13905  modsumfzodifsn  13906  addmodlteq  13908  uzrdgxfr  13929  fzen2  13931  monoord2  13995  seqf1olem1  14003  seqf1olem2  14004  seqz  14012  expaddzlem  14067  znsqcld  14124  modexp  14200  sqoddm1div8  14205  bcm1k  14277  bcp1nk  14279  bcval5  14280  bcpasc  14283  hashfz  14389  hashfzo  14391  hashfzp1  14393  hashbclem  14414  seqcoll  14426  ccatval3  14541  ccatlid  14549  ccatass  14551  ccatalpha  14556  swrdfv0  14612  swrdfv2  14624  swrds1  14629  ccatswrd  14631  pfxfv  14645  ccatpfx  14663  swrdpfx  14669  pfxccatin12lem2  14693  spllen  14716  revccat  14728  revrev  14729  cshwidxmod  14765  cshwidxm1  14769  cshweqrep  14783  2cshwcshw  14787  cshimadifsn0  14792  swrds2m  14903  seqshft  15047  fzomaxdif  15306  climshft2  15544  iserex  15619  isercoll2  15631  serf0  15643  iseraltlem2  15645  iseraltlem3  15646  iseralt  15647  sumrblem  15673  fsumm1  15713  fsumsplitsnun  15717  fsump1  15718  fsumshftm  15743  fsumrev2  15744  telfsumo  15765  fsumparts  15769  binomlem  15794  isumshft  15804  isumsplit  15805  isum1p  15806  arisum  15825  pwdif  15833  cvgrat  15848  mertenslem1  15849  ntrivcvg  15862  ntrivcvgtail  15865  prodrblem  15894  fprodser  15914  fprodm1  15932  fprodp1  15934  fprodrev  15942  fprodmodd  15962  fallfacval3  15977  fallfacfwd  16001  0fallfac  16002  binomfallfaclem2  16005  fallfacval4  16008  fsumkthpow  16021  eirrlem  16171  sqrt2irrlem  16215  addmulmodb  16234  dvds2ln  16258  dvdsadd2b  16275  fsumdvds  16277  fzocongeq  16293  addmodlteqALT  16294  dvdsexp  16297  dvdsmod  16298  3dvds  16300  fprodfvdvdsd  16303  odd2np1  16310  oddm1even  16312  oexpneg  16314  mod2eq1n2dvds  16316  mulsucdiv2z  16322  zob  16328  ltoddhalfle  16330  sumodd  16357  pwp1fsum  16360  divalglem0  16362  divalglem4  16365  divalglem8  16369  divalgb  16373  divalgmod  16375  modremain  16377  flodddiv4  16384  bitsp1  16400  bitsfzo  16404  bitsmod  16405  bitsinv1lem  16410  bitsf1  16415  sadaddlem  16435  bitsres  16442  bitsuz  16443  bitsshft  16444  smumullem  16461  modgcd  16501  gcdmultipled  16503  dvdsgcdidd  16506  bezoutlem1  16508  bezoutlem2  16509  bezoutlem3  16510  bezoutlem4  16511  dvdsmulgcd  16525  rplpwr  16527  lcmid  16578  absprodnn  16587  mulgcddvds  16624  divgcdcoprm0  16634  cncongr1  16636  cncongr2  16637  dvdszzq  16691  rpexp  16692  prmdvdsbc  16696  qmuldeneqnum  16717  numdensq  16724  qden1elz  16727  numdenexp  16730  hashdvds  16745  phiprm  16747  eulerthlem2  16752  fermltl  16754  prmdiv  16755  prmdiveq  16756  hashgcdlem  16758  odzdvds  16766  vfermltlALT  16773  modprm0  16776  modprmn0modprm0  16778  pythagtriplem6  16792  pythagtriplem7  16793  pythagtriplem15  16800  pcpremul  16814  pceulem  16816  pczpre  16818  pcdiv  16823  pcqmul  16824  pcqdiv  16828  pcexp  16830  pcaddlem  16859  pcadd  16860  fldivp1  16868  pcfac  16870  pcbc  16871  prmpwdvds  16875  prmreclem4  16890  4sqlem5  16913  4sqlem8  16916  4sqlem9  16917  4sqlem10  16918  4sqlem11  16926  4sqlem14  16929  4sqlem16  16931  4sqlem17  16932  vdwapun  16945  vdwnnlem2  16967  prmop1  17009  prmdvdsprmo  17013  prmgaplem7  17028  prmlem0  17076  chnlt  18589  mulgsubcl  19064  mulgdirlem  19081  mulgdir  19082  mulgass  19087  mulgmodid  19089  mulgsubdir  19090  psgnunilem5  19469  psgnunilem2  19470  psgnunilem4  19472  m1expaddsub  19473  psgnuni  19474  odnncl  19520  odmulg  19531  odbezout  19533  sylow1lem1  19573  sylow2alem2  19593  efgsres  19713  efgredleme  19718  efgredlemc  19720  odadd1  19823  odadd2  19824  cyggeninv  19858  gsummptshft  19911  ablfacrp  20043  pgpfac1lem3  20054  fincygsubgodd  20089  srgbinomlem3  20209  srgbinomlem4  20210  zringmulg  21436  zringlpirlem1  21442  zringlpirlem3  21444  prmirredlem  21452  fermltlchr  21509  zndvds0  21530  znf1o  21531  znunit  21543  cayhamlem1  22831  tgpmulg  24058  zdis  24782  uniioombllem3  25552  mbfi1fseqlem4  25685  dvexp3  25945  aareccl  26292  aalioulem1  26298  geolim3  26305  aaliou3lem2  26309  aaliou3lem6  26314  ulmshft  26355  sineq0  26488  efif1olem2  26507  igamz  27011  wilthlem1  27031  wilthlem2  27032  basellem3  27046  mumul  27144  musum  27154  musumsum  27155  muinv  27156  ppiub  27167  chtub  27175  logfac2  27180  chpchtsum  27182  dchrptlem1  27227  pcbcctr  27239  bcmono  27240  bposlem5  27251  bposlem6  27252  lgslem1  27260  lgsval2lem  27270  lgsval4a  27282  lgsneg  27284  lgsneg1  27285  lgsmod  27286  lgsdirprm  27294  lgsdir  27295  lgsdilem2  27296  lgsdi  27297  lgsne0  27298  lgsabs1  27299  lgssq  27300  lgssq2  27301  lgsmulsqcoprm  27306  lgsdirnn0  27307  lgsdinn0  27308  lgsqrlem1  27309  gausslemma2dlem1a  27328  gausslemma2dlem1  27329  gausslemma2dlem4  27332  gausslemma2dlem5a  27333  gausslemma2dlem5  27334  gausslemma2dlem6  27335  gausslemma2d  27337  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgsquadlem1  27343  lgsquad2lem1  27347  lgsquad3  27350  2lgslem1b  27355  2lgsoddprmlem2  27372  2sqlem3  27383  2sqlem4  27384  2sqlem8a  27388  2sqlem8  27389  2sqlem11  27392  2sqblem  27394  2sqn0  27397  2sqmod  27399  dchrisumlem1  27452  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasum2lem  27459  mudivsum  27493  mulogsum  27495  mulog2sumlem2  27498  selberglem1  27508  selberglem3  27510  selberg  27511  pntpbnd2  27550  pntlemf  27568  padicabvcxp  27595  axlowdimlem14  29024  axlowdimlem16  29026  pthdadjvtx  29796  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshlem4  29888  crctcsh  29892  clwwlkccatlem  30059  clwwisshclwws  30085  eucrctshift  30313  fzm1ne1  32861  fzspl  32862  bcm1n  32868  elq2  32885  znumd  32886  zdend  32887  numdenneg  32888  divnumden2  32889  ltesubnnd  32896  ccatf1  33009  swrdrn3  33015  swrdf1  33016  cshwrnid  33021  gsumzrsum  33126  gsummulsubdishift1  33129  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2  33194  archiabllem1  33254  archiabllem2c  33256  elrgspnlem1  33303  elrgspnlem2  33304  znfermltl  33426  zringidom  33611  zringfrac  33614  esplyindfv  33720  zconstr  33908  cos9thpiminplylem2  33927  zrhnm  34111  cnzh  34112  rezh  34113  zrhcntr  34123  qqhval2lem  34125  qqhghm  34132  qqhrhm  34133  qqhnm  34134  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemic  34651  ballotlem1c  34652  ballotlemsgt1  34655  ballotlemsdom  34656  ballotlemsel1i  34657  ballotlemsf1o  34658  ballotlemsima  34660  ballotlemfrceq  34673  ballotlemfrcn0  34674  ballotlem1ri  34679  signsplypnf  34694  itgexpif  34750  fsum2dsub  34751  breprexplemc  34776  vtsprod  34783  circlemeth  34784  revpfxsfxrev  35298  swrdrevpfx  35299  revwlk  35307  swrdwlk  35309  divcnvlin  35915  fwddifnp1  36347  knoppndvlem2  36773  knoppndvlem7  36778  knoppndvlem14  36785  knoppndvlem16  36787  ltflcei  37929  poimirlem1  37942  poimirlem2  37943  poimirlem7  37948  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem24  37965  poimirlem31  37972  poimirlem32  37973  fdc  38066  mettrifi  38078  caushft  38082  cntotbnd  38117  fzsplitnd  42421  lcmineqlem6  42473  lcmineqlem18  42485  aks4d1p1p1  42502  aks4d1p8d3  42525  aks4d1p8  42526  primrootscoprmpow  42538  posbezout  42539  primrootscoprbij  42541  primrootspoweq0  42545  hashscontpow1  42560  aks6d1c3  42562  aks6d1c4  42563  aks6d1c5lem1  42575  aks6d1c5lem2  42577  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  aks6d1c6lem3  42611  unitscyglem2  42635  unitscyglem4  42637  sumcubes  42745  oexpreposd  42754  exp11d  42758  dvdsexpb  42767  mzpsubmpt  43175  lzenom  43202  diophun  43205  eqrabdioph  43209  irrapxlem2  43251  irrapxlem3  43252  pellexlem6  43262  pell1234qrreccl  43282  pellfund14  43326  rmxyneg  43348  rmxyadd  43349  rmxp1  43360  rmxm1  43362  rmym1  43363  rmxluc  43364  rmyluc  43365  rmyluc2  43366  rmxdbl  43367  rmydbl  43368  congadd  43394  congsub  43398  congabseq  43402  acongrep  43408  acongeq  43411  jm2.18  43416  jm2.19lem1  43417  jm2.19lem2  43418  jm2.19lem3  43419  jm2.22  43423  jm2.23  43424  jm2.20nn  43425  jm2.25  43427  jm2.26lem3  43429  jm2.27c  43435  nzss  44744  hashnzfz  44747  hashnzfz2  44748  hashnzfzclim  44749  uzmptshftfval  44773  sineq0ALT  45363  fzisoeu  45733  fperiodmul  45737  monoord2xrv  45911  fmul01lt1lem2  46015  sumnnodd  46060  dvdsn1add  46367  dvnmul  46371  dvnprodlem1  46374  stoweidlem11  46439  stoweidlem26  46454  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkeritg  46530  fourierdlem26  46561  fourierdlem48  46582  fourierdlem49  46583  fourierdlem79  46613  fourierdlem91  46625  fourierdlem103  46637  fourierdlem104  46638  fouriersw  46659  etransclem1  46663  etransclem4  46666  etransclem8  46670  etransclem9  46671  etransclem15  46677  etransclem17  46679  etransclem18  46680  etransclem20  46682  etransclem21  46683  etransclem22  46684  etransclem23  46685  etransclem24  46686  etransclem25  46687  etransclem35  46697  etransclem38  46700  etransclem41  46703  etransclem44  46706  etransclem45  46707  etransclem46  46708  etransclem47  46709  etransclem48  46710  chnerlem2  47313  2elfz2melfz  47766  ceilbi  47785  flmrecm1  47791  fldivmod  47792  submodaddmod  47795  zplusmodne  47797  m1modne  47802  minusmod5ne  47803  submodlt  47804  minusmodnep2tmod  47807  m1modmmod  47812  modmkpkne  47815  modmknepk  47816  mod2addne  47818  modm2nep1  47820  modm1nep2  47822  modm1nem2  47823  2timesltsq  47826  fsumsplitsndif  47829  iccpartgtprec  47880  fargshiftf1  47901  fargshiftfo  47902  nprmmul3  47989  mod42tp1mod8  48065  sfprmdvdsmersenne  48066  lighneallem3  48070  lighneallem4b  48072  modexp2m1d  48075  nprmdvdsfacm1lem1  48083  ppivalnnprm  48088  dfodd6  48113  onego  48122  m1expoddALTV  48124  zofldiv2ALTV  48138  oddflALTV  48139  oexpnegALTV  48153  omoeALTV  48161  omeoALTV  48162  epoo  48179  emoo  48180  epee  48181  emee  48182  evensumeven  48183  evenltle  48193  even3prm2  48195  mogoldbblem  48196  fppr2odd  48207  fpprwppr  48215  fpprwpprb  48216  sbgoldbst  48254  sbgoldbaltlem2  48256  sgoldbeven3prm  48259  nnsum3primesprm  48266  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  bgoldbtbndlem2  48282  bgoldbtbndlem4  48284  bgoldbtbnd  48285  gpgedgvtx1  48538  gpgvtxedg0  48539  gpgvtxedg1  48540  gpg5nbgrvtx13starlem2  48548  gpg3nbgrvtx0  48552  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  2zrngamnd  48723  2zrngacmnd  48724  2zrngagrp  48725  2zrngALT  48730  2zrngnmlid  48731  2zrngnmlid2  48733  ztprmneprm  48823  altgsumbcALT  48829  zofldiv2  49007  fllogbd  49036  nnpw2blen  49056  blen1b  49064  blennngt2o2  49068  blennn0e2  49070  dig2nn1st  49081  dignn0flhalflem1  49091