Theorem zcnd 12595

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11022  ℤcz 12486

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 2115  ax-9 2123  ax-ext 2706  ax-resscn 11081

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 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-neg 11365  df-z 12487

This theorem is referenced by:  zsupss  12848  rpnnen1lem5  12892  fzm1  13521  fzrevral  13526  fzshftral  13529  nn0disj  13558  predfz  13567  fzoss2  13601  elfzo0suble  13620  fzo0addelr  13633  elfzoext  13636  fzosubel  13638  fzosubel3  13640  fzocatel  13643  fzosplitsnm1  13654  elfzom1elp1fzo1  13681  fzom1ne1  13699  2tnp1ge0ge0  13747  quoremz  13773  intfrac2  13776  intfracq  13777  flpmodeq  13792  moddiffl  13800  modmul1  13845  modmul12d  13846  modfzo0difsn  13864  modsumfzodifsn  13865  addmodlteq  13867  uzrdgxfr  13888  fzen2  13890  monoord2  13954  seqf1olem1  13962  seqf1olem2  13963  seqz  13971  expaddzlem  14026  znsqcld  14083  modexp  14159  sqoddm1div8  14164  bcm1k  14236  bcp1nk  14238  bcval5  14239  bcpasc  14242  hashfz  14348  hashfzo  14350  hashfzp1  14352  hashbclem  14373  seqcoll  14385  ccatval3  14500  ccatlid  14508  ccatass  14510  ccatalpha  14515  swrdfv0  14571  swrdfv2  14583  swrds1  14588  ccatswrd  14590  pfxfv  14604  ccatpfx  14622  swrdpfx  14628  pfxccatin12lem2  14652  spllen  14675  revccat  14687  revrev  14688  cshwidxmod  14724  cshwidxm1  14728  cshweqrep  14742  2cshwcshw  14746  cshimadifsn0  14751  swrds2m  14862  seqshft  15006  fzomaxdif  15265  climshft2  15503  iserex  15578  isercoll2  15590  serf0  15602  iseraltlem2  15604  iseraltlem3  15605  iseralt  15606  sumrblem  15632  fsumm1  15672  fsumsplitsnun  15676  fsump1  15677  fsumshftm  15702  fsumrev2  15703  telfsumo  15723  fsumparts  15727  binomlem  15750  isumshft  15760  isumsplit  15761  isum1p  15762  arisum  15781  pwdif  15789  cvgrat  15804  mertenslem1  15805  ntrivcvg  15818  ntrivcvgtail  15821  prodrblem  15850  fprodser  15870  fprodm1  15888  fprodp1  15890  fprodrev  15898  fprodmodd  15918  fallfacval3  15933  fallfacfwd  15957  0fallfac  15958  binomfallfaclem2  15961  fallfacval4  15964  fsumkthpow  15977  eirrlem  16127  sqrt2irrlem  16171  addmulmodb  16190  dvds2ln  16214  dvdsadd2b  16231  fsumdvds  16233  fzocongeq  16249  addmodlteqALT  16250  dvdsexp  16253  dvdsmod  16254  3dvds  16256  fprodfvdvdsd  16259  odd2np1  16266  oddm1even  16268  oexpneg  16270  mod2eq1n2dvds  16272  mulsucdiv2z  16278  zob  16284  ltoddhalfle  16286  sumodd  16313  pwp1fsum  16316  divalglem0  16318  divalglem4  16321  divalglem8  16325  divalgb  16329  divalgmod  16331  modremain  16333  flodddiv4  16340  bitsp1  16356  bitsfzo  16360  bitsmod  16361  bitsinv1lem  16366  bitsf1  16371  sadaddlem  16391  bitsres  16398  bitsuz  16399  bitsshft  16400  smumullem  16417  modgcd  16457  gcdmultipled  16459  dvdsgcdidd  16462  bezoutlem1  16464  bezoutlem2  16465  bezoutlem3  16466  bezoutlem4  16467  dvdsmulgcd  16481  rplpwr  16483  lcmid  16534  absprodnn  16543  mulgcddvds  16580  divgcdcoprm0  16590  cncongr1  16592  cncongr2  16593  dvdszzq  16646  rpexp  16647  prmdvdsbc  16651  qmuldeneqnum  16672  numdensq  16679  qden1elz  16682  numdenexp  16685  hashdvds  16700  phiprm  16702  eulerthlem2  16707  fermltl  16709  prmdiv  16710  prmdiveq  16711  hashgcdlem  16713  odzdvds  16721  vfermltlALT  16728  modprm0  16731  modprmn0modprm0  16733  pythagtriplem6  16747  pythagtriplem7  16748  pythagtriplem15  16755  pcpremul  16769  pceulem  16771  pczpre  16773  pcdiv  16778  pcqmul  16779  pcqdiv  16783  pcexp  16785  pcaddlem  16814  pcadd  16815  fldivp1  16823  pcfac  16825  pcbc  16826  prmpwdvds  16830  prmreclem4  16845  4sqlem5  16868  4sqlem8  16871  4sqlem9  16872  4sqlem10  16873  4sqlem11  16881  4sqlem14  16884  4sqlem16  16886  4sqlem17  16887  vdwapun  16900  vdwnnlem2  16922  prmop1  16964  prmdvdsprmo  16968  prmgaplem7  16983  prmlem0  17031  chnlt  18544  mulgsubcl  19016  mulgdirlem  19033  mulgdir  19034  mulgass  19039  mulgmodid  19041  mulgsubdir  19042  psgnunilem5  19421  psgnunilem2  19422  psgnunilem4  19424  m1expaddsub  19425  psgnuni  19426  odnncl  19472  odmulg  19483  odbezout  19485  sylow1lem1  19525  sylow2alem2  19545  efgsres  19665  efgredleme  19670  efgredlemc  19672  odadd1  19775  odadd2  19776  cyggeninv  19810  gsummptshft  19863  ablfacrp  19995  pgpfac1lem3  20006  fincygsubgodd  20041  srgbinomlem3  20161  srgbinomlem4  20162  zringmulg  21409  zringlpirlem1  21415  zringlpirlem3  21417  prmirredlem  21425  fermltlchr  21482  zndvds0  21503  znf1o  21504  znunit  21516  cayhamlem1  22808  tgpmulg  24035  zdis  24759  uniioombllem3  25540  mbfi1fseqlem4  25673  dvexp3  25936  aareccl  26288  aalioulem1  26294  geolim3  26301  aaliou3lem2  26305  aaliou3lem6  26310  ulmshft  26353  sineq0  26487  efif1olem2  26506  igamz  27012  wilthlem1  27032  wilthlem2  27033  basellem3  27047  mumul  27145  musum  27155  musumsum  27156  muinv  27157  ppiub  27169  chtub  27177  logfac2  27182  chpchtsum  27184  dchrptlem1  27229  pcbcctr  27241  bcmono  27242  bposlem5  27253  bposlem6  27254  lgslem1  27262  lgsval2lem  27272  lgsval4a  27284  lgsneg  27286  lgsneg1  27287  lgsmod  27288  lgsdirprm  27296  lgsdir  27297  lgsdilem2  27298  lgsdi  27299  lgsne0  27300  lgsabs1  27301  lgssq  27302  lgssq2  27303  lgsmulsqcoprm  27308  lgsdirnn0  27309  lgsdinn0  27310  lgsqrlem1  27311  gausslemma2dlem1a  27330  gausslemma2dlem1  27331  gausslemma2dlem4  27334  gausslemma2dlem5a  27335  gausslemma2dlem5  27336  gausslemma2dlem6  27337  gausslemma2d  27339  lgseisenlem1  27340  lgseisenlem2  27341  lgseisenlem3  27342  lgseisenlem4  27343  lgsquadlem1  27345  lgsquad2lem1  27349  lgsquad3  27352  2lgslem1b  27357  2lgsoddprmlem2  27374  2sqlem3  27385  2sqlem4  27386  2sqlem8a  27390  2sqlem8  27391  2sqlem11  27394  2sqblem  27396  2sqn0  27399  2sqmod  27401  dchrisumlem1  27454  dchrmusum2  27459  dchrvmasumlem1  27460  dchrvmasum2lem  27461  mudivsum  27495  mulogsum  27497  mulog2sumlem2  27500  selberglem1  27510  selberglem3  27512  selberg  27513  pntpbnd2  27552  pntlemf  27570  padicabvcxp  27597  axlowdimlem14  28977  axlowdimlem16  28979  pthdadjvtx  29750  crctcshwlkn0lem4  29835  crctcshwlkn0lem5  29836  crctcshlem4  29842  crctcsh  29846  clwwlkccatlem  30013  clwwisshclwws  30039  eucrctshift  30267  fzm1ne1  32817  fzspl  32818  bcm1n  32824  elq2  32841  znumd  32842  zdend  32843  numdenneg  32844  divnumden2  32845  ltesubnnd  32852  ccatf1  32980  swrdrn3  32986  swrdf1  32987  cshwrnid  32992  gsumzrsum  33097  gsummulsubdishift1  33100  cycpmco2lem3  33159  cycpmco2lem4  33160  cycpmco2lem5  33161  cycpmco2lem6  33162  cycpmco2  33164  archiabllem1  33224  archiabllem2c  33226  elrgspnlem1  33273  elrgspnlem2  33274  znfermltl  33396  zringidom  33581  zringfrac  33584  esplyindfv  33681  zconstr  33870  cos9thpiminplylem2  33889  zrhnm  34073  cnzh  34074  rezh  34075  zrhcntr  34085  qqhval2lem  34087  qqhghm  34094  qqhrhm  34095  qqhnm  34096  ballotlemfc0  34599  ballotlemfcc  34600  ballotlemic  34613  ballotlem1c  34614  ballotlemsgt1  34617  ballotlemsdom  34618  ballotlemsel1i  34619  ballotlemsf1o  34620  ballotlemsima  34622  ballotlemfrceq  34635  ballotlemfrcn0  34636  ballotlem1ri  34641  signsplypnf  34656  itgexpif  34712  fsum2dsub  34713  breprexplemc  34738  vtsprod  34745  circlemeth  34746  revpfxsfxrev  35259  swrdrevpfx  35260  revwlk  35268  swrdwlk  35270  divcnvlin  35876  fwddifnp1  36308  knoppndvlem2  36656  knoppndvlem7  36661  knoppndvlem14  36668  knoppndvlem16  36670  ltflcei  37748  poimirlem1  37761  poimirlem2  37762  poimirlem7  37767  poimirlem16  37776  poimirlem17  37777  poimirlem19  37779  poimirlem20  37780  poimirlem24  37784  poimirlem31  37791  poimirlem32  37792  fdc  37885  mettrifi  37897  caushft  37901  cntotbnd  37936  fzsplitnd  42175  lcmineqlem6  42227  lcmineqlem18  42239  aks4d1p1p1  42256  aks4d1p8d3  42279  aks4d1p8  42280  primrootscoprmpow  42292  posbezout  42293  primrootscoprbij  42295  primrootspoweq0  42299  hashscontpow1  42314  aks6d1c3  42316  aks6d1c4  42317  aks6d1c5lem1  42329  aks6d1c5lem2  42331  sticksstones10  42348  sticksstones12a  42350  sticksstones12  42351  aks6d1c6lem3  42365  unitscyglem2  42389  unitscyglem4  42391  sumcubes  42510  oexpreposd  42519  exp11d  42523  dvdsexpb  42532  mzpsubmpt  42927  lzenom  42954  diophun  42957  eqrabdioph  42961  irrapxlem2  43007  irrapxlem3  43008  pellexlem6  43018  pell1234qrreccl  43038  pellfund14  43082  rmxyneg  43104  rmxyadd  43105  rmxp1  43116  rmxm1  43118  rmym1  43119  rmxluc  43120  rmyluc  43121  rmyluc2  43122  rmxdbl  43123  rmydbl  43124  congadd  43150  congsub  43154  congabseq  43158  acongrep  43164  acongeq  43167  jm2.18  43172  jm2.19lem1  43173  jm2.19lem2  43174  jm2.19lem3  43175  jm2.22  43179  jm2.23  43180  jm2.20nn  43181  jm2.25  43183  jm2.26lem3  43185  jm2.27c  43191  nzss  44500  hashnzfz  44503  hashnzfz2  44504  hashnzfzclim  44505  uzmptshftfval  44529  sineq0ALT  45119  fzisoeu  45490  fperiodmul  45494  monoord2xrv  45669  fmul01lt1lem2  45773  sumnnodd  45818  dvdsn1add  46125  dvnmul  46129  dvnprodlem1  46132  stoweidlem11  46197  stoweidlem26  46212  dirkertrigeqlem1  46284  dirkertrigeqlem2  46285  dirkertrigeqlem3  46286  dirkertrigeq  46287  dirkeritg  46288  fourierdlem26  46319  fourierdlem48  46340  fourierdlem49  46341  fourierdlem79  46371  fourierdlem91  46383  fourierdlem103  46395  fourierdlem104  46396  fouriersw  46417  etransclem1  46421  etransclem4  46424  etransclem8  46428  etransclem9  46429  etransclem15  46435  etransclem17  46437  etransclem18  46438  etransclem20  46440  etransclem21  46441  etransclem22  46442  etransclem23  46443  etransclem24  46444  etransclem25  46445  etransclem35  46455  etransclem38  46458  etransclem41  46461  etransclem44  46464  etransclem45  46465  etransclem46  46466  etransclem47  46467  etransclem48  46468  chnerlem2  47069  2elfz2melfz  47506  ceilbi  47521  fldivmod  47526  submodaddmod  47529  zplusmodne  47531  m1modne  47536  minusmod5ne  47537  submodlt  47538  minusmodnep2tmod  47541  m1modmmod  47546  modmkpkne  47549  modmknepk  47550  mod2addne  47552  modm2nep1  47554  modm1nep2  47556  modm1nem2  47557  fsumsplitsndif  47561  iccpartgtprec  47608  fargshiftf1  47629  fargshiftfo  47630  mod42tp1mod8  47790  sfprmdvdsmersenne  47791  lighneallem3  47795  lighneallem4b  47797  modexp2m1d  47800  dfodd6  47825  onego  47834  m1expoddALTV  47836  zofldiv2ALTV  47850  oddflALTV  47851  oexpnegALTV  47865  omoeALTV  47873  omeoALTV  47874  epoo  47891  emoo  47892  epee  47893  emee  47894  evensumeven  47895  evenltle  47905  even3prm2  47907  mogoldbblem  47908  fppr2odd  47919  fpprwppr  47927  fpprwpprb  47928  sbgoldbst  47966  sbgoldbaltlem2  47968  sgoldbeven3prm  47971  nnsum3primesprm  47978  nnsum4primesodd  47984  nnsum4primesoddALTV  47985  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  bgoldbtbndlem2  47994  bgoldbtbndlem4  47996  bgoldbtbnd  47997  gpgedgvtx1  48250  gpgvtxedg0  48251  gpgvtxedg1  48252  gpg5nbgrvtx13starlem2  48260  gpg3nbgrvtx0  48264  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem2lem3  48304  2zrngamnd  48435  2zrngacmnd  48436  2zrngagrp  48437  2zrngALT  48442  2zrngnmlid  48443  2zrngnmlid2  48445  ztprmneprm  48535  altgsumbcALT  48541  zofldiv2  48719  fllogbd  48748  nnpw2blen  48768  blen1b  48776  blennngt2o2  48780  blennn0e2  48782  dig2nn1st  48793  dignn0flhalflem1  48803