Theorem zcnd 12639

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11066  ℤcz 12529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530

This theorem is referenced by:  zsupss  12896  rpnnen1lem5  12940  fzm1  13568  fzrevral  13573  fzshftral  13576  nn0disj  13605  predfz  13614  fzoss2  13648  elfzo0suble  13667  fzo0addelr  13680  elfzoext  13683  fzosubel  13685  fzosubel3  13687  fzocatel  13690  fzosplitsnm1  13701  elfzom1elp1fzo1  13728  2tnp1ge0ge0  13791  quoremz  13817  intfrac2  13820  intfracq  13821  flpmodeq  13836  moddiffl  13844  modmul1  13889  modmul12d  13890  modfzo0difsn  13908  modsumfzodifsn  13909  addmodlteq  13911  uzrdgxfr  13932  fzen2  13934  monoord2  13998  seqf1olem1  14006  seqf1olem2  14007  seqz  14015  expaddzlem  14070  znsqcld  14127  modexp  14203  sqoddm1div8  14208  bcm1k  14280  bcp1nk  14282  bcval5  14283  bcpasc  14286  hashfz  14392  hashfzo  14394  hashfzp1  14396  hashbclem  14417  seqcoll  14429  ccatval3  14544  ccatlid  14551  ccatass  14553  ccatalpha  14558  swrdfv0  14614  swrdfv2  14626  swrds1  14631  ccatswrd  14633  pfxfv  14647  ccatpfx  14666  swrdpfx  14672  pfxccatin12lem2  14696  spllen  14719  revccat  14731  revrev  14732  cshwidxmod  14768  cshwidxm1  14772  cshweqrep  14786  2cshwcshw  14791  cshimadifsn0  14796  swrds2m  14907  seqshft  15051  fzomaxdif  15310  climshft2  15548  iserex  15623  isercoll2  15635  serf0  15647  iseraltlem2  15649  iseraltlem3  15650  iseralt  15651  sumrblem  15677  fsumm1  15717  fsumsplitsnun  15721  fsump1  15722  fsumshftm  15747  fsumrev2  15748  telfsumo  15768  fsumparts  15772  binomlem  15795  isumshft  15805  isumsplit  15806  isum1p  15807  arisum  15826  pwdif  15834  cvgrat  15849  mertenslem1  15850  ntrivcvg  15863  ntrivcvgtail  15866  prodrblem  15895  fprodser  15915  fprodm1  15933  fprodp1  15935  fprodrev  15943  fprodmodd  15963  fallfacval3  15978  fallfacfwd  16002  0fallfac  16003  binomfallfaclem2  16006  fallfacval4  16009  fsumkthpow  16022  eirrlem  16172  sqrt2irrlem  16216  addmulmodb  16235  dvds2ln  16259  dvdsadd2b  16276  fsumdvds  16278  fzocongeq  16294  addmodlteqALT  16295  dvdsexp  16298  dvdsmod  16299  3dvds  16301  fprodfvdvdsd  16304  odd2np1  16311  oddm1even  16313  oexpneg  16315  mod2eq1n2dvds  16317  mulsucdiv2z  16323  zob  16329  ltoddhalfle  16331  sumodd  16358  pwp1fsum  16361  divalglem0  16363  divalglem4  16366  divalglem8  16370  divalgb  16374  divalgmod  16376  modremain  16378  flodddiv4  16385  bitsp1  16401  bitsfzo  16405  bitsmod  16406  bitsinv1lem  16411  bitsf1  16416  sadaddlem  16436  bitsres  16443  bitsuz  16444  bitsshft  16445  smumullem  16462  modgcd  16502  gcdmultipled  16504  dvdsgcdidd  16507  bezoutlem1  16509  bezoutlem2  16510  bezoutlem3  16511  bezoutlem4  16512  dvdsmulgcd  16526  rplpwr  16528  lcmid  16579  absprodnn  16588  mulgcddvds  16625  divgcdcoprm0  16635  cncongr1  16637  cncongr2  16638  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  mulgsubcl  19020  mulgdirlem  19037  mulgdir  19038  mulgass  19043  mulgmodid  19045  mulgsubdir  19046  psgnunilem5  19424  psgnunilem2  19425  psgnunilem4  19427  m1expaddsub  19428  psgnuni  19429  odnncl  19475  odmulg  19486  odbezout  19488  sylow1lem1  19528  sylow2alem2  19548  efgsres  19668  efgredleme  19673  efgredlemc  19675  odadd1  19778  odadd2  19779  cyggeninv  19813  gsummptshft  19866  ablfacrp  19998  pgpfac1lem3  20009  fincygsubgodd  20044  srgbinomlem3  20137  srgbinomlem4  20138  zringmulg  21366  zringlpirlem1  21372  zringlpirlem3  21374  prmirredlem  21382  fermltlchr  21439  zndvds0  21460  znf1o  21461  znunit  21473  cayhamlem1  22753  tgpmulg  23980  zdis  24705  uniioombllem3  25486  mbfi1fseqlem4  25619  dvexp3  25882  aareccl  26234  aalioulem1  26240  geolim3  26247  aaliou3lem2  26251  aaliou3lem6  26256  ulmshft  26299  sineq0  26433  efif1olem2  26452  igamz  26958  wilthlem1  26978  wilthlem2  26979  basellem3  26993  mumul  27091  musum  27101  musumsum  27102  muinv  27103  ppiub  27115  chtub  27123  logfac2  27128  chpchtsum  27130  dchrptlem1  27175  pcbcctr  27187  bcmono  27188  bposlem5  27199  bposlem6  27200  lgslem1  27208  lgsval2lem  27218  lgsval4a  27230  lgsneg  27232  lgsneg1  27233  lgsmod  27234  lgsdirprm  27242  lgsdir  27243  lgsdilem2  27244  lgsdi  27245  lgsne0  27246  lgsabs1  27247  lgssq  27248  lgssq2  27249  lgsmulsqcoprm  27254  lgsdirnn0  27255  lgsdinn0  27256  lgsqrlem1  27257  gausslemma2dlem1a  27276  gausslemma2dlem1  27277  gausslemma2dlem4  27280  gausslemma2dlem5a  27281  gausslemma2dlem5  27282  gausslemma2dlem6  27283  gausslemma2d  27285  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgsquadlem1  27291  lgsquad2lem1  27295  lgsquad3  27298  2lgslem1b  27303  2lgsoddprmlem2  27320  2sqlem3  27331  2sqlem4  27332  2sqlem8a  27336  2sqlem8  27337  2sqlem11  27340  2sqblem  27342  2sqn0  27345  2sqmod  27347  dchrisumlem1  27400  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasum2lem  27407  mudivsum  27441  mulogsum  27443  mulog2sumlem2  27446  selberglem1  27456  selberglem3  27458  selberg  27459  pntpbnd2  27498  pntlemf  27516  padicabvcxp  27543  axlowdimlem14  28882  axlowdimlem16  28884  pthdadjvtx  29658  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  crctcshlem4  29750  crctcsh  29754  clwwlkccatlem  29918  clwwisshclwws  29944  eucrctshift  30172  fzm1ne1  32711  fzspl  32712  bcm1n  32718  fzom1ne1  32724  elq2  32736  znumd  32737  zdend  32738  numdenneg  32739  divnumden2  32740  ltesubnnd  32747  ccatf1  32870  swrdrn3  32877  swrdf1  32878  cshwrnid  32883  chnlt  32939  gsumzrsum  32999  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2  33090  archiabllem1  33147  archiabllem2c  33149  elrgspnlem1  33193  elrgspnlem2  33194  znfermltl  33337  zringidom  33522  zringfrac  33525  zconstr  33754  cos9thpiminplylem2  33773  zrhnm  33957  cnzh  33958  rezh  33959  zrhcntr  33969  qqhval2lem  33971  qqhghm  33978  qqhrhm  33979  qqhnm  33980  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemic  34498  ballotlem1c  34499  ballotlemsgt1  34502  ballotlemsdom  34503  ballotlemsel1i  34504  ballotlemsf1o  34505  ballotlemsima  34507  ballotlemfrceq  34520  ballotlemfrcn0  34521  ballotlem1ri  34526  signsplypnf  34541  itgexpif  34597  fsum2dsub  34598  breprexplemc  34623  vtsprod  34630  circlemeth  34631  revpfxsfxrev  35103  swrdrevpfx  35104  revwlk  35112  swrdwlk  35114  divcnvlin  35720  fwddifnp1  36153  knoppndvlem2  36501  knoppndvlem7  36506  knoppndvlem14  36513  knoppndvlem16  36515  ltflcei  37602  poimirlem1  37615  poimirlem2  37616  poimirlem7  37621  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem24  37638  poimirlem31  37645  poimirlem32  37646  fdc  37739  mettrifi  37751  caushft  37755  cntotbnd  37790  fzsplitnd  41970  lcmineqlem6  42022  lcmineqlem18  42034  aks4d1p1p1  42051  aks4d1p8d3  42074  aks4d1p8  42075  primrootscoprmpow  42087  posbezout  42088  primrootscoprbij  42090  primrootspoweq0  42094  hashscontpow1  42109  aks6d1c3  42111  aks6d1c4  42112  aks6d1c5lem1  42124  aks6d1c5lem2  42126  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  aks6d1c6lem3  42160  unitscyglem2  42184  unitscyglem4  42186  sumcubes  42301  oexpreposd  42310  exp11d  42314  dvdsexpb  42323  mzpsubmpt  42731  lzenom  42758  diophun  42761  eqrabdioph  42765  irrapxlem2  42811  irrapxlem3  42812  pellexlem6  42822  pell1234qrreccl  42842  pellfund14  42886  rmxyneg  42909  rmxyadd  42910  rmxp1  42921  rmxm1  42923  rmym1  42924  rmxluc  42925  rmyluc  42926  rmyluc2  42927  rmxdbl  42928  rmydbl  42929  congadd  42955  congsub  42959  congabseq  42963  acongrep  42969  acongeq  42972  jm2.18  42977  jm2.19lem1  42978  jm2.19lem2  42979  jm2.19lem3  42980  jm2.22  42984  jm2.23  42985  jm2.20nn  42986  jm2.25  42988  jm2.26lem3  42990  jm2.27c  42996  nzss  44306  hashnzfz  44309  hashnzfz2  44310  hashnzfzclim  44311  uzmptshftfval  44335  sineq0ALT  44926  fzisoeu  45298  fperiodmul  45302  monoord2xrv  45479  fmul01lt1lem2  45583  sumnnodd  45628  dvdsn1add  45937  dvnmul  45941  dvnprodlem1  45944  stoweidlem11  46009  stoweidlem26  46024  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkeritg  46100  fourierdlem26  46131  fourierdlem48  46152  fourierdlem49  46153  fourierdlem79  46183  fourierdlem91  46195  fourierdlem103  46207  fourierdlem104  46208  fouriersw  46229  etransclem1  46233  etransclem4  46236  etransclem8  46240  etransclem9  46241  etransclem15  46247  etransclem17  46249  etransclem18  46250  etransclem20  46252  etransclem21  46253  etransclem22  46254  etransclem23  46255  etransclem24  46256  etransclem25  46257  etransclem35  46267  etransclem38  46270  etransclem41  46273  etransclem44  46276  etransclem45  46277  etransclem46  46278  etransclem47  46279  etransclem48  46280  2elfz2melfz  47319  ceilbi  47334  fldivmod  47339  submodaddmod  47342  zplusmodne  47344  m1modne  47349  minusmod5ne  47350  submodlt  47351  minusmodnep2tmod  47354  m1modmmod  47359  modmkpkne  47362  modmknepk  47363  mod2addne  47365  modm2nep1  47367  modm1nep2  47369  modm1nem2  47370  fsumsplitsndif  47374  iccpartgtprec  47421  fargshiftf1  47442  fargshiftfo  47443  mod42tp1mod8  47603  sfprmdvdsmersenne  47604  lighneallem3  47608  lighneallem4b  47610  modexp2m1d  47613  dfodd6  47638  onego  47647  m1expoddALTV  47649  zofldiv2ALTV  47663  oddflALTV  47664  oexpnegALTV  47678  omoeALTV  47686  omeoALTV  47687  epoo  47704  emoo  47705  epee  47706  emee  47707  evensumeven  47708  evenltle  47718  even3prm2  47720  mogoldbblem  47721  fppr2odd  47732  fpprwppr  47740  fpprwpprb  47741  sbgoldbst  47779  sbgoldbaltlem2  47781  sgoldbeven3prm  47784  nnsum3primesprm  47791  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbtbndlem2  47807  bgoldbtbndlem4  47809  bgoldbtbnd  47810  gpgedgvtx1  48053  gpgvtxedg0  48054  gpgvtxedg1  48055  gpg5nbgrvtx13starlem2  48063  gpg3nbgrvtx0  48067  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  2zrngamnd  48235  2zrngacmnd  48236  2zrngagrp  48237  2zrngALT  48242  2zrngnmlid  48243  2zrngnmlid2  48245  ztprmneprm  48335  altgsumbcALT  48341  zofldiv2  48520  fllogbd  48549  nnpw2blen  48569  blen1b  48577  blennngt2o2  48581  blennn0e2  48583  dig2nn1st  48594  dignn0flhalflem1  48604