Theorem zcnd 12356

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 10800  ℤcz 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250

This theorem is referenced by:  zsupss  12606  rpnnen1lem5  12650  fzm1  13265  fzrevral  13270  fzshftral  13273  nn0disj  13301  predfz  13310  fzoss2  13343  fzo0addelr  13370  fzosubel  13374  fzosubel3  13376  fzocatel  13379  fzosplitsnm1  13390  elfzom1elp1fzo1  13415  2tnp1ge0ge0  13477  quoremz  13503  intfrac2  13506  intfracq  13507  flpmodeq  13522  moddiffl  13530  modmul1  13572  modmul12d  13573  modfzo0difsn  13591  modsumfzodifsn  13592  addmodlteq  13594  uzrdgxfr  13615  fzen2  13617  monoord2  13682  seqf1olem1  13690  seqf1olem2  13691  seqz  13699  expaddzlem  13754  znsqcld  13808  modexp  13881  sqoddm1div8  13886  bcm1k  13957  bcp1nk  13959  bcval5  13960  bcpasc  13963  hashfz  14070  hashfzo  14072  hashfzp1  14074  hashbclem  14092  seqcoll  14106  ccatval3  14212  ccatlid  14219  ccatass  14221  ccatalpha  14226  swrdfv0  14290  swrdfv2  14302  swrds1  14307  ccatswrd  14309  pfxfv  14323  ccatpfx  14342  swrdpfx  14348  pfxccatin12lem2  14372  spllen  14395  revccat  14407  revrev  14408  cshwidxmod  14444  cshwidxm1  14448  cshweqrep  14462  2cshwcshw  14466  cshimadifsn0  14471  swrds2m  14582  seqshft  14724  fzomaxdif  14983  climshft2  15219  iserex  15296  isercoll2  15308  serf0  15320  iseraltlem2  15322  iseraltlem3  15323  iseralt  15324  sumrblem  15351  fsumm1  15391  fsumsplitsnun  15395  fsump1  15396  fsumshftm  15421  fsumrev2  15422  telfsumo  15442  fsumparts  15446  binomlem  15469  isumshft  15479  isumsplit  15480  isum1p  15481  arisum  15500  pwdif  15508  cvgrat  15523  mertenslem1  15524  ntrivcvg  15537  ntrivcvgtail  15540  prodrblem  15567  fprodser  15587  fprodm1  15605  fprodp1  15607  fprodrev  15615  fprodmodd  15635  fallfacval3  15650  fallfacfwd  15674  0fallfac  15675  binomfallfaclem2  15678  fallfacval4  15681  fsumkthpow  15694  eirrlem  15841  sqrt2irrlem  15885  dvds2ln  15926  dvdsadd2b  15943  fsumdvds  15945  fzocongeq  15961  addmodlteqALT  15962  dvdsexp  15965  dvdsmod  15966  3dvds  15968  fprodfvdvdsd  15971  odd2np1  15978  oddm1even  15980  oexpneg  15982  mod2eq1n2dvds  15984  mulsucdiv2z  15990  zob  15996  ltoddhalfle  15998  sumodd  16025  pwp1fsum  16028  divalglem0  16030  divalglem4  16033  divalglem8  16037  divalgb  16041  divalgmod  16043  modremain  16045  flodddiv4  16050  bitsp1  16066  bitsfzo  16070  bitsmod  16071  bitsinv1lem  16076  bitsf1  16081  sadaddlem  16101  bitsres  16108  bitsuz  16109  bitsshft  16110  smumullem  16127  modgcd  16168  gcdmultipled  16170  dvdsgcdidd  16173  bezoutlem1  16175  bezoutlem2  16176  bezoutlem3  16177  bezoutlem4  16178  dvdsmulgcd  16193  rplpwr  16195  lcmid  16242  absprodnn  16251  mulgcddvds  16288  divgcdcoprm0  16298  cncongr1  16300  cncongr2  16301  rpexp  16355  qmuldeneqnum  16379  numdensq  16386  qden1elz  16389  hashdvds  16404  phiprm  16406  eulerthlem2  16411  fermltl  16413  prmdiv  16414  prmdiveq  16415  hashgcdlem  16417  odzdvds  16424  vfermltlALT  16431  modprm0  16434  modprmn0modprm0  16436  pythagtriplem6  16450  pythagtriplem7  16451  pythagtriplem15  16458  pcpremul  16472  pceulem  16474  pczpre  16476  pcdiv  16481  pcqmul  16482  pcqdiv  16486  pcexp  16488  pcaddlem  16517  pcadd  16518  fldivp1  16526  pcfac  16528  pcbc  16529  prmpwdvds  16533  prmreclem4  16548  4sqlem5  16571  4sqlem8  16574  4sqlem9  16575  4sqlem10  16576  4sqlem11  16584  4sqlem14  16587  4sqlem16  16589  4sqlem17  16590  vdwapun  16603  vdwnnlem2  16625  prmop1  16667  prmdvdsprmo  16671  prmgaplem7  16686  prmlem0  16735  mulgsubcl  18633  mulgdirlem  18649  mulgdir  18650  mulgass  18655  mulgmodid  18657  mulgsubdir  18658  psgnunilem5  19017  psgnunilem2  19018  psgnunilem4  19020  m1expaddsub  19021  psgnuni  19022  odnncl  19068  odmulg  19078  odbezout  19080  sylow1lem1  19118  sylow2alem2  19138  efgsres  19259  efgredleme  19264  efgredlemc  19266  odadd1  19364  odadd2  19365  cyggeninv  19398  gsummptshft  19452  ablfacrp  19584  pgpfac1lem3  19595  fincygsubgodd  19630  srgbinomlem3  19693  srgbinomlem4  19694  zringmulg  20590  zringlpirlem1  20596  zringlpirlem3  20598  prmirredlem  20606  zndvds0  20670  znf1o  20671  znunit  20683  cayhamlem1  21923  tgpmulg  23152  zdis  23885  uniioombllem3  24654  mbfi1fseqlem4  24788  dvexp3  25047  aareccl  25391  aalioulem1  25397  geolim3  25404  aaliou3lem2  25408  aaliou3lem6  25413  ulmshft  25454  sineq0  25585  efif1olem2  25604  igamz  26102  wilthlem1  26122  wilthlem2  26123  basellem3  26137  mumul  26235  musum  26245  musumsum  26246  muinv  26247  ppiub  26257  chtub  26265  logfac2  26270  chpchtsum  26272  dchrptlem1  26317  pcbcctr  26329  bcmono  26330  bposlem5  26341  bposlem6  26342  lgslem1  26350  lgsval2lem  26360  lgsval4a  26372  lgsneg  26374  lgsneg1  26375  lgsmod  26376  lgsdirprm  26384  lgsdir  26385  lgsdilem2  26386  lgsdi  26387  lgsne0  26388  lgsabs1  26389  lgssq  26390  lgssq2  26391  lgsmulsqcoprm  26396  lgsdirnn0  26397  lgsdinn0  26398  lgsqrlem1  26399  gausslemma2dlem1a  26418  gausslemma2dlem1  26419  gausslemma2dlem4  26422  gausslemma2dlem5a  26423  gausslemma2dlem5  26424  gausslemma2dlem6  26425  gausslemma2d  26427  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgseisenlem4  26431  lgsquadlem1  26433  lgsquad2lem1  26437  lgsquad3  26440  2lgslem1b  26445  2lgsoddprmlem2  26462  2sqlem3  26473  2sqlem4  26474  2sqlem8a  26478  2sqlem8  26479  2sqlem11  26482  2sqblem  26484  2sqn0  26487  2sqmod  26489  dchrisumlem1  26542  dchrmusum2  26547  dchrvmasumlem1  26548  dchrvmasum2lem  26549  mudivsum  26583  mulogsum  26585  mulog2sumlem2  26588  selberglem1  26598  selberglem3  26600  selberg  26601  pntpbnd2  26640  pntlemf  26658  padicabvcxp  26685  axlowdimlem14  27226  axlowdimlem16  27228  pthdadjvtx  27999  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  crctcshlem4  28086  crctcsh  28090  clwwlkccatlem  28254  clwwisshclwws  28280  eucrctshift  28508  fzm1ne1  31012  fzspl  31013  bcm1n  31018  fzom1ne1  31024  dvdszzq  31031  prmdvdsbc  31032  numdenneg  31033  divnumden2  31034  ltesubnnd  31038  ccatf1  31125  swrdrn3  31129  swrdf1  31130  cshwrnid  31135  cycpmco2lem3  31297  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2  31302  archiabllem1  31349  archiabllem2c  31351  znfermltl  31464  zrhnm  31819  cnzh  31820  rezh  31821  qqhval2lem  31831  qqhghm  31838  qqhrhm  31839  qqhnm  31840  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemic  32373  ballotlem1c  32374  ballotlemsgt1  32377  ballotlemsdom  32378  ballotlemsel1i  32379  ballotlemsf1o  32380  ballotlemsima  32382  ballotlemfrceq  32395  ballotlemfrcn0  32396  ballotlem1ri  32401  signsplypnf  32429  itgexpif  32486  fsum2dsub  32487  breprexplemc  32512  vtsprod  32519  circlemeth  32520  revpfxsfxrev  32977  swrdrevpfx  32978  revwlk  32986  swrdwlk  32988  divcnvlin  33604  fwddifnp1  34394  knoppndvlem2  34620  knoppndvlem7  34625  knoppndvlem14  34632  knoppndvlem16  34634  ltflcei  35692  poimirlem1  35705  poimirlem2  35706  poimirlem7  35711  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem24  35728  poimirlem31  35735  poimirlem32  35736  fdc  35830  mettrifi  35842  caushft  35846  cntotbnd  35881  fzsplitnd  39919  lcmineqlem6  39970  lcmineqlem18  39982  aks4d1p1p1  39999  aks4d1p8d3  40022  aks4d1p8  40023  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  metakunt12  40064  metakunt15  40067  metakunt16  40068  metakunt28  40080  oexpreposd  40242  exp11d  40246  numdenexp  40258  dvdsexpb  40263  mzpsubmpt  40481  lzenom  40508  diophun  40511  eqrabdioph  40515  irrapxlem2  40561  irrapxlem3  40562  pellexlem6  40572  pell1234qrreccl  40592  pellfund14  40636  rmxyneg  40658  rmxyadd  40659  rmxp1  40670  rmxm1  40672  rmym1  40673  rmxluc  40674  rmyluc  40675  rmyluc2  40676  rmxdbl  40677  rmydbl  40678  congadd  40704  congsub  40708  congabseq  40712  acongrep  40718  acongeq  40721  jm2.18  40726  jm2.19lem1  40727  jm2.19lem2  40728  jm2.19lem3  40729  jm2.22  40733  jm2.23  40734  jm2.20nn  40735  jm2.25  40737  jm2.26lem3  40739  jm2.27c  40745  nzss  41824  hashnzfz  41827  hashnzfz2  41828  hashnzfzclim  41829  uzmptshftfval  41853  sineq0ALT  42446  fzisoeu  42729  fperiodmul  42733  monoord2xrv  42914  fmul01lt1lem2  43016  sumnnodd  43061  dvdsn1add  43370  dvnmul  43374  dvnprodlem1  43377  stoweidlem11  43442  stoweidlem26  43457  dirkertrigeqlem1  43529  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkeritg  43533  fourierdlem26  43564  fourierdlem48  43585  fourierdlem49  43586  fourierdlem79  43616  fourierdlem91  43628  fourierdlem103  43640  fourierdlem104  43641  fouriersw  43662  etransclem1  43666  etransclem4  43669  etransclem8  43673  etransclem9  43674  etransclem15  43680  etransclem17  43682  etransclem18  43683  etransclem20  43685  etransclem21  43686  etransclem22  43687  etransclem23  43688  etransclem24  43689  etransclem25  43690  etransclem35  43700  etransclem38  43703  etransclem41  43706  etransclem44  43709  etransclem45  43710  etransclem46  43711  etransclem47  43712  etransclem48  43713  2elfz2melfz  44698  fsumsplitsndif  44713  iccpartgtprec  44760  fargshiftf1  44781  fargshiftfo  44782  mod42tp1mod8  44942  sfprmdvdsmersenne  44943  lighneallem3  44947  lighneallem4b  44949  modexp2m1d  44952  dfodd6  44977  onego  44986  m1expoddALTV  44988  zofldiv2ALTV  45002  oddflALTV  45003  oexpnegALTV  45017  omoeALTV  45025  omeoALTV  45026  epoo  45043  emoo  45044  epee  45045  emee  45046  evensumeven  45047  evenltle  45057  even3prm2  45059  mogoldbblem  45060  fppr2odd  45071  fpprwppr  45079  fpprwpprb  45080  sbgoldbst  45118  sbgoldbaltlem2  45120  sgoldbeven3prm  45123  nnsum3primesprm  45130  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  bgoldbtbndlem2  45146  bgoldbtbndlem4  45148  bgoldbtbnd  45149  2zrngamnd  45387  2zrngacmnd  45388  2zrngagrp  45389  2zrngALT  45394  2zrngnmlid  45395  2zrngnmlid2  45397  ztprmneprm  45571  altgsumbcALT  45577  fldivmod  45752  m1modmmod  45755  zofldiv2  45765  fllogbd  45794  nnpw2blen  45814  blen1b  45822  blennngt2o2  45826  blennn0e2  45828  dig2nn1st  45839  dignn0flhalflem1  45849