Theorem zcnd 11811

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

Syntax hints:   → wi 4   ∈ wcel 2166  ℂcc 10250  ℤcz 11704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-resscn 10309

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-iota 6086  df-fv 6131  df-ov 6908  df-neg 10588  df-z 11705

This theorem is referenced by:  zsupss  12060  rpnnen1lem5  12103  fzm1  12714  fzrevral  12719  fzshftral  12722  nn0disj  12750  predfz  12759  fzoss2  12791  fzo0addelr  12818  fzosubel  12822  fzosubel3  12824  fzocatel  12827  fzosplitsnm1  12838  elfzom1elp1fzo1  12863  2tnp1ge0ge0  12925  quoremz  12949  intfrac2  12952  intfracq  12953  flpmodeq  12968  moddiffl  12976  modmul1  13018  modmul12d  13019  modfzo0difsn  13037  modsumfzodifsn  13038  addmodlteq  13040  uzrdgxfr  13061  fzen2  13063  monoord2  13126  seqf1olem1  13134  seqf1olem2  13135  seqz  13143  expaddzlem  13197  modexp  13293  sqoddm1div8  13324  bcm1k  13395  bcp1nk  13397  bcval5  13398  bcpasc  13401  hashfz  13503  hashfzo  13505  hashfzp1  13507  hashbclem  13525  seqcoll  13537  ccatval3  13639  ccatlid  13646  ccatass  13648  ccatalpha  13653  swrd0valOLD  13707  swrdfv0  13711  swrdidOLD  13715  swrd0fvOLD  13728  swrdfv2  13735  swrds1  13741  ccatswrd  13746  pfxfv  13761  ccatpfx  13780  swrdswrd0OLD  13787  swrdpfx  13788  pfxccatin12lem2  13828  spllen  13866  spllenOLD  13867  splfv1OLD  13869  splfv2a  13870  splfv2aOLD  13871  revccat  13882  revrev  13883  cshwidxmod  13924  cshwidxm1  13928  cshweqrep  13942  2cshwcshw  13946  cshimadifsn0  13951  swrds2m  14062  seqshft  14202  fzomaxdif  14460  climshft2  14690  iserex  14764  isercoll2  14776  serf0  14788  iseraltlem2  14790  iseraltlem3  14791  iseralt  14792  sumrblem  14819  fsumm1  14857  fsumsplitsnun  14861  fsump1  14862  fsumshftm  14887  fsumrev2  14888  telfsumo  14908  fsumparts  14912  binomlem  14935  isumshft  14945  isumsplit  14946  isum1p  14947  arisum  14966  cvgrat  14988  mertenslem1  14989  ntrivcvg  15002  ntrivcvgtail  15005  prodrblem  15032  fprodser  15052  fprodm1  15070  fprodp1  15072  fprodrev  15080  fprodmodd  15100  fallfacval3  15115  fallfacfwd  15139  0fallfac  15140  binomfallfaclem2  15143  fallfacval4  15146  fsumkthpow  15159  eirrlem  15306  sqrt2irrlem  15351  dvds2ln  15391  dvdsadd2b  15405  fsumdvds  15407  fzocongeq  15423  addmodlteqALT  15424  dvdsexp  15426  dvdsmod  15427  3dvds  15429  fprodfvdvdsd  15432  odd2np1  15439  oddm1even  15441  oexpneg  15443  mod2eq1n2dvds  15445  mulsucdiv2z  15451  zob  15457  ltoddhalfle  15459  sumodd  15485  pwp1fsum  15488  divalglem0  15490  divalglem4  15493  divalglem8  15497  divalgb  15501  divalgmod  15503  modremain  15505  flodddiv4  15510  bitsp1  15526  bitsfzo  15530  bitsmod  15531  bitsinv1lem  15536  bitsf1  15541  sadaddlem  15561  bitsres  15568  bitsuz  15569  bitsshft  15570  smumullem  15587  modgcd  15626  bezoutlem1  15629  bezoutlem2  15630  bezoutlem3  15631  bezoutlem4  15632  dvdsmulgcd  15647  rplpwr  15649  lcmid  15695  absprodnn  15704  mulgcddvds  15741  divgcdcoprm0  15751  cncongr1  15753  cncongr2  15754  rpexp  15803  qmuldeneqnum  15826  numdensq  15833  qden1elz  15836  hashdvds  15851  phiprm  15853  eulerthlem2  15858  fermltl  15860  prmdiv  15861  prmdiveq  15862  hashgcdlem  15864  odzdvds  15871  vfermltlALT  15878  modprm0  15881  modprmn0modprm0  15883  pythagtriplem6  15897  pythagtriplem7  15898  pythagtriplem15  15905  pcpremul  15919  pceulem  15921  pczpre  15923  pcdiv  15928  pcqmul  15929  pcqdiv  15933  pcexp  15935  pcaddlem  15963  pcadd  15964  fldivp1  15972  pcfac  15974  pcbc  15975  prmpwdvds  15979  prmreclem4  15994  4sqlem5  16017  4sqlem8  16020  4sqlem9  16021  4sqlem10  16022  4sqlem11  16030  4sqlem14  16033  4sqlem16  16035  4sqlem17  16036  vdwapun  16049  vdwnnlem2  16071  prmop1  16113  prmdvdsprmo  16117  prmgaplem7  16132  prmlem0  16178  mulgsubcl  17909  mulgdirlem  17924  mulgdir  17925  mulgass  17930  mulgmodid  17932  mulgsubdir  17933  psgnunilem5  18264  psgnunilem5OLD  18265  psgnunilem2  18266  psgnunilem4  18268  m1expaddsub  18269  psgnuni  18270  odnncl  18315  odmulg  18324  odbezout  18326  sylow1lem1  18364  sylow2alem2  18384  efgsres  18502  efgsresOLD  18503  efgredleme  18508  efgredlemc  18510  odadd1  18604  odadd2  18605  cyggeninv  18638  gsummptshft  18689  ablfacrp  18819  pgpfac1lem3  18830  srgbinomlem3  18896  srgbinomlem4  18897  zringmulg  20186  zringlpirlem1  20192  zringlpirlem3  20194  prmirredlem  20201  zndvds0  20258  znf1o  20259  znunit  20271  cayhamlem1  21041  tgpmulg  22267  zdis  22989  uniioombllem3  23751  mbfi1fseqlem4  23884  dvexp3  24140  aareccl  24480  aalioulem1  24486  geolim3  24493  aaliou3lem2  24497  aaliou3lem6  24502  ulmshft  24543  sineq0  24673  efif1olem2  24689  igamz  25187  wilthlem1  25207  wilthlem2  25208  basellem3  25222  mumul  25320  musum  25330  musumsum  25331  muinv  25332  ppiub  25342  chtub  25350  logfac2  25355  chpchtsum  25357  dchrptlem1  25402  pcbcctr  25414  bcmono  25415  bposlem5  25426  bposlem6  25427  lgslem1  25435  lgsval2lem  25445  lgsval4a  25457  lgsneg  25459  lgsneg1  25460  lgsmod  25461  lgsdirprm  25469  lgsdir  25470  lgsdilem2  25471  lgsdi  25472  lgsne0  25473  lgsabs1  25474  lgssq  25475  lgssq2  25476  lgsmulsqcoprm  25481  lgsdirnn0  25482  lgsdinn0  25483  lgsqrlem1  25484  gausslemma2dlem1a  25503  gausslemma2dlem1  25504  gausslemma2dlem4  25507  gausslemma2dlem5a  25508  gausslemma2dlem5  25509  gausslemma2dlem6  25510  gausslemma2d  25512  lgseisenlem1  25513  lgseisenlem2  25514  lgseisenlem3  25515  lgseisenlem4  25516  lgsquadlem1  25518  lgsquad2lem1  25522  lgsquad3  25525  2lgslem1b  25530  2lgsoddprmlem2  25547  2sqlem3  25558  2sqlem4  25559  2sqlem8a  25563  2sqlem8  25564  2sqlem11  25567  2sqblem  25569  dchrisumlem1  25591  dchrmusum2  25596  dchrvmasumlem1  25597  dchrvmasum2lem  25598  mudivsum  25632  mulogsum  25634  mulog2sumlem2  25637  selberglem1  25647  selberglem3  25649  selberg  25650  pntpbnd2  25689  pntlemf  25707  padicabvcxp  25734  axlowdimlem14  26254  axlowdimlem16  26256  pthdadjvtx  27032  crctcshwlkn0lem4  27112  crctcshwlkn0lem5  27113  crctcshlem4  27119  crctcsh  27123  clwwlkccatlem  27318  clwwisshclwws  27353  eucrctshift  27620  znsqcld  30059  fzspl  30097  bcm1n  30101  numdenneg  30110  divnumden2  30111  ltesubnnd  30115  2sqn0  30191  2sqmod  30193  archiabllem1  30292  archiabllem2c  30294  zrhnm  30558  cnzh  30559  rezh  30560  qqhval2lem  30570  qqhghm  30577  qqhrhm  30578  qqhnm  30579  ballotlemfc0  31100  ballotlemfcc  31101  ballotlemic  31114  ballotlem1c  31115  ballotlemsgt1  31118  ballotlemsdom  31119  ballotlemsel1i  31120  ballotlemsf1o  31121  ballotlemsima  31123  ballotlemfrceq  31136  ballotlemfrcn0  31137  ballotlem1ri  31142  signsplypnf  31174  itgexpif  31233  fsum2dsub  31234  breprexplemc  31259  vtsprod  31266  circlemeth  31267  divcnvlin  32160  fwddifnp1  32811  knoppndvlem2  33036  knoppndvlem7  33041  knoppndvlem14  33048  knoppndvlem16  33050  ltflcei  33940  poimirlem1  33954  poimirlem2  33955  poimirlem7  33960  poimirlem16  33969  poimirlem17  33970  poimirlem19  33972  poimirlem20  33973  poimirlem24  33977  poimirlem31  33984  poimirlem32  33985  fdc  34083  mettrifi  34095  caushft  34099  cntotbnd  34137  oexpreposd  38068  mzpsubmpt  38150  lzenom  38177  diophun  38181  eqrabdioph  38185  irrapxlem2  38231  irrapxlem3  38232  pellexlem6  38242  pell1234qrreccl  38262  pellfund14  38306  rmxyneg  38328  rmxyadd  38329  rmxp1  38340  rmxm1  38342  rmym1  38343  rmxluc  38344  rmyluc  38345  rmyluc2  38346  rmxdbl  38347  rmydbl  38348  congadd  38376  congsub  38380  congabseq  38384  acongrep  38390  acongeq  38393  jm2.18  38398  jm2.19lem1  38399  jm2.19lem2  38400  jm2.19lem3  38401  jm2.22  38405  jm2.23  38406  jm2.20nn  38407  jm2.25  38409  jm2.26lem3  38411  jm2.27c  38417  nzss  39356  hashnzfz  39359  hashnzfz2  39360  hashnzfzclim  39361  uzmptshftfval  39385  sineq0ALT  39991  fzisoeu  40312  fperiodmul  40316  monoord2xrv  40508  fmul01lt1lem2  40612  sumnnodd  40657  dvdsn1add  40949  dvnmul  40953  dvnprodlem1  40956  stoweidlem11  41022  stoweidlem26  41037  dirkertrigeqlem1  41109  dirkertrigeqlem2  41110  dirkertrigeqlem3  41111  dirkertrigeq  41112  dirkeritg  41113  fourierdlem26  41144  fourierdlem48  41165  fourierdlem49  41166  fourierdlem79  41196  fourierdlem91  41208  fourierdlem103  41220  fourierdlem104  41221  fouriersw  41242  etransclem1  41246  etransclem4  41249  etransclem8  41253  etransclem9  41254  etransclem15  41260  etransclem17  41262  etransclem18  41263  etransclem20  41265  etransclem21  41266  etransclem22  41267  etransclem23  41268  etransclem24  41269  etransclem25  41270  etransclem35  41280  etransclem38  41283  etransclem41  41286  etransclem44  41289  etransclem45  41290  etransclem46  41291  etransclem47  41292  etransclem48  41293  2elfz2melfz  42216  fsumsplitsndif  42231  iccpartgtprec  42244  fargshiftf1  42265  fargshiftfo  42266  pwdif  42331  mod42tp1mod8  42349  sfprmdvdsmersenne  42350  lighneallem3  42354  lighneallem4b  42356  modexp2m1d  42359  dfodd6  42380  onego  42389  m1expoddALTV  42391  zofldiv2ALTV  42404  oddflALTV  42405  oexpnegALTV  42418  omoeALTV  42426  omeoALTV  42427  epoo  42442  emoo  42443  epee  42444  emee  42445  evensumeven  42446  evenltle  42456  even3prm2  42458  mogoldbblem  42459  sbgoldbst  42496  sbgoldbaltlem2  42498  sgoldbeven3prm  42501  nnsum3primesprm  42508  nnsum4primesodd  42514  nnsum4primesoddALTV  42515  nnsum4primeseven  42518  nnsum4primesevenALTV  42519  bgoldbtbndlem2  42524  bgoldbtbndlem4  42526  bgoldbtbnd  42527  2zrngamnd  42788  2zrngacmnd  42789  2zrngagrp  42790  2zrngALT  42795  2zrngnmlid  42796  2zrngnmlid2  42798  ztprmneprm  42972  altgsumbcALT  42978  fldivmod  43160  m1modmmod  43163  zofldiv2  43172  fllogbd  43201  nnpw2blen  43221  blen1b  43229  blennngt2o2  43233  blennn0e2  43235  dig2nn1st  43246  dignn0flhalflem1  43256