Theorem zcnd 12698

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

Syntax hints:   → wi 4   ∈ wcel 2099  ℂcc 11137  ℤcz 12589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-resscn 11196

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-neg 11478  df-z 12590

This theorem is referenced by:  zsupss  12952  rpnnen1lem5  12996  fzm1  13614  fzrevral  13619  fzshftral  13622  nn0disj  13650  predfz  13659  fzoss2  13693  fzo0addelr  13720  fzosubel  13724  fzosubel3  13726  fzocatel  13729  fzosplitsnm1  13740  elfzom1elp1fzo1  13765  2tnp1ge0ge0  13827  quoremz  13853  intfrac2  13856  intfracq  13857  flpmodeq  13872  moddiffl  13880  modmul1  13922  modmul12d  13923  modfzo0difsn  13941  modsumfzodifsn  13942  addmodlteq  13944  uzrdgxfr  13965  fzen2  13967  monoord2  14031  seqf1olem1  14039  seqf1olem2  14040  seqz  14048  expaddzlem  14103  znsqcld  14159  modexp  14233  sqoddm1div8  14238  bcm1k  14307  bcp1nk  14309  bcval5  14310  bcpasc  14313  hashfz  14419  hashfzo  14421  hashfzp1  14423  hashbclem  14444  seqcoll  14458  ccatval3  14562  ccatlid  14569  ccatass  14571  ccatalpha  14576  swrdfv0  14632  swrdfv2  14644  swrds1  14649  ccatswrd  14651  pfxfv  14665  ccatpfx  14684  swrdpfx  14690  pfxccatin12lem2  14714  spllen  14737  revccat  14749  revrev  14750  cshwidxmod  14786  cshwidxm1  14790  cshweqrep  14804  2cshwcshw  14809  cshimadifsn0  14814  swrds2m  14925  seqshft  15065  fzomaxdif  15323  climshft2  15559  iserex  15636  isercoll2  15648  serf0  15660  iseraltlem2  15662  iseraltlem3  15663  iseralt  15664  sumrblem  15690  fsumm1  15730  fsumsplitsnun  15734  fsump1  15735  fsumshftm  15760  fsumrev2  15761  telfsumo  15781  fsumparts  15785  binomlem  15808  isumshft  15818  isumsplit  15819  isum1p  15820  arisum  15839  pwdif  15847  cvgrat  15862  mertenslem1  15863  ntrivcvg  15876  ntrivcvgtail  15879  prodrblem  15906  fprodser  15926  fprodm1  15944  fprodp1  15946  fprodrev  15954  fprodmodd  15974  fallfacval3  15989  fallfacfwd  16013  0fallfac  16014  binomfallfaclem2  16017  fallfacval4  16020  fsumkthpow  16033  eirrlem  16181  sqrt2irrlem  16225  dvds2ln  16266  dvdsadd2b  16283  fsumdvds  16285  fzocongeq  16301  addmodlteqALT  16302  dvdsexp  16305  dvdsmod  16306  3dvds  16308  fprodfvdvdsd  16311  odd2np1  16318  oddm1even  16320  oexpneg  16322  mod2eq1n2dvds  16324  mulsucdiv2z  16330  zob  16336  ltoddhalfle  16338  sumodd  16365  pwp1fsum  16368  divalglem0  16370  divalglem4  16373  divalglem8  16377  divalgb  16381  divalgmod  16383  modremain  16385  flodddiv4  16390  bitsp1  16406  bitsfzo  16410  bitsmod  16411  bitsinv1lem  16416  bitsf1  16421  sadaddlem  16441  bitsres  16448  bitsuz  16449  bitsshft  16450  smumullem  16467  modgcd  16508  gcdmultipled  16510  dvdsgcdidd  16513  bezoutlem1  16515  bezoutlem2  16516  bezoutlem3  16517  bezoutlem4  16518  dvdsmulgcd  16531  rplpwr  16533  lcmid  16580  absprodnn  16589  mulgcddvds  16626  divgcdcoprm0  16636  cncongr1  16638  cncongr2  16639  dvdszzq  16693  rpexp  16694  prmdvdsbc  16698  qmuldeneqnum  16719  numdensq  16726  qden1elz  16729  hashdvds  16744  phiprm  16746  eulerthlem2  16751  fermltl  16753  prmdiv  16754  prmdiveq  16755  hashgcdlem  16757  odzdvds  16764  vfermltlALT  16771  modprm0  16774  modprmn0modprm0  16776  pythagtriplem6  16790  pythagtriplem7  16791  pythagtriplem15  16798  pcpremul  16812  pceulem  16814  pczpre  16816  pcdiv  16821  pcqmul  16822  pcqdiv  16826  pcexp  16828  pcaddlem  16857  pcadd  16858  fldivp1  16866  pcfac  16868  pcbc  16869  prmpwdvds  16873  prmreclem4  16888  4sqlem5  16911  4sqlem8  16914  4sqlem9  16915  4sqlem10  16916  4sqlem11  16924  4sqlem14  16927  4sqlem16  16929  4sqlem17  16930  vdwapun  16943  vdwnnlem2  16965  prmop1  17007  prmdvdsprmo  17011  prmgaplem7  17026  prmlem0  17075  mulgsubcl  19043  mulgdirlem  19060  mulgdir  19061  mulgass  19066  mulgmodid  19068  mulgsubdir  19069  psgnunilem5  19449  psgnunilem2  19450  psgnunilem4  19452  m1expaddsub  19453  psgnuni  19454  odnncl  19500  odmulg  19511  odbezout  19513  sylow1lem1  19553  sylow2alem2  19573  efgsres  19693  efgredleme  19698  efgredlemc  19700  odadd1  19803  odadd2  19804  cyggeninv  19838  gsummptshft  19891  ablfacrp  20023  pgpfac1lem3  20034  fincygsubgodd  20069  srgbinomlem3  20168  srgbinomlem4  20169  zringmulg  21382  zringlpirlem1  21388  zringlpirlem3  21390  prmirredlem  21398  fermltlchr  21459  zndvds0  21484  znf1o  21485  znunit  21497  cayhamlem1  22781  tgpmulg  24010  zdis  24745  uniioombllem3  25527  mbfi1fseqlem4  25661  dvexp3  25923  aareccl  26274  aalioulem1  26280  geolim3  26287  aaliou3lem2  26291  aaliou3lem6  26296  ulmshft  26339  sineq0  26471  efif1olem2  26490  igamz  26993  wilthlem1  27013  wilthlem2  27014  basellem3  27028  mumul  27126  musum  27136  musumsum  27137  muinv  27138  ppiub  27150  chtub  27158  logfac2  27163  chpchtsum  27165  dchrptlem1  27210  pcbcctr  27222  bcmono  27223  bposlem5  27234  bposlem6  27235  lgslem1  27243  lgsval2lem  27253  lgsval4a  27265  lgsneg  27267  lgsneg1  27268  lgsmod  27269  lgsdirprm  27277  lgsdir  27278  lgsdilem2  27279  lgsdi  27280  lgsne0  27281  lgsabs1  27282  lgssq  27283  lgssq2  27284  lgsmulsqcoprm  27289  lgsdirnn0  27290  lgsdinn0  27291  lgsqrlem1  27292  gausslemma2dlem1a  27311  gausslemma2dlem1  27312  gausslemma2dlem4  27315  gausslemma2dlem5a  27316  gausslemma2dlem5  27317  gausslemma2dlem6  27318  gausslemma2d  27320  lgseisenlem1  27321  lgseisenlem2  27322  lgseisenlem3  27323  lgseisenlem4  27324  lgsquadlem1  27326  lgsquad2lem1  27330  lgsquad3  27333  2lgslem1b  27338  2lgsoddprmlem2  27355  2sqlem3  27366  2sqlem4  27367  2sqlem8a  27371  2sqlem8  27372  2sqlem11  27375  2sqblem  27377  2sqn0  27380  2sqmod  27382  dchrisumlem1  27435  dchrmusum2  27440  dchrvmasumlem1  27441  dchrvmasum2lem  27442  mudivsum  27476  mulogsum  27478  mulog2sumlem2  27481  selberglem1  27491  selberglem3  27493  selberg  27494  pntpbnd2  27533  pntlemf  27551  padicabvcxp  27578  axlowdimlem14  28779  axlowdimlem16  28781  pthdadjvtx  29557  crctcshwlkn0lem4  29637  crctcshwlkn0lem5  29638  crctcshlem4  29644  crctcsh  29648  clwwlkccatlem  29812  clwwisshclwws  29838  eucrctshift  30066  fzm1ne1  32570  fzspl  32571  bcm1n  32576  fzom1ne1  32582  znumd  32591  zdend  32592  numdenneg  32593  divnumden2  32594  ltesubnnd  32598  ccatf1  32685  swrdrn3  32689  swrdf1  32690  cshwrnid  32695  cycpmco2lem3  32862  cycpmco2lem4  32863  cycpmco2lem5  32864  cycpmco2lem6  32865  cycpmco2  32867  archiabllem1  32914  archiabllem2c  32916  zringidom  32973  zringfrac  33009  znfermltl  33091  zrhnm  33570  cnzh  33571  rezh  33572  qqhval2lem  33582  qqhghm  33589  qqhrhm  33590  qqhnm  33591  ballotlemfc0  34112  ballotlemfcc  34113  ballotlemic  34126  ballotlem1c  34127  ballotlemsgt1  34130  ballotlemsdom  34131  ballotlemsel1i  34132  ballotlemsf1o  34133  ballotlemsima  34135  ballotlemfrceq  34148  ballotlemfrcn0  34149  ballotlem1ri  34154  signsplypnf  34182  itgexpif  34238  fsum2dsub  34239  breprexplemc  34264  vtsprod  34271  circlemeth  34272  revpfxsfxrev  34725  swrdrevpfx  34726  revwlk  34734  swrdwlk  34736  divcnvlin  35327  fwddifnp1  35761  knoppndvlem2  35988  knoppndvlem7  35993  knoppndvlem14  36000  knoppndvlem16  36002  ltflcei  37081  poimirlem1  37094  poimirlem2  37095  poimirlem7  37100  poimirlem16  37109  poimirlem17  37110  poimirlem19  37112  poimirlem20  37113  poimirlem24  37117  poimirlem31  37124  poimirlem32  37125  fdc  37218  mettrifi  37230  caushft  37234  cntotbnd  37269  fzsplitnd  41453  lcmineqlem6  41505  lcmineqlem18  41517  aks4d1p1p1  41534  aks4d1p8d3  41557  aks4d1p8  41558  primrootscoprmpow  41570  posbezout  41571  primrootscoprbij  41573  primrootspoweq0  41577  hashscontpow1  41592  aks6d1c3  41594  aks6d1c4  41595  aks6d1c5lem1  41607  aks6d1c5lem2  41609  sticksstones10  41627  sticksstones12a  41629  sticksstones12  41630  aks6d1c6lem3  41644  metakunt12  41668  metakunt15  41671  metakunt16  41672  metakunt28  41684  sumcubes  41873  oexpreposd  41881  exp11d  41885  numdenexp  41897  dvdsexpb  41902  mzpsubmpt  42163  lzenom  42190  diophun  42193  eqrabdioph  42197  irrapxlem2  42243  irrapxlem3  42244  pellexlem6  42254  pell1234qrreccl  42274  pellfund14  42318  rmxyneg  42341  rmxyadd  42342  rmxp1  42353  rmxm1  42355  rmym1  42356  rmxluc  42357  rmyluc  42358  rmyluc2  42359  rmxdbl  42360  rmydbl  42361  congadd  42387  congsub  42391  congabseq  42395  acongrep  42401  acongeq  42404  jm2.18  42409  jm2.19lem1  42410  jm2.19lem2  42411  jm2.19lem3  42412  jm2.22  42416  jm2.23  42417  jm2.20nn  42418  jm2.25  42420  jm2.26lem3  42422  jm2.27c  42428  nzss  43754  hashnzfz  43757  hashnzfz2  43758  hashnzfzclim  43759  uzmptshftfval  43783  sineq0ALT  44376  fzisoeu  44682  fperiodmul  44686  monoord2xrv  44866  fmul01lt1lem2  44973  sumnnodd  45018  dvdsn1add  45327  dvnmul  45331  dvnprodlem1  45334  stoweidlem11  45399  stoweidlem26  45414  dirkertrigeqlem1  45486  dirkertrigeqlem2  45487  dirkertrigeqlem3  45488  dirkertrigeq  45489  dirkeritg  45490  fourierdlem26  45521  fourierdlem48  45542  fourierdlem49  45543  fourierdlem79  45573  fourierdlem91  45585  fourierdlem103  45597  fourierdlem104  45598  fouriersw  45619  etransclem1  45623  etransclem4  45626  etransclem8  45630  etransclem9  45631  etransclem15  45637  etransclem17  45639  etransclem18  45640  etransclem20  45642  etransclem21  45643  etransclem22  45644  etransclem23  45645  etransclem24  45646  etransclem25  45647  etransclem35  45657  etransclem38  45660  etransclem41  45663  etransclem44  45666  etransclem45  45667  etransclem46  45668  etransclem47  45669  etransclem48  45670  2elfz2melfz  46698  fsumsplitsndif  46713  iccpartgtprec  46760  fargshiftf1  46781  fargshiftfo  46782  mod42tp1mod8  46942  sfprmdvdsmersenne  46943  lighneallem3  46947  lighneallem4b  46949  modexp2m1d  46952  dfodd6  46977  onego  46986  m1expoddALTV  46988  zofldiv2ALTV  47002  oddflALTV  47003  oexpnegALTV  47017  omoeALTV  47025  omeoALTV  47026  epoo  47043  emoo  47044  epee  47045  emee  47046  evensumeven  47047  evenltle  47057  even3prm2  47059  mogoldbblem  47060  fppr2odd  47071  fpprwppr  47079  fpprwpprb  47080  sbgoldbst  47118  sbgoldbaltlem2  47120  sgoldbeven3prm  47123  nnsum3primesprm  47130  nnsum4primesodd  47136  nnsum4primesoddALTV  47137  nnsum4primeseven  47140  nnsum4primesevenALTV  47141  bgoldbtbndlem2  47146  bgoldbtbndlem4  47148  bgoldbtbnd  47149  2zrngamnd  47309  2zrngacmnd  47310  2zrngagrp  47311  2zrngALT  47316  2zrngnmlid  47317  2zrngnmlid2  47319  ztprmneprm  47411  altgsumbcALT  47417  fldivmod  47591  m1modmmod  47594  zofldiv2  47604  fllogbd  47633  nnpw2blen  47653  blen1b  47661  blennngt2o2  47665  blennn0e2  47667  dig2nn1st  47678  dignn0flhalflem1  47688