Theorem zcnd 12076

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 10524  ℤcz 11969

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-neg 10862  df-z 11970

This theorem is referenced by:  zsupss  12325  rpnnen1lem5  12368  fzm1  12982  fzrevral  12987  fzshftral  12990  nn0disj  13018  predfz  13027  fzoss2  13060  fzo0addelr  13087  fzosubel  13091  fzosubel3  13093  fzocatel  13096  fzosplitsnm1  13107  elfzom1elp1fzo1  13132  2tnp1ge0ge0  13194  quoremz  13218  intfrac2  13221  intfracq  13222  flpmodeq  13237  moddiffl  13245  modmul1  13287  modmul12d  13288  modfzo0difsn  13306  modsumfzodifsn  13307  addmodlteq  13309  uzrdgxfr  13330  fzen2  13332  monoord2  13397  seqf1olem1  13405  seqf1olem2  13406  seqz  13414  expaddzlem  13468  znsqcld  13522  modexp  13595  sqoddm1div8  13600  bcm1k  13671  bcp1nk  13673  bcval5  13674  bcpasc  13677  hashfz  13784  hashfzo  13786  hashfzp1  13788  hashbclem  13806  seqcoll  13818  ccatval3  13924  ccatlid  13931  ccatass  13933  ccatalpha  13938  swrdfv0  14002  swrdfv2  14014  swrds1  14019  ccatswrd  14021  pfxfv  14035  ccatpfx  14054  swrdpfx  14060  pfxccatin12lem2  14084  spllen  14107  revccat  14119  revrev  14120  cshwidxmod  14156  cshwidxm1  14160  cshweqrep  14174  2cshwcshw  14178  cshimadifsn0  14183  swrds2m  14294  seqshft  14436  fzomaxdif  14695  climshft2  14931  iserex  15005  isercoll2  15017  serf0  15029  iseraltlem2  15031  iseraltlem3  15032  iseralt  15033  sumrblem  15060  fsumm1  15098  fsumsplitsnun  15102  fsump1  15103  fsumshftm  15128  fsumrev2  15129  telfsumo  15149  fsumparts  15153  binomlem  15176  isumshft  15186  isumsplit  15187  isum1p  15188  arisum  15207  pwdif  15215  cvgrat  15231  mertenslem1  15232  ntrivcvg  15245  ntrivcvgtail  15248  prodrblem  15275  fprodser  15295  fprodm1  15313  fprodp1  15315  fprodrev  15323  fprodmodd  15343  fallfacval3  15358  fallfacfwd  15382  0fallfac  15383  binomfallfaclem2  15386  fallfacval4  15389  fsumkthpow  15402  eirrlem  15549  sqrt2irrlem  15593  dvds2ln  15634  dvdsadd2b  15648  fsumdvds  15650  fzocongeq  15666  addmodlteqALT  15667  dvdsexp  15669  dvdsmod  15670  3dvds  15672  fprodfvdvdsd  15675  odd2np1  15682  oddm1even  15684  oexpneg  15686  mod2eq1n2dvds  15688  mulsucdiv2z  15694  zob  15700  ltoddhalfle  15702  sumodd  15729  pwp1fsum  15732  divalglem0  15734  divalglem4  15737  divalglem8  15741  divalgb  15745  divalgmod  15747  modremain  15749  flodddiv4  15754  bitsp1  15770  bitsfzo  15774  bitsmod  15775  bitsinv1lem  15780  bitsf1  15785  sadaddlem  15805  bitsres  15812  bitsuz  15813  bitsshft  15814  smumullem  15831  modgcd  15870  gcdmultipled  15872  dvdsgcdidd  15875  bezoutlem1  15877  bezoutlem2  15878  bezoutlem3  15879  bezoutlem4  15880  dvdsmulgcd  15895  rplpwr  15897  lcmid  15943  absprodnn  15952  mulgcddvds  15989  divgcdcoprm0  15999  cncongr1  16001  cncongr2  16002  rpexp  16054  qmuldeneqnum  16077  numdensq  16084  qden1elz  16087  hashdvds  16102  phiprm  16104  eulerthlem2  16109  fermltl  16111  prmdiv  16112  prmdiveq  16113  hashgcdlem  16115  odzdvds  16122  vfermltlALT  16129  modprm0  16132  modprmn0modprm0  16134  pythagtriplem6  16148  pythagtriplem7  16149  pythagtriplem15  16156  pcpremul  16170  pceulem  16172  pczpre  16174  pcdiv  16179  pcqmul  16180  pcqdiv  16184  pcexp  16186  pcaddlem  16214  pcadd  16215  fldivp1  16223  pcfac  16225  pcbc  16226  prmpwdvds  16230  prmreclem4  16245  4sqlem5  16268  4sqlem8  16271  4sqlem9  16272  4sqlem10  16273  4sqlem11  16281  4sqlem14  16284  4sqlem16  16286  4sqlem17  16287  vdwapun  16300  vdwnnlem2  16322  prmop1  16364  prmdvdsprmo  16368  prmgaplem7  16383  prmlem0  16431  mulgsubcl  18234  mulgdirlem  18250  mulgdir  18251  mulgass  18256  mulgmodid  18258  mulgsubdir  18259  psgnunilem5  18614  psgnunilem2  18615  psgnunilem4  18617  m1expaddsub  18618  psgnuni  18619  odnncl  18665  odmulg  18675  odbezout  18677  sylow1lem1  18715  sylow2alem2  18735  efgsres  18856  efgredleme  18861  efgredlemc  18863  odadd1  18961  odadd2  18962  cyggeninv  18995  gsummptshft  19049  ablfacrp  19181  pgpfac1lem3  19192  fincygsubgodd  19227  srgbinomlem3  19285  srgbinomlem4  19286  zringmulg  20171  zringlpirlem1  20177  zringlpirlem3  20179  prmirredlem  20186  zndvds0  20242  znf1o  20243  znunit  20255  cayhamlem1  21471  tgpmulg  22698  zdis  23421  uniioombllem3  24189  mbfi1fseqlem4  24322  dvexp3  24581  aareccl  24922  aalioulem1  24928  geolim3  24935  aaliou3lem2  24939  aaliou3lem6  24944  ulmshft  24985  sineq0  25116  efif1olem2  25135  igamz  25633  wilthlem1  25653  wilthlem2  25654  basellem3  25668  mumul  25766  musum  25776  musumsum  25777  muinv  25778  ppiub  25788  chtub  25796  logfac2  25801  chpchtsum  25803  dchrptlem1  25848  pcbcctr  25860  bcmono  25861  bposlem5  25872  bposlem6  25873  lgslem1  25881  lgsval2lem  25891  lgsval4a  25903  lgsneg  25905  lgsneg1  25906  lgsmod  25907  lgsdirprm  25915  lgsdir  25916  lgsdilem2  25917  lgsdi  25918  lgsne0  25919  lgsabs1  25920  lgssq  25921  lgssq2  25922  lgsmulsqcoprm  25927  lgsdirnn0  25928  lgsdinn0  25929  lgsqrlem1  25930  gausslemma2dlem1a  25949  gausslemma2dlem1  25950  gausslemma2dlem4  25953  gausslemma2dlem5a  25954  gausslemma2dlem5  25955  gausslemma2dlem6  25956  gausslemma2d  25958  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem3  25961  lgseisenlem4  25962  lgsquadlem1  25964  lgsquad2lem1  25968  lgsquad3  25971  2lgslem1b  25976  2lgsoddprmlem2  25993  2sqlem3  26004  2sqlem4  26005  2sqlem8a  26009  2sqlem8  26010  2sqlem11  26013  2sqblem  26015  2sqn0  26018  2sqmod  26020  dchrisumlem1  26073  dchrmusum2  26078  dchrvmasumlem1  26079  dchrvmasum2lem  26080  mudivsum  26114  mulogsum  26116  mulog2sumlem2  26119  selberglem1  26129  selberglem3  26131  selberg  26132  pntpbnd2  26171  pntlemf  26189  padicabvcxp  26216  axlowdimlem14  26749  axlowdimlem16  26751  pthdadjvtx  27519  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  crctcshlem4  27606  crctcsh  27610  clwwlkccatlem  27774  clwwisshclwws  27800  eucrctshift  28028  fzm1ne1  30538  fzspl  30539  bcm1n  30544  fzom1ne1  30550  dvdszzq  30557  prmdvdsbc  30558  numdenneg  30559  divnumden2  30560  ltesubnnd  30564  ccatf1  30651  swrdrn3  30655  swrdf1  30656  cshwrnid  30661  cycpmco2lem3  30820  cycpmco2lem4  30821  cycpmco2lem5  30822  cycpmco2lem6  30823  cycpmco2  30825  archiabllem1  30872  archiabllem2c  30874  zrhnm  31320  cnzh  31321  rezh  31322  qqhval2lem  31332  qqhghm  31339  qqhrhm  31340  qqhnm  31341  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemic  31874  ballotlem1c  31875  ballotlemsgt1  31878  ballotlemsdom  31879  ballotlemsel1i  31880  ballotlemsf1o  31881  ballotlemsima  31883  ballotlemfrceq  31896  ballotlemfrcn0  31897  ballotlem1ri  31902  signsplypnf  31930  itgexpif  31987  fsum2dsub  31988  breprexplemc  32013  vtsprod  32020  circlemeth  32021  revpfxsfxrev  32475  swrdrevpfx  32476  revwlk  32484  swrdwlk  32486  divcnvlin  33077  fwddifnp1  33739  knoppndvlem2  33965  knoppndvlem7  33970  knoppndvlem14  33977  knoppndvlem16  33979  ltflcei  35045  poimirlem1  35058  poimirlem2  35059  poimirlem7  35064  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem24  35081  poimirlem31  35088  poimirlem32  35089  fdc  35183  mettrifi  35195  caushft  35199  cntotbnd  35234  fzsplitnd  39270  lcmineqlem6  39322  lcmineqlem18  39334  aks4d1p1p1  39345  metakunt12  39361  metakunt15  39364  metakunt16  39365  metakunt28  39377  oexpreposd  39487  numdenexp  39494  exp11d  39497  mzpsubmpt  39684  lzenom  39711  diophun  39714  eqrabdioph  39718  irrapxlem2  39764  irrapxlem3  39765  pellexlem6  39775  pell1234qrreccl  39795  pellfund14  39839  rmxyneg  39861  rmxyadd  39862  rmxp1  39873  rmxm1  39875  rmym1  39876  rmxluc  39877  rmyluc  39878  rmyluc2  39879  rmxdbl  39880  rmydbl  39881  congadd  39907  congsub  39911  congabseq  39915  acongrep  39921  acongeq  39924  jm2.18  39929  jm2.19lem1  39930  jm2.19lem2  39931  jm2.19lem3  39932  jm2.22  39936  jm2.23  39937  jm2.20nn  39938  jm2.25  39940  jm2.26lem3  39942  jm2.27c  39948  nzss  41021  hashnzfz  41024  hashnzfz2  41025  hashnzfzclim  41026  uzmptshftfval  41050  sineq0ALT  41643  fzisoeu  41932  fperiodmul  41936  monoord2xrv  42123  fmul01lt1lem2  42227  sumnnodd  42272  dvdsn1add  42581  dvnmul  42585  dvnprodlem1  42588  stoweidlem11  42653  stoweidlem26  42668  dirkertrigeqlem1  42740  dirkertrigeqlem2  42741  dirkertrigeqlem3  42742  dirkertrigeq  42743  dirkeritg  42744  fourierdlem26  42775  fourierdlem48  42796  fourierdlem49  42797  fourierdlem79  42827  fourierdlem91  42839  fourierdlem103  42851  fourierdlem104  42852  fouriersw  42873  etransclem1  42877  etransclem4  42880  etransclem8  42884  etransclem9  42885  etransclem15  42891  etransclem17  42893  etransclem18  42894  etransclem20  42896  etransclem21  42897  etransclem22  42898  etransclem23  42899  etransclem24  42900  etransclem25  42901  etransclem35  42911  etransclem38  42914  etransclem41  42917  etransclem44  42920  etransclem45  42921  etransclem46  42922  etransclem47  42923  etransclem48  42924  2elfz2melfz  43875  fsumsplitsndif  43890  iccpartgtprec  43937  fargshiftf1  43958  fargshiftfo  43959  mod42tp1mod8  44120  sfprmdvdsmersenne  44121  lighneallem3  44125  lighneallem4b  44127  modexp2m1d  44130  dfodd6  44155  onego  44164  m1expoddALTV  44166  zofldiv2ALTV  44180  oddflALTV  44181  oexpnegALTV  44195  omoeALTV  44203  omeoALTV  44204  epoo  44221  emoo  44222  epee  44223  emee  44224  evensumeven  44225  evenltle  44235  even3prm2  44237  mogoldbblem  44238  fppr2odd  44249  fpprwppr  44257  fpprwpprb  44258  sbgoldbst  44296  sbgoldbaltlem2  44298  sgoldbeven3prm  44301  nnsum3primesprm  44308  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbndlem2  44324  bgoldbtbndlem4  44326  bgoldbtbnd  44327  2zrngamnd  44565  2zrngacmnd  44566  2zrngagrp  44567  2zrngALT  44572  2zrngnmlid  44573  2zrngnmlid2  44575  ztprmneprm  44749  altgsumbcALT  44755  fldivmod  44932  m1modmmod  44935  zofldiv2  44945  fllogbd  44974  nnpw2blen  44994  blen1b  45002  blennngt2o2  45006  blennn0e2  45008  dig2nn1st  45019  dignn0flhalflem1  45029