Theorem zcnd 12581

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11007  ℤcz 12471

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 11066

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-neg 11350  df-z 12472

This theorem is referenced by:  zsupss  12838  rpnnen1lem5  12882  fzm1  13510  fzrevral  13515  fzshftral  13518  nn0disj  13547  predfz  13556  fzoss2  13590  elfzo0suble  13609  fzo0addelr  13622  elfzoext  13625  fzosubel  13627  fzosubel3  13629  fzocatel  13632  fzosplitsnm1  13643  elfzom1elp1fzo1  13670  2tnp1ge0ge0  13733  quoremz  13759  intfrac2  13762  intfracq  13763  flpmodeq  13778  moddiffl  13786  modmul1  13831  modmul12d  13832  modfzo0difsn  13850  modsumfzodifsn  13851  addmodlteq  13853  uzrdgxfr  13874  fzen2  13876  monoord2  13940  seqf1olem1  13948  seqf1olem2  13949  seqz  13957  expaddzlem  14012  znsqcld  14069  modexp  14145  sqoddm1div8  14150  bcm1k  14222  bcp1nk  14224  bcval5  14225  bcpasc  14228  hashfz  14334  hashfzo  14336  hashfzp1  14338  hashbclem  14359  seqcoll  14371  ccatval3  14486  ccatlid  14493  ccatass  14495  ccatalpha  14500  swrdfv0  14556  swrdfv2  14568  swrds1  14573  ccatswrd  14575  pfxfv  14589  ccatpfx  14607  swrdpfx  14613  pfxccatin12lem2  14637  spllen  14660  revccat  14672  revrev  14673  cshwidxmod  14709  cshwidxm1  14713  cshweqrep  14727  2cshwcshw  14732  cshimadifsn0  14737  swrds2m  14848  seqshft  14992  fzomaxdif  15251  climshft2  15489  iserex  15564  isercoll2  15576  serf0  15588  iseraltlem2  15590  iseraltlem3  15591  iseralt  15592  sumrblem  15618  fsumm1  15658  fsumsplitsnun  15662  fsump1  15663  fsumshftm  15688  fsumrev2  15689  telfsumo  15709  fsumparts  15713  binomlem  15736  isumshft  15746  isumsplit  15747  isum1p  15748  arisum  15767  pwdif  15775  cvgrat  15790  mertenslem1  15791  ntrivcvg  15804  ntrivcvgtail  15807  prodrblem  15836  fprodser  15856  fprodm1  15874  fprodp1  15876  fprodrev  15884  fprodmodd  15904  fallfacval3  15919  fallfacfwd  15943  0fallfac  15944  binomfallfaclem2  15947  fallfacval4  15950  fsumkthpow  15963  eirrlem  16113  sqrt2irrlem  16157  addmulmodb  16176  dvds2ln  16200  dvdsadd2b  16217  fsumdvds  16219  fzocongeq  16235  addmodlteqALT  16236  dvdsexp  16239  dvdsmod  16240  3dvds  16242  fprodfvdvdsd  16245  odd2np1  16252  oddm1even  16254  oexpneg  16256  mod2eq1n2dvds  16258  mulsucdiv2z  16264  zob  16270  ltoddhalfle  16272  sumodd  16299  pwp1fsum  16302  divalglem0  16304  divalglem4  16307  divalglem8  16311  divalgb  16315  divalgmod  16317  modremain  16319  flodddiv4  16326  bitsp1  16342  bitsfzo  16346  bitsmod  16347  bitsinv1lem  16352  bitsf1  16357  sadaddlem  16377  bitsres  16384  bitsuz  16385  bitsshft  16386  smumullem  16403  modgcd  16443  gcdmultipled  16445  dvdsgcdidd  16448  bezoutlem1  16450  bezoutlem2  16451  bezoutlem3  16452  bezoutlem4  16453  dvdsmulgcd  16467  rplpwr  16469  lcmid  16520  absprodnn  16529  mulgcddvds  16566  divgcdcoprm0  16576  cncongr1  16578  cncongr2  16579  dvdszzq  16632  rpexp  16633  prmdvdsbc  16637  qmuldeneqnum  16658  numdensq  16665  qden1elz  16668  numdenexp  16671  hashdvds  16686  phiprm  16688  eulerthlem2  16693  fermltl  16695  prmdiv  16696  prmdiveq  16697  hashgcdlem  16699  odzdvds  16707  vfermltlALT  16714  modprm0  16717  modprmn0modprm0  16719  pythagtriplem6  16733  pythagtriplem7  16734  pythagtriplem15  16741  pcpremul  16755  pceulem  16757  pczpre  16759  pcdiv  16764  pcqmul  16765  pcqdiv  16769  pcexp  16771  pcaddlem  16800  pcadd  16801  fldivp1  16809  pcfac  16811  pcbc  16812  prmpwdvds  16816  prmreclem4  16831  4sqlem5  16854  4sqlem8  16857  4sqlem9  16858  4sqlem10  16859  4sqlem11  16867  4sqlem14  16870  4sqlem16  16872  4sqlem17  16873  vdwapun  16886  vdwnnlem2  16908  prmop1  16950  prmdvdsprmo  16954  prmgaplem7  16969  prmlem0  17017  mulgsubcl  18967  mulgdirlem  18984  mulgdir  18985  mulgass  18990  mulgmodid  18992  mulgsubdir  18993  psgnunilem5  19373  psgnunilem2  19374  psgnunilem4  19376  m1expaddsub  19377  psgnuni  19378  odnncl  19424  odmulg  19435  odbezout  19437  sylow1lem1  19477  sylow2alem2  19497  efgsres  19617  efgredleme  19622  efgredlemc  19624  odadd1  19727  odadd2  19728  cyggeninv  19762  gsummptshft  19815  ablfacrp  19947  pgpfac1lem3  19958  fincygsubgodd  19993  srgbinomlem3  20113  srgbinomlem4  20114  zringmulg  21363  zringlpirlem1  21369  zringlpirlem3  21371  prmirredlem  21379  fermltlchr  21436  zndvds0  21457  znf1o  21458  znunit  21470  cayhamlem1  22751  tgpmulg  23978  zdis  24703  uniioombllem3  25484  mbfi1fseqlem4  25617  dvexp3  25880  aareccl  26232  aalioulem1  26238  geolim3  26245  aaliou3lem2  26249  aaliou3lem6  26254  ulmshft  26297  sineq0  26431  efif1olem2  26450  igamz  26956  wilthlem1  26976  wilthlem2  26977  basellem3  26991  mumul  27089  musum  27099  musumsum  27100  muinv  27101  ppiub  27113  chtub  27121  logfac2  27126  chpchtsum  27128  dchrptlem1  27173  pcbcctr  27185  bcmono  27186  bposlem5  27197  bposlem6  27198  lgslem1  27206  lgsval2lem  27216  lgsval4a  27228  lgsneg  27230  lgsneg1  27231  lgsmod  27232  lgsdirprm  27240  lgsdir  27241  lgsdilem2  27242  lgsdi  27243  lgsne0  27244  lgsabs1  27245  lgssq  27246  lgssq2  27247  lgsmulsqcoprm  27252  lgsdirnn0  27253  lgsdinn0  27254  lgsqrlem1  27255  gausslemma2dlem1a  27274  gausslemma2dlem1  27275  gausslemma2dlem4  27278  gausslemma2dlem5a  27279  gausslemma2dlem5  27280  gausslemma2dlem6  27281  gausslemma2d  27283  lgseisenlem1  27284  lgseisenlem2  27285  lgseisenlem3  27286  lgseisenlem4  27287  lgsquadlem1  27289  lgsquad2lem1  27293  lgsquad3  27296  2lgslem1b  27301  2lgsoddprmlem2  27318  2sqlem3  27329  2sqlem4  27330  2sqlem8a  27334  2sqlem8  27335  2sqlem11  27338  2sqblem  27340  2sqn0  27343  2sqmod  27345  dchrisumlem1  27398  dchrmusum2  27403  dchrvmasumlem1  27404  dchrvmasum2lem  27405  mudivsum  27439  mulogsum  27441  mulog2sumlem2  27444  selberglem1  27454  selberglem3  27456  selberg  27457  pntpbnd2  27496  pntlemf  27514  padicabvcxp  27541  axlowdimlem14  28900  axlowdimlem16  28902  pthdadjvtx  29673  crctcshwlkn0lem4  29758  crctcshwlkn0lem5  29759  crctcshlem4  29765  crctcsh  29769  clwwlkccatlem  29933  clwwisshclwws  29959  eucrctshift  30187  fzm1ne1  32732  fzspl  32733  bcm1n  32739  fzom1ne1  32745  elq2  32757  znumd  32758  zdend  32759  numdenneg  32760  divnumden2  32761  ltesubnnd  32768  ccatf1  32891  swrdrn3  32898  swrdf1  32899  cshwrnid  32904  chnlt  32956  gsumzrsum  33013  cycpmco2lem3  33071  cycpmco2lem4  33072  cycpmco2lem5  33073  cycpmco2lem6  33074  cycpmco2  33076  archiabllem1  33136  archiabllem2c  33138  elrgspnlem1  33183  elrgspnlem2  33184  znfermltl  33304  zringidom  33489  zringfrac  33492  zconstr  33737  cos9thpiminplylem2  33756  zrhnm  33940  cnzh  33941  rezh  33942  zrhcntr  33952  qqhval2lem  33954  qqhghm  33961  qqhrhm  33962  qqhnm  33963  ballotlemfc0  34467  ballotlemfcc  34468  ballotlemic  34481  ballotlem1c  34482  ballotlemsgt1  34485  ballotlemsdom  34486  ballotlemsel1i  34487  ballotlemsf1o  34488  ballotlemsima  34490  ballotlemfrceq  34503  ballotlemfrcn0  34504  ballotlem1ri  34509  signsplypnf  34524  itgexpif  34580  fsum2dsub  34581  breprexplemc  34606  vtsprod  34613  circlemeth  34614  revpfxsfxrev  35099  swrdrevpfx  35100  revwlk  35108  swrdwlk  35110  divcnvlin  35716  fwddifnp1  36149  knoppndvlem2  36497  knoppndvlem7  36502  knoppndvlem14  36509  knoppndvlem16  36511  ltflcei  37598  poimirlem1  37611  poimirlem2  37612  poimirlem7  37617  poimirlem16  37626  poimirlem17  37627  poimirlem19  37629  poimirlem20  37630  poimirlem24  37634  poimirlem31  37641  poimirlem32  37642  fdc  37735  mettrifi  37747  caushft  37751  cntotbnd  37786  fzsplitnd  41965  lcmineqlem6  42017  lcmineqlem18  42029  aks4d1p1p1  42046  aks4d1p8d3  42069  aks4d1p8  42070  primrootscoprmpow  42082  posbezout  42083  primrootscoprbij  42085  primrootspoweq0  42089  hashscontpow1  42104  aks6d1c3  42106  aks6d1c4  42107  aks6d1c5lem1  42119  aks6d1c5lem2  42121  sticksstones10  42138  sticksstones12a  42140  sticksstones12  42141  aks6d1c6lem3  42155  unitscyglem2  42179  unitscyglem4  42181  sumcubes  42296  oexpreposd  42305  exp11d  42309  dvdsexpb  42318  mzpsubmpt  42726  lzenom  42753  diophun  42756  eqrabdioph  42760  irrapxlem2  42806  irrapxlem3  42807  pellexlem6  42817  pell1234qrreccl  42837  pellfund14  42881  rmxyneg  42903  rmxyadd  42904  rmxp1  42915  rmxm1  42917  rmym1  42918  rmxluc  42919  rmyluc  42920  rmyluc2  42921  rmxdbl  42922  rmydbl  42923  congadd  42949  congsub  42953  congabseq  42957  acongrep  42963  acongeq  42966  jm2.18  42971  jm2.19lem1  42972  jm2.19lem2  42973  jm2.19lem3  42974  jm2.22  42978  jm2.23  42979  jm2.20nn  42980  jm2.25  42982  jm2.26lem3  42984  jm2.27c  42990  nzss  44300  hashnzfz  44303  hashnzfz2  44304  hashnzfzclim  44305  uzmptshftfval  44329  sineq0ALT  44920  fzisoeu  45292  fperiodmul  45296  monoord2xrv  45472  fmul01lt1lem2  45576  sumnnodd  45621  dvdsn1add  45930  dvnmul  45934  dvnprodlem1  45937  stoweidlem11  46002  stoweidlem26  46017  dirkertrigeqlem1  46089  dirkertrigeqlem2  46090  dirkertrigeqlem3  46091  dirkertrigeq  46092  dirkeritg  46093  fourierdlem26  46124  fourierdlem48  46145  fourierdlem49  46146  fourierdlem79  46176  fourierdlem91  46188  fourierdlem103  46200  fourierdlem104  46201  fouriersw  46222  etransclem1  46226  etransclem4  46229  etransclem8  46233  etransclem9  46234  etransclem15  46240  etransclem17  46242  etransclem18  46243  etransclem20  46245  etransclem21  46246  etransclem22  46247  etransclem23  46248  etransclem24  46249  etransclem25  46250  etransclem35  46260  etransclem38  46263  etransclem41  46266  etransclem44  46269  etransclem45  46270  etransclem46  46271  etransclem47  46272  etransclem48  46273  2elfz2melfz  47312  ceilbi  47327  fldivmod  47332  submodaddmod  47335  zplusmodne  47337  m1modne  47342  minusmod5ne  47343  submodlt  47344  minusmodnep2tmod  47347  m1modmmod  47352  modmkpkne  47355  modmknepk  47356  mod2addne  47358  modm2nep1  47360  modm1nep2  47362  modm1nem2  47363  fsumsplitsndif  47367  iccpartgtprec  47414  fargshiftf1  47435  fargshiftfo  47436  mod42tp1mod8  47596  sfprmdvdsmersenne  47597  lighneallem3  47601  lighneallem4b  47603  modexp2m1d  47606  dfodd6  47631  onego  47640  m1expoddALTV  47642  zofldiv2ALTV  47656  oddflALTV  47657  oexpnegALTV  47671  omoeALTV  47679  omeoALTV  47680  epoo  47697  emoo  47698  epee  47699  emee  47700  evensumeven  47701  evenltle  47711  even3prm2  47713  mogoldbblem  47714  fppr2odd  47725  fpprwppr  47733  fpprwpprb  47734  sbgoldbst  47772  sbgoldbaltlem2  47774  sgoldbeven3prm  47777  nnsum3primesprm  47784  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  bgoldbtbndlem2  47800  bgoldbtbndlem4  47802  bgoldbtbnd  47803  gpgedgvtx1  48056  gpgvtxedg0  48057  gpgvtxedg1  48058  gpg5nbgrvtx13starlem2  48066  gpg3nbgrvtx0  48070  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  2zrngamnd  48241  2zrngacmnd  48242  2zrngagrp  48243  2zrngALT  48248  2zrngnmlid  48249  2zrngnmlid2  48251  ztprmneprm  48341  altgsumbcALT  48347  zofldiv2  48526  fllogbd  48555  nnpw2blen  48575  blen1b  48583  blennngt2o2  48587  blennn0e2  48589  dig2nn1st  48600  dignn0flhalflem1  48610