Theorem zcnd 12629

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11031  ℤcz 12519

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6450  df-fv 6502  df-ov 7365  df-neg 11375  df-z 12520

This theorem is referenced by:  zsupss  12882  rpnnen1lem5  12926  fzm1  13556  fzrevral  13561  fzshftral  13564  nn0disj  13593  predfz  13602  fzoss2  13637  elfzo0suble  13656  fzo0addelr  13669  elfzoext  13672  fzosubel  13674  fzosubel3  13676  fzocatel  13679  fzosplitsnm1  13690  elfzom1elp1fzo1  13717  fzom1ne1  13735  2tnp1ge0ge0  13783  quoremz  13809  intfrac2  13812  intfracq  13813  flpmodeq  13828  moddiffl  13836  modmul1  13881  modmul12d  13882  modfzo0difsn  13900  modsumfzodifsn  13901  addmodlteq  13903  uzrdgxfr  13924  fzen2  13926  monoord2  13990  seqf1olem1  13998  seqf1olem2  13999  seqz  14007  expaddzlem  14062  znsqcld  14119  modexp  14195  sqoddm1div8  14200  bcm1k  14272  bcp1nk  14274  bcval5  14275  bcpasc  14278  hashfz  14384  hashfzo  14386  hashfzp1  14388  hashbclem  14409  seqcoll  14421  ccatval3  14536  ccatlid  14544  ccatass  14546  ccatalpha  14551  swrdfv0  14607  swrdfv2  14619  swrds1  14624  ccatswrd  14626  pfxfv  14640  ccatpfx  14658  swrdpfx  14664  pfxccatin12lem2  14688  spllen  14711  revccat  14723  revrev  14724  cshwidxmod  14760  cshwidxm1  14764  cshweqrep  14778  2cshwcshw  14782  cshimadifsn0  14787  swrds2m  14898  seqshft  15042  fzomaxdif  15301  climshft2  15539  iserex  15614  isercoll2  15626  serf0  15638  iseraltlem2  15640  iseraltlem3  15641  iseralt  15642  sumrblem  15668  fsumm1  15708  fsumsplitsnun  15712  fsump1  15713  fsumshftm  15738  fsumrev2  15739  telfsumo  15760  fsumparts  15764  binomlem  15789  isumshft  15799  isumsplit  15800  isum1p  15801  arisum  15820  pwdif  15828  cvgrat  15843  mertenslem1  15844  ntrivcvg  15857  ntrivcvgtail  15860  prodrblem  15889  fprodser  15909  fprodm1  15927  fprodp1  15929  fprodrev  15937  fprodmodd  15957  fallfacval3  15972  fallfacfwd  15996  0fallfac  15997  binomfallfaclem2  16000  fallfacval4  16003  fsumkthpow  16016  eirrlem  16166  sqrt2irrlem  16210  addmulmodb  16229  dvds2ln  16253  dvdsadd2b  16270  fsumdvds  16272  fzocongeq  16288  addmodlteqALT  16289  dvdsexp  16292  dvdsmod  16293  3dvds  16295  fprodfvdvdsd  16298  odd2np1  16305  oddm1even  16307  oexpneg  16309  mod2eq1n2dvds  16311  mulsucdiv2z  16317  zob  16323  ltoddhalfle  16325  sumodd  16352  pwp1fsum  16355  divalglem0  16357  divalglem4  16360  divalglem8  16364  divalgb  16368  divalgmod  16370  modremain  16372  flodddiv4  16379  bitsp1  16395  bitsfzo  16399  bitsmod  16400  bitsinv1lem  16405  bitsf1  16410  sadaddlem  16430  bitsres  16437  bitsuz  16438  bitsshft  16439  smumullem  16456  modgcd  16496  gcdmultipled  16498  dvdsgcdidd  16501  bezoutlem1  16503  bezoutlem2  16504  bezoutlem3  16505  bezoutlem4  16506  dvdsmulgcd  16520  rplpwr  16522  lcmid  16573  absprodnn  16582  mulgcddvds  16619  divgcdcoprm0  16629  cncongr1  16631  cncongr2  16632  dvdszzq  16686  rpexp  16687  prmdvdsbc  16691  qmuldeneqnum  16712  numdensq  16719  qden1elz  16722  numdenexp  16725  hashdvds  16740  phiprm  16742  eulerthlem2  16747  fermltl  16749  prmdiv  16750  prmdiveq  16751  hashgcdlem  16753  odzdvds  16761  vfermltlALT  16768  modprm0  16771  modprmn0modprm0  16773  pythagtriplem6  16787  pythagtriplem7  16788  pythagtriplem15  16795  pcpremul  16809  pceulem  16811  pczpre  16813  pcdiv  16818  pcqmul  16819  pcqdiv  16823  pcexp  16825  pcaddlem  16854  pcadd  16855  fldivp1  16863  pcfac  16865  pcbc  16866  prmpwdvds  16870  prmreclem4  16885  4sqlem5  16908  4sqlem8  16911  4sqlem9  16912  4sqlem10  16913  4sqlem11  16921  4sqlem14  16924  4sqlem16  16926  4sqlem17  16927  vdwapun  16940  vdwnnlem2  16962  prmop1  17004  prmdvdsprmo  17008  prmgaplem7  17023  prmlem0  17071  chnlt  18584  mulgsubcl  19059  mulgdirlem  19076  mulgdir  19077  mulgass  19082  mulgmodid  19084  mulgsubdir  19085  psgnunilem5  19464  psgnunilem2  19465  psgnunilem4  19467  m1expaddsub  19468  psgnuni  19469  odnncl  19515  odmulg  19526  odbezout  19528  sylow1lem1  19568  sylow2alem2  19588  efgsres  19708  efgredleme  19713  efgredlemc  19715  odadd1  19818  odadd2  19819  cyggeninv  19853  gsummptshft  19906  ablfacrp  20038  pgpfac1lem3  20049  fincygsubgodd  20084  srgbinomlem3  20204  srgbinomlem4  20205  zringmulg  21450  zringlpirlem1  21456  zringlpirlem3  21458  prmirredlem  21466  fermltlchr  21523  zndvds0  21544  znf1o  21545  znunit  21557  cayhamlem1  22845  tgpmulg  24072  zdis  24796  uniioombllem3  25566  mbfi1fseqlem4  25699  dvexp3  25959  aareccl  26307  aalioulem1  26313  geolim3  26320  aaliou3lem2  26324  aaliou3lem6  26329  ulmshft  26372  sineq0  26505  efif1olem2  26524  igamz  27029  wilthlem1  27049  wilthlem2  27050  basellem3  27064  mumul  27162  musum  27172  musumsum  27173  muinv  27174  ppiub  27185  chtub  27193  logfac2  27198  chpchtsum  27200  dchrptlem1  27245  pcbcctr  27257  bcmono  27258  bposlem5  27269  bposlem6  27270  lgslem1  27278  lgsval2lem  27288  lgsval4a  27300  lgsneg  27302  lgsneg1  27303  lgsmod  27304  lgsdirprm  27312  lgsdir  27313  lgsdilem2  27314  lgsdi  27315  lgsne0  27316  lgsabs1  27317  lgssq  27318  lgssq2  27319  lgsmulsqcoprm  27324  lgsdirnn0  27325  lgsdinn0  27326  lgsqrlem1  27327  gausslemma2dlem1a  27346  gausslemma2dlem1  27347  gausslemma2dlem4  27350  gausslemma2dlem5a  27351  gausslemma2dlem5  27352  gausslemma2dlem6  27353  gausslemma2d  27355  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem3  27358  lgseisenlem4  27359  lgsquadlem1  27361  lgsquad2lem1  27365  lgsquad3  27368  2lgslem1b  27373  2lgsoddprmlem2  27390  2sqlem3  27401  2sqlem4  27402  2sqlem8a  27406  2sqlem8  27407  2sqlem11  27410  2sqblem  27412  2sqn0  27415  2sqmod  27417  dchrisumlem1  27470  dchrmusum2  27475  dchrvmasumlem1  27476  dchrvmasum2lem  27477  mudivsum  27511  mulogsum  27513  mulog2sumlem2  27516  selberglem1  27526  selberglem3  27528  selberg  27529  pntpbnd2  27568  pntlemf  27586  padicabvcxp  27613  axlowdimlem14  29042  axlowdimlem16  29044  pthdadjvtx  29815  crctcshwlkn0lem4  29900  crctcshwlkn0lem5  29901  crctcshlem4  29907  crctcsh  29911  clwwlkccatlem  30078  clwwisshclwws  30104  eucrctshift  30332  fzm1ne1  32880  fzspl  32881  bcm1n  32887  elq2  32904  znumd  32905  zdend  32906  numdenneg  32907  divnumden2  32908  ltesubnnd  32915  ccatf1  33028  swrdrn3  33034  swrdf1  33035  cshwrnid  33040  gsumzrsum  33145  gsummulsubdishift1  33148  cycpmco2lem3  33208  cycpmco2lem4  33209  cycpmco2lem5  33210  cycpmco2lem6  33211  cycpmco2  33213  archiabllem1  33273  archiabllem2c  33275  elrgspnlem1  33322  elrgspnlem2  33323  znfermltl  33445  zringidom  33630  zringfrac  33633  esplyindfv  33739  zconstr  33928  cos9thpiminplylem2  33947  zrhnm  34131  cnzh  34132  rezh  34133  zrhcntr  34143  qqhval2lem  34145  qqhghm  34152  qqhrhm  34153  qqhnm  34154  ballotlemfc0  34657  ballotlemfcc  34658  ballotlemic  34671  ballotlem1c  34672  ballotlemsgt1  34675  ballotlemsdom  34676  ballotlemsel1i  34677  ballotlemsf1o  34678  ballotlemsima  34680  ballotlemfrceq  34693  ballotlemfrcn0  34694  ballotlem1ri  34699  signsplypnf  34714  itgexpif  34770  fsum2dsub  34771  breprexplemc  34796  vtsprod  34803  circlemeth  34804  revpfxsfxrev  35318  swrdrevpfx  35319  revwlk  35327  swrdwlk  35329  divcnvlin  35935  fwddifnp1  36367  knoppndvlem2  36793  knoppndvlem7  36798  knoppndvlem14  36805  knoppndvlem16  36807  ltflcei  37947  poimirlem1  37960  poimirlem2  37961  poimirlem7  37966  poimirlem16  37975  poimirlem17  37976  poimirlem19  37978  poimirlem20  37979  poimirlem24  37983  poimirlem31  37990  poimirlem32  37991  fdc  38084  mettrifi  38096  caushft  38100  cntotbnd  38135  fzsplitnd  42439  lcmineqlem6  42491  lcmineqlem18  42503  aks4d1p1p1  42520  aks4d1p8d3  42543  aks4d1p8  42544  primrootscoprmpow  42556  posbezout  42557  primrootscoprbij  42559  primrootspoweq0  42563  hashscontpow1  42578  aks6d1c3  42580  aks6d1c4  42581  aks6d1c5lem1  42593  aks6d1c5lem2  42595  sticksstones10  42612  sticksstones12a  42614  sticksstones12  42615  aks6d1c6lem3  42629  unitscyglem2  42653  unitscyglem4  42655  sumcubes  42763  oexpreposd  42772  exp11d  42776  dvdsexpb  42785  mzpsubmpt  43193  lzenom  43220  diophun  43223  eqrabdioph  43227  irrapxlem2  43273  irrapxlem3  43274  pellexlem6  43284  pell1234qrreccl  43304  pellfund14  43348  rmxyneg  43370  rmxyadd  43371  rmxp1  43382  rmxm1  43384  rmym1  43385  rmxluc  43386  rmyluc  43387  rmyluc2  43388  rmxdbl  43389  rmydbl  43390  congadd  43416  congsub  43420  congabseq  43424  acongrep  43430  acongeq  43433  jm2.18  43438  jm2.19lem1  43439  jm2.19lem2  43440  jm2.19lem3  43441  jm2.22  43445  jm2.23  43446  jm2.20nn  43447  jm2.25  43449  jm2.26lem3  43451  jm2.27c  43457  nzss  44766  hashnzfz  44769  hashnzfz2  44770  hashnzfzclim  44771  uzmptshftfval  44795  sineq0ALT  45385  fzisoeu  45755  fperiodmul  45759  monoord2xrv  45933  fmul01lt1lem2  46037  sumnnodd  46082  dvdsn1add  46389  dvnmul  46393  dvnprodlem1  46396  stoweidlem11  46461  stoweidlem26  46476  dirkertrigeqlem1  46548  dirkertrigeqlem2  46549  dirkertrigeqlem3  46550  dirkertrigeq  46551  dirkeritg  46552  fourierdlem26  46583  fourierdlem48  46604  fourierdlem49  46605  fourierdlem79  46635  fourierdlem91  46647  fourierdlem103  46659  fourierdlem104  46660  fouriersw  46681  etransclem1  46685  etransclem4  46688  etransclem8  46692  etransclem9  46693  etransclem15  46699  etransclem17  46701  etransclem18  46702  etransclem20  46704  etransclem21  46705  etransclem22  46706  etransclem23  46707  etransclem24  46708  etransclem25  46709  etransclem35  46719  etransclem38  46722  etransclem41  46725  etransclem44  46728  etransclem45  46729  etransclem46  46730  etransclem47  46731  etransclem48  46732  chnerlem2  47333  2elfz2melfz  47782  ceilbi  47801  flmrecm1  47807  fldivmod  47808  submodaddmod  47811  zplusmodne  47813  m1modne  47818  minusmod5ne  47819  submodlt  47820  minusmodnep2tmod  47823  m1modmmod  47828  modmkpkne  47831  modmknepk  47832  mod2addne  47834  modm2nep1  47836  modm1nep2  47838  modm1nem2  47839  2timesltsq  47842  fsumsplitsndif  47845  iccpartgtprec  47896  fargshiftf1  47917  fargshiftfo  47918  nprmmul3  48005  mod42tp1mod8  48081  sfprmdvdsmersenne  48082  lighneallem3  48086  lighneallem4b  48088  modexp2m1d  48091  nprmdvdsfacm1lem1  48099  ppivalnnprm  48104  dfodd6  48129  onego  48138  m1expoddALTV  48140  zofldiv2ALTV  48154  oddflALTV  48155  oexpnegALTV  48169  omoeALTV  48177  omeoALTV  48178  epoo  48195  emoo  48196  epee  48197  emee  48198  evensumeven  48199  evenltle  48209  even3prm2  48211  mogoldbblem  48212  fppr2odd  48223  fpprwppr  48231  fpprwpprb  48232  sbgoldbst  48270  sbgoldbaltlem2  48272  sgoldbeven3prm  48275  nnsum3primesprm  48282  nnsum4primesodd  48288  nnsum4primesoddALTV  48289  nnsum4primeseven  48292  nnsum4primesevenALTV  48293  bgoldbtbndlem2  48298  bgoldbtbndlem4  48300  bgoldbtbnd  48301  gpgedgvtx1  48554  gpgvtxedg0  48555  gpgvtxedg1  48556  gpg5nbgrvtx13starlem2  48564  gpg3nbgrvtx0  48568  pgnbgreunbgrlem2lem1  48606  pgnbgreunbgrlem2lem2  48607  pgnbgreunbgrlem2lem3  48608  2zrngamnd  48739  2zrngacmnd  48740  2zrngagrp  48741  2zrngALT  48746  2zrngnmlid  48747  2zrngnmlid2  48749  ztprmneprm  48839  altgsumbcALT  48845  zofldiv2  49023  fllogbd  49052  nnpw2blen  49072  blen1b  49080  blennngt2o2  49084  blennn0e2  49086  dig2nn1st  49097  dignn0flhalflem1  49107