Theorem zcnd 12578

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 11004  ℤcz 12468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-resscn 11063

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-neg 11347  df-z 12469

This theorem is referenced by:  zsupss  12835  rpnnen1lem5  12879  fzm1  13507  fzrevral  13512  fzshftral  13515  nn0disj  13544  predfz  13553  fzoss2  13587  elfzo0suble  13606  fzo0addelr  13619  elfzoext  13622  fzosubel  13624  fzosubel3  13626  fzocatel  13629  fzosplitsnm1  13640  elfzom1elp1fzo1  13667  fzom1ne1  13685  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  14494  ccatass  14496  ccatalpha  14501  swrdfv0  14557  swrdfv2  14569  swrds1  14574  ccatswrd  14576  pfxfv  14590  ccatpfx  14608  swrdpfx  14614  pfxccatin12lem2  14638  spllen  14661  revccat  14673  revrev  14674  cshwidxmod  14710  cshwidxm1  14714  cshweqrep  14728  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  chnlt  18529  mulgsubcl  19001  mulgdirlem  19018  mulgdir  19019  mulgass  19024  mulgmodid  19026  mulgsubdir  19027  psgnunilem5  19406  psgnunilem2  19407  psgnunilem4  19409  m1expaddsub  19410  psgnuni  19411  odnncl  19457  odmulg  19468  odbezout  19470  sylow1lem1  19510  sylow2alem2  19530  efgsres  19650  efgredleme  19655  efgredlemc  19657  odadd1  19760  odadd2  19761  cyggeninv  19795  gsummptshft  19848  ablfacrp  19980  pgpfac1lem3  19991  fincygsubgodd  20026  srgbinomlem3  20146  srgbinomlem4  20147  zringmulg  21393  zringlpirlem1  21399  zringlpirlem3  21401  prmirredlem  21409  fermltlchr  21466  zndvds0  21487  znf1o  21488  znunit  21500  cayhamlem1  22781  tgpmulg  24008  zdis  24732  uniioombllem3  25513  mbfi1fseqlem4  25646  dvexp3  25909  aareccl  26261  aalioulem1  26267  geolim3  26274  aaliou3lem2  26278  aaliou3lem6  26283  ulmshft  26326  sineq0  26460  efif1olem2  26479  igamz  26985  wilthlem1  27005  wilthlem2  27006  basellem3  27020  mumul  27118  musum  27128  musumsum  27129  muinv  27130  ppiub  27142  chtub  27150  logfac2  27155  chpchtsum  27157  dchrptlem1  27202  pcbcctr  27214  bcmono  27215  bposlem5  27226  bposlem6  27227  lgslem1  27235  lgsval2lem  27245  lgsval4a  27257  lgsneg  27259  lgsneg1  27260  lgsmod  27261  lgsdirprm  27269  lgsdir  27270  lgsdilem2  27271  lgsdi  27272  lgsne0  27273  lgsabs1  27274  lgssq  27275  lgssq2  27276  lgsmulsqcoprm  27281  lgsdirnn0  27282  lgsdinn0  27283  lgsqrlem1  27284  gausslemma2dlem1a  27303  gausslemma2dlem1  27304  gausslemma2dlem4  27307  gausslemma2dlem5a  27308  gausslemma2dlem5  27309  gausslemma2dlem6  27310  gausslemma2d  27312  lgseisenlem1  27313  lgseisenlem2  27314  lgseisenlem3  27315  lgseisenlem4  27316  lgsquadlem1  27318  lgsquad2lem1  27322  lgsquad3  27325  2lgslem1b  27330  2lgsoddprmlem2  27347  2sqlem3  27358  2sqlem4  27359  2sqlem8a  27363  2sqlem8  27364  2sqlem11  27367  2sqblem  27369  2sqn0  27372  2sqmod  27374  dchrisumlem1  27427  dchrmusum2  27432  dchrvmasumlem1  27433  dchrvmasum2lem  27434  mudivsum  27468  mulogsum  27470  mulog2sumlem2  27473  selberglem1  27483  selberglem3  27485  selberg  27486  pntpbnd2  27525  pntlemf  27543  padicabvcxp  27570  axlowdimlem14  28933  axlowdimlem16  28935  pthdadjvtx  29706  crctcshwlkn0lem4  29791  crctcshwlkn0lem5  29792  crctcshlem4  29798  crctcsh  29802  clwwlkccatlem  29969  clwwisshclwws  29995  eucrctshift  30223  fzm1ne1  32771  fzspl  32772  bcm1n  32777  elq2  32794  znumd  32795  zdend  32796  numdenneg  32797  divnumden2  32798  ltesubnnd  32805  ccatf1  32930  swrdrn3  32936  swrdf1  32937  cshwrnid  32942  gsumzrsum  33039  cycpmco2lem3  33097  cycpmco2lem4  33098  cycpmco2lem5  33099  cycpmco2lem6  33100  cycpmco2  33102  archiabllem1  33162  archiabllem2c  33164  elrgspnlem1  33209  elrgspnlem2  33210  znfermltl  33331  zringidom  33516  zringfrac  33519  zconstr  33777  cos9thpiminplylem2  33796  zrhnm  33980  cnzh  33981  rezh  33982  zrhcntr  33992  qqhval2lem  33994  qqhghm  34001  qqhrhm  34002  qqhnm  34003  ballotlemfc0  34506  ballotlemfcc  34507  ballotlemic  34520  ballotlem1c  34521  ballotlemsgt1  34524  ballotlemsdom  34525  ballotlemsel1i  34526  ballotlemsf1o  34527  ballotlemsima  34529  ballotlemfrceq  34542  ballotlemfrcn0  34543  ballotlem1ri  34548  signsplypnf  34563  itgexpif  34619  fsum2dsub  34620  breprexplemc  34645  vtsprod  34652  circlemeth  34653  revpfxsfxrev  35160  swrdrevpfx  35161  revwlk  35169  swrdwlk  35171  divcnvlin  35777  fwddifnp1  36209  knoppndvlem2  36557  knoppndvlem7  36562  knoppndvlem14  36569  knoppndvlem16  36571  ltflcei  37658  poimirlem1  37671  poimirlem2  37672  poimirlem7  37677  poimirlem16  37686  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem24  37694  poimirlem31  37701  poimirlem32  37702  fdc  37795  mettrifi  37807  caushft  37811  cntotbnd  37846  fzsplitnd  42085  lcmineqlem6  42137  lcmineqlem18  42149  aks4d1p1p1  42166  aks4d1p8d3  42189  aks4d1p8  42190  primrootscoprmpow  42202  posbezout  42203  primrootscoprbij  42205  primrootspoweq0  42209  hashscontpow1  42224  aks6d1c3  42226  aks6d1c4  42227  aks6d1c5lem1  42239  aks6d1c5lem2  42241  sticksstones10  42258  sticksstones12a  42260  sticksstones12  42261  aks6d1c6lem3  42275  unitscyglem2  42299  unitscyglem4  42301  sumcubes  42416  oexpreposd  42425  exp11d  42429  dvdsexpb  42438  mzpsubmpt  42846  lzenom  42873  diophun  42876  eqrabdioph  42880  irrapxlem2  42926  irrapxlem3  42927  pellexlem6  42937  pell1234qrreccl  42957  pellfund14  43001  rmxyneg  43023  rmxyadd  43024  rmxp1  43035  rmxm1  43037  rmym1  43038  rmxluc  43039  rmyluc  43040  rmyluc2  43041  rmxdbl  43042  rmydbl  43043  congadd  43069  congsub  43073  congabseq  43077  acongrep  43083  acongeq  43086  jm2.18  43091  jm2.19lem1  43092  jm2.19lem2  43093  jm2.19lem3  43094  jm2.22  43098  jm2.23  43099  jm2.20nn  43100  jm2.25  43102  jm2.26lem3  43104  jm2.27c  43110  nzss  44420  hashnzfz  44423  hashnzfz2  44424  hashnzfzclim  44425  uzmptshftfval  44449  sineq0ALT  45039  fzisoeu  45411  fperiodmul  45415  monoord2xrv  45591  fmul01lt1lem2  45695  sumnnodd  45740  dvdsn1add  46047  dvnmul  46051  dvnprodlem1  46054  stoweidlem11  46119  stoweidlem26  46134  dirkertrigeqlem1  46206  dirkertrigeqlem2  46207  dirkertrigeqlem3  46208  dirkertrigeq  46209  dirkeritg  46210  fourierdlem26  46241  fourierdlem48  46262  fourierdlem49  46263  fourierdlem79  46293  fourierdlem91  46305  fourierdlem103  46317  fourierdlem104  46318  fouriersw  46339  etransclem1  46343  etransclem4  46346  etransclem8  46350  etransclem9  46351  etransclem15  46357  etransclem17  46359  etransclem18  46360  etransclem20  46362  etransclem21  46363  etransclem22  46364  etransclem23  46365  etransclem24  46366  etransclem25  46367  etransclem35  46377  etransclem38  46380  etransclem41  46383  etransclem44  46386  etransclem45  46387  etransclem46  46388  etransclem47  46389  etransclem48  46390  chnerlem2  46991  2elfz2melfz  47428  ceilbi  47443  fldivmod  47448  submodaddmod  47451  zplusmodne  47453  m1modne  47458  minusmod5ne  47459  submodlt  47460  minusmodnep2tmod  47463  m1modmmod  47468  modmkpkne  47471  modmknepk  47472  mod2addne  47474  modm2nep1  47476  modm1nep2  47478  modm1nem2  47479  fsumsplitsndif  47483  iccpartgtprec  47530  fargshiftf1  47551  fargshiftfo  47552  mod42tp1mod8  47712  sfprmdvdsmersenne  47713  lighneallem3  47717  lighneallem4b  47719  modexp2m1d  47722  dfodd6  47747  onego  47756  m1expoddALTV  47758  zofldiv2ALTV  47772  oddflALTV  47773  oexpnegALTV  47787  omoeALTV  47795  omeoALTV  47796  epoo  47813  emoo  47814  epee  47815  emee  47816  evensumeven  47817  evenltle  47827  even3prm2  47829  mogoldbblem  47830  fppr2odd  47841  fpprwppr  47849  fpprwpprb  47850  sbgoldbst  47888  sbgoldbaltlem2  47890  sgoldbeven3prm  47893  nnsum3primesprm  47900  nnsum4primesodd  47906  nnsum4primesoddALTV  47907  nnsum4primeseven  47910  nnsum4primesevenALTV  47911  bgoldbtbndlem2  47916  bgoldbtbndlem4  47918  bgoldbtbnd  47919  gpgedgvtx1  48172  gpgvtxedg0  48173  gpgvtxedg1  48174  gpg5nbgrvtx13starlem2  48182  gpg3nbgrvtx0  48186  pgnbgreunbgrlem2lem1  48224  pgnbgreunbgrlem2lem2  48225  pgnbgreunbgrlem2lem3  48226  2zrngamnd  48357  2zrngacmnd  48358  2zrngagrp  48359  2zrngALT  48364  2zrngnmlid  48365  2zrngnmlid2  48367  ztprmneprm  48457  altgsumbcALT  48463  zofldiv2  48642  fllogbd  48671  nnpw2blen  48691  blen1b  48699  blennngt2o2  48703  blennn0e2  48705  dig2nn1st  48716  dignn0flhalflem1  48726