Theorem zcnd 12804

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11198  ℤcz 12693

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-resscn 11257

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-neg 11544  df-z 12694

This theorem is used by:  zsupss  13064  rpnnen1lem5  13109  fzm1  13741  fzrevral  13746  fzshftral  13749  nn0disj  13778  predfz  13787  fzoss2  13822  elfzo0suble  13841  fzo0addelr  13854  elfzoext  13857  fzosubel  13859  fzosubel3  13861  fzocatel  13864  fzosplitsnm1  13875  elfzom1elp1fzo1  13902  fzom1ne1  13920  2tnp1ge0ge0  13969  quoremz  13995  intfrac2  13998  intfracq  13999  flpmodeq  14014  moddiffl  14022  modmul1  14067  modmul12d  14068  modfzo0difsn  14086  modsumfzodifsn  14087  addmodlteq  14089  uzrdgxfr  14110  fzen2  14112  monoord2  14176  seqf1olem1  14184  seqf1olem2  14185  seqz  14193  expaddzlem  14248  znsqcld  14305  modexp  14382  sqoddm1div8  14387  bcm1k  14459  bcp1nk  14461  bcval5  14462  bcpasc  14465  hashfz  14572  hashfzo  14574  hashfzp1  14576  hashbclem  14597  seqcoll  14609  ccatval3  14724  ccatlid  14732  ccatass  14734  ccatf1  14736  ccatalpha  14740  swrdfv0  14797  swrdf1  14799  swrdrn3  14802  swrdfv2  14811  swrds1  14816  ccatswrd  14818  pfxfv  14832  ccatpfx  14850  swrdpfx  14856  pfxccatin12lem2  14880  spllen  14903  revccat  14915  revrev  14916  revpfxsfxrev  14917  swrdrevpfx  14918  cshwidxmod  14954  cshwidxm1  14958  cshweqrep  14972  2cshwcshw  14976  cshimadifsn0  14981  swrds2m  15092  seqshft  15238  fzomaxdif  15511  climshft2  15749  iserex  15824  isercoll2  15836  serf0  15848  iseraltlem2  15850  iseraltlem3  15851  iseralt  15852  sumrblem  15877  fsumm1  15917  fsumsplitsnun  15921  fsump1  15922  fsumshftm  15947  fsumrev2  15948  telfsumo  15969  fsumparts  15973  binomlem  15998  isumshft  16008  isumsplit  16009  isum1p  16010  arisum  16029  pwdif  16037  cvgrat  16052  mertenslem1  16053  ntrivcvg  16066  ntrivcvgtail  16069  prodrblem  16096  fprodser  16116  fprodm1  16134  fprodp1  16136  fprodrev  16144  fprodmodd  16164  fallfacval3  16179  fallfacfwd  16202  0fallfac  16203  binomfallfaclem2  16206  fallfacval4  16209  fsumkthpow  16222  eirrlem  16372  sqrt2irrlem  16416  addmulmodb  16435  dvds2ln  16459  dvdsadd2b  16476  fsumdvds  16478  fzocongeq  16494  addmodlteqALT  16495  dvdsexp  16498  dvdsmod  16499  3dvds  16501  fprodfvdvdsd  16504  odd2np1  16511  oddm1even  16513  oexpneg  16515  mod2eq1n2dvds  16517  mulsucdiv2z  16523  zob  16529  ltoddhalfle  16531  sumodd  16558  pwp1fsum  16561  divalglem0  16563  divalglem4  16566  divalglem8  16570  divalgb  16574  divalgmod  16576  modremain  16578  flodddiv4  16585  bitsp1  16601  bitsfzo  16605  bitsmod  16606  bitsinv1lem  16611  bitsf1  16616  sadaddlem  16636  bitsres  16643  bitsuz  16644  bitsshft  16645  smumullem  16662  modgcd  16705  gcdmultipled  16707  dvdsgcdidd  16710  bezoutlem1  16712  bezoutlem2  16713  bezoutlem3  16714  bezoutlem4  16715  dvdsmulgcd  16730  rplpwr  16732  lcmid  16784  absprodnn  16793  mulgcddvds  16830  divgcdcoprm0  16840  cncongr1  16842  cncongr2  16843  dvdszzq  16897  rpexp  16898  prmdvdsbc  16902  qmuldeneqnum  16923  numdensq  16930  qden1elz  16933  numdenexp  16937  hashdvds  16952  phiprm  16954  eulerthlem2  16959  fermltl  16961  prmdiv  16962  prmdiveq  16963  hashgcdlem  16965  odzdvds  16973  vfermltlALT  16980  modprm0  16983  modprmn0modprm0  16985  pythagtriplem6  16999  pythagtriplem7  17000  pythagtriplem15  17007  pcpremul  17021  pceulem  17023  pczpre  17025  pcdiv  17030  pcqmul  17031  pcqdiv  17035  pcexp  17037  pcaddlem  17066  pcadd  17067  fldivp1  17075  pcfac  17077  pcbc  17078  prmpwdvds  17082  prmreclem4  17097  4sqlem5  17120  4sqlem8  17123  4sqlem9  17124  4sqlem10  17125  4sqlem11  17133  4sqlem14  17136  4sqlem16  17138  4sqlem17  17139  vdwapun  17152  vdwnnlem2  17174  prmop1  17216  prmdvdsprmo  17220  prmgaplem7  17235  prmlem0  17283  chnlt  18797  mulgsubcl  19298  mulgdirlem  19315  mulgdir  19316  mulgass  19321  mulgmodid  19323  mulgsubdir  19324  psgnunilem5  19708  psgnunilem2  19709  psgnunilem4  19711  m1expaddsub  19712  psgnuni  19713  odnncl  19759  odmulg  19770  odbezout  19772  sylow1lem1  19812  sylow2alem2  19832  efgsres  19952  efgredleme  19957  efgredlemc  19959  odadd1  20062  odadd2  20063  cyggeninv  20097  gsummptshft  20150  ablfacrp  20282  pgpfac1lem3  20293  fincygsubgodd  20328  srgbinomlem3  20454  srgbinomlem4  20455  zringmulg  21762  zringlpirlem1  21768  zringlpirlem3  21770  prmirredlem  21778  fermltlchr  21835  zndvds0  21856  znf1o  21857  znunit  21869  cayhamlem1  23184  tgpmulg  24412  zdis  25136  uniioombllem3  25906  mbfi1fseqlem4  26039  dvexp3  26298  aareccl  26653  aalioulem1  26659  geolim3  26666  aaliou3lem2  26670  aaliou3lem6  26675  ulmshft  26717  sineq0  26852  efif1olem2  26871  igamz  27375  wilthlem1  27395  wilthlem2  27396  basellem3  27410  mumul  27508  musum  27518  musumsum  27519  muinv  27520  ppiub  27531  chtub  27539  logfac2  27544  chpchtsum  27546  dchrptlem1  27591  pcbcctr  27603  bcmono  27604  bposlem5  27615  bposlem6  27616  lgslem1  27624  lgsval2lem  27634  lgsval4a  27646  lgsneg  27648  lgsneg1  27649  lgsmod  27650  lgsdirprm  27658  lgsdir  27659  lgsdilem2  27660  lgsdi  27661  lgsne0  27662  lgsabs1  27663  lgssq  27664  lgssq2  27665  lgsmulsqcoprm  27670  lgsdirnn0  27671  lgsdinn0  27672  lgsqrlem1  27673  gausslemma2dlem1a  27692  gausslemma2dlem1  27693  gausslemma2dlem4  27696  gausslemma2dlem5a  27697  gausslemma2dlem5  27698  gausslemma2dlem6  27699  gausslemma2d  27701  lgseisenlem1  27702  lgseisenlem2  27703  lgseisenlem3  27704  lgseisenlem4  27705  lgsquadlem1  27707  lgsquad2lem1  27711  lgsquad3  27714  2lgslem1b  27719  2lgsoddprmlem2  27736  2sqlem3  27747  2sqlem4  27748  2sqlem8a  27752  2sqlem8  27753  2sqlem11  27756  2sqblem  27758  2sqn0  27761  2sqmod  27763  dchrisumlem1  27816  dchrmusum2  27821  dchrvmasumlem1  27822  dchrvmasum2lem  27823  mudivsum  27857  mulogsum  27859  mulog2sumlem2  27862  selberglem1  27872  selberglem3  27874  selberg  27875  pntpbnd2  27914  pntlemf  27932  padicabvcxp  27959  axlowdimlem14  29533  axlowdimlem16  29535  revwlk  30267  swrdwlk  30268  pthdadjvtx  30313  crctcshwlkn0lem4  30402  crctcshwlkn0lem5  30403  crctcshlem4  30409  crctcsh  30413  clwwlkccatlem  30580  clwwisshclwws  30606  eucrctshift  30844  fzm1ne1  33380  fzspl  33381  bcm1n  33387  elq2  33403  znumd  33404  zdend  33405  numdenneg  33406  divnumden2  33407  ltesubnnd  33414  cshwrnid  33522  gsumzrsum  33626  gsummulsubdishift1  33629  cycpmco2lem3  33689  cycpmco2lem4  33690  cycpmco2lem5  33691  cycpmco2lem6  33692  cycpmco2  33694  archiabllem1  33754  archiabllem2c  33756  elrgspnlem1  33803  elrgspnlem2  33804  znfermltl  33922  zringidom  34083  zringfrac  34086  esplyindfv  34208  zconstr  34396  cos9thpiminplylem2  34415  zrhnm  34599  cnzh  34600  rezh  34601  zrhcntr  34611  qqhval2lem  34613  qqhghm  34620  qqhrhm  34621  qqhnm  34622  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemic  35139  ballotlem1c  35140  ballotlemsgt1  35143  ballotlemsdom  35144  ballotlemsel1i  35145  ballotlemsf1o  35146  ballotlemsima  35148  ballotlemfrceq  35161  ballotlemfrcn0  35162  ballotlem1ri  35167  signsplypnf  35179  itgexpif  35235  fsum2dsub  35236  breprexplemc  35261  vtsprod  35268  circlemeth  35269  divcnvlin  36498  fwddifnp1  36930  knoppndvlem2  37379  knoppndvlem7  37384  knoppndvlem14  37391  knoppndvlem16  37393  ltflcei  38531  poimirlem1  38539  poimirlem2  38540  poimirlem7  38545  poimirlem16  38554  poimirlem17  38555  poimirlem19  38557  poimirlem20  38558  poimirlem24  38562  poimirlem31  38569  poimirlem32  38570  fdc  38679  mettrifi  38691  caushft  38695  cntotbnd  38730  fzsplitnd  43032  lcmineqlem6  43084  lcmineqlem18  43096  aks4d1p1p1  43113  aks4d1p8d3  43136  aks4d1p8  43137  primrootscoprmpow  43149  posbezout  43150  primrootscoprbij  43152  primrootspoweq0  43156  hashscontpow1  43171  aks6d1c3  43173  aks6d1c4  43174  aks6d1c5lem1  43186  aks6d1c5lem2  43188  sticksstones10  43205  sticksstones12a  43207  sticksstones12  43208  aks6d1c6lem3  43222  unitscyglem2  43246  unitscyglem4  43248  sumcubes  43370  oexpreposd  43379  exp11d  43383  dvdsexpb  43387  mzpsubmpt  43753  lzenom  43780  diophun  43783  eqrabdioph  43787  irrapxlem2  43829  irrapxlem3  43830  pellexlem6  43840  pell1234qrreccl  43860  pellfund14  43904  rmxyneg  43926  rmxyadd  43927  rmxp1  43938  rmxm1  43940  rmym1  43941  rmxluc  43942  rmyluc  43943  rmyluc2  43944  rmxdbl  43945  rmydbl  43946  congadd  43972  congsub  43976  congabseq  43980  acongrep  43986  acongeq  43989  jm2.18  43994  jm2.19lem1  43995  jm2.19lem2  43996  jm2.19lem3  43997  jm2.22  44001  jm2.23  44002  jm2.20nn  44003  jm2.25  44005  jm2.26lem3  44007  jm2.27c  44013  nzss  45300  hashnzfz  45303  hashnzfz2  45304  hashnzfzclim  45305  uzmptshftfval  45329  sineq0ALT  45918  fzisoeu  46315  fperiodmul  46319  monoord2xrv  46492  fmul01lt1lem2  46596  sumnnodd  46641  dvdsn1add  46948  dvnmul  46952  dvnprodlem1  46955  stoweidlem11  47020  stoweidlem26  47035  dirkertrigeqlem1  47107  dirkertrigeqlem2  47108  dirkertrigeqlem3  47109  dirkertrigeq  47110  dirkeritg  47111  fourierdlem26  47142  fourierdlem48  47163  fourierdlem49  47164  fourierdlem79  47194  fourierdlem91  47206  fourierdlem103  47218  fourierdlem104  47219  fouriersw  47240  etransclem1  47244  etransclem4  47247  etransclem8  47251  etransclem9  47252  etransclem15  47258  etransclem17  47260  etransclem18  47261  etransclem20  47263  etransclem21  47264  etransclem22  47265  etransclem23  47266  etransclem24  47267  etransclem25  47268  etransclem35  47278  etransclem38  47281  etransclem41  47284  etransclem44  47287  etransclem45  47288  etransclem46  47289  etransclem47  47290  etransclem48  47291  chnerlem2  47892  2elfz2melfz  48387  ceilbi  48406  flmrecm1  48412  fldivmod  48413  submodaddmod  48416  zplusmodne  48418  m1modne  48423  minusmod5ne  48424  submodlt  48425  minusmodnep2tmod  48428  m1modmmod  48433  modmkpkne  48436  modmknepk  48437  mod2addne  48439  modm2nep1  48441  modm1nep2  48443  modm1nem2  48444  2timesltsq  48447  fsumsplitsndif  48450  iccpartgtprec  48501  fargshiftf1  48522  fargshiftfo  48523  nprmmul3  48610  mod42tp1mod8  48686  sfprmdvdsmersenne  48687  lighneallem3  48691  lighneallem4b  48693  modexp2m1d  48696  nprmdvdsfacm1lem1  48704  ppivalnnprm  48709  dfodd6  48734  onego  48743  m1expoddALTV  48745  zofldiv2ALTV  48759  oddflALTV  48760  oexpnegALTV  48774  omoeALTV  48782  omeoALTV  48783  epoo  48800  emoo  48801  epee  48802  emee  48803  evensumeven  48804  evenltle  48814  even3prm2  48816  mogoldbblem  48817  fppr2odd  48828  fpprwppr  48836  fpprwpprb  48837  sbgoldbst  48875  sbgoldbaltlem2  48877  sgoldbeven3prm  48880  nnsum3primesprm  48887  nnsum4primesodd  48893  nnsum4primesoddALTV  48894  nnsum4primeseven  48897  nnsum4primesevenALTV  48898  bgoldbtbndlem2  48903  bgoldbtbndlem4  48905  bgoldbtbnd  48906  gpgedgvtx1  49159  gpgvtxedg0  49160  gpgvtxedg1  49161  gpg5nbgrvtx13starlem2  49169  gpg3nbgrvtx0  49173  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  pgnbgreunbgrlem2lem3  49213  2zrngamnd  49343  2zrngacmnd  49344  2zrngagrp  49345  2zrngALT  49350  2zrngnmlid  49351  2zrngnmlid2  49353  ztprmneprm  49458  altgsumbcALT  49464  zofldiv2  49642  fllogbd  49671  nnpw2blen  49691  blen1b  49699  blennngt2o2  49703  blennn0e2  49705  dig2nn1st  49716  dignn0flhalflem1  49726