Theorem zcnd 11483

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

Syntax hints:   → wi 4   ∈ wcel 1990  ℂcc 9934  ℤcz 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-neg 10269  df-z 11378

This theorem is referenced by:  zsupss  11777  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  fzm1  12420  fzrevral  12425  fzshftral  12428  nn0disj  12455  predfz  12464  fzoss2  12496  fzo0addelr  12522  fzosubel  12526  fzosubel3  12528  fzocatel  12531  fzosplitsnm1  12542  elfzom1elp1fzo1  12568  2tnp1ge0ge0  12630  quoremz  12654  intfrac2  12657  intfracq  12658  flpmodeq  12673  moddiffl  12681  modmul1  12723  modmul12d  12724  modfzo0difsn  12742  modsumfzodifsn  12743  addmodlteq  12745  uzrdgxfr  12766  fzen2  12768  monoord2  12832  seqf1olem1  12840  seqf1olem2  12841  seqz  12849  expaddzlem  12903  modexp  12999  sqoddm1div8  13028  bcm1k  13102  bcp1nk  13104  bcval5  13105  bcpasc  13108  hashfz  13214  hashfzo  13216  hashfzp1  13218  hashbclem  13236  seqcoll  13248  ccatval3  13363  ccatlid  13369  ccatass  13371  ccatalpha  13375  swrd0val  13421  swrdid  13428  swrd0fv  13439  swrdfv2  13446  swrds1  13451  ccatswrd  13456  swrdswrd0  13462  spllen  13505  splfv1  13506  splfv2a  13507  revccat  13515  revrev  13516  cshwidxmod  13549  cshwidxm1  13553  cshweqrep  13567  2cshwcshw  13571  cshimadifsn0  13576  seqshft  13825  fzomaxdif  14083  climshft2  14313  iserex  14387  isercoll2  14399  serf0  14411  iseraltlem2  14413  iseraltlem3  14414  iseralt  14415  sumrblem  14442  fsumm1  14480  fsumsplitsnun  14484  fsumsplitsnunOLD  14486  fsump1  14487  fsumshftm  14513  fsumrev2  14514  telfsumo  14534  fsumparts  14538  binomlem  14561  isumshft  14571  isumsplit  14572  isum1p  14573  arisum  14592  cvgrat  14615  mertenslem1  14616  ntrivcvg  14629  ntrivcvgtail  14632  prodrblem  14659  fprodser  14679  fprodm1  14697  fprodp1  14699  fprodrev  14707  fprodmodd  14728  fallfacval3  14743  fallfacfwd  14767  0fallfac  14768  binomfallfaclem2  14771  fallfacval4  14774  fsumkthpow  14787  eirrlem  14932  sqrt2irrlem  14977  sqrt2irrlemOLD  14978  dvds2ln  15014  dvdsadd2b  15028  fsumdvds  15030  fzocongeq  15046  addmodlteqALT  15047  dvdsexp  15049  dvdsmod  15050  3dvds  15052  3dvdsOLD  15053  fprodfvdvdsd  15058  odd2np1  15065  oddm1even  15067  oexpneg  15069  mod2eq1n2dvds  15071  mulsucdiv2z  15077  zob  15083  ltoddhalfle  15085  sumodd  15111  pwp1fsum  15114  divalglem0  15116  divalglem4  15119  divalglem8  15123  divalgb  15127  divalgmod  15129  divalgmodOLD  15130  modremain  15132  flodddiv4  15137  bitsp1  15153  bitsfzo  15157  bitsmod  15158  bitsinv1lem  15163  bitsf1  15168  sadaddlem  15188  bitsres  15195  bitsuz  15196  bitsshft  15197  smumullem  15214  modgcd  15253  bezoutlem1  15256  bezoutlem2  15257  bezoutlem3  15258  bezoutlem4  15259  dvdsmulgcd  15274  rplpwr  15276  lcmid  15322  absprodnn  15331  mulgcddvds  15369  divgcdcoprm0  15379  cncongr1  15381  cncongr2  15382  rpexp  15432  qmuldeneqnum  15455  numdensq  15462  qden1elz  15465  hashdvds  15480  phiprm  15482  eulerthlem2  15487  fermltl  15489  prmdiv  15490  prmdiveq  15491  hashgcdlem  15493  odzdvds  15500  vfermltlALT  15507  modprm0  15510  modprmn0modprm0  15512  pythagtriplem6  15526  pythagtriplem7  15527  pythagtriplem15  15534  pcpremul  15548  pceulem  15550  pczpre  15552  pcdiv  15557  pcqmul  15558  pcqdiv  15562  pcexp  15564  pcaddlem  15592  pcadd  15593  fldivp1  15601  pcfac  15603  pcbc  15604  prmpwdvds  15608  prmreclem4  15623  4sqlem5  15646  4sqlem8  15649  4sqlem9  15650  4sqlem10  15651  4sqlem11  15659  4sqlem14  15662  4sqlem16  15664  4sqlem17  15665  vdwapun  15678  vdwnnlem2  15700  prmop1  15742  prmdvdsprmo  15746  prmgaplem7  15761  prmlem0  15812  mulgsubcl  17555  mulgdirlem  17572  mulgdir  17573  mulgass  17579  mulgmodid  17581  mulgsubdir  17582  psgnunilem5  17914  psgnunilem2  17915  psgnunilem4  17917  m1expaddsub  17918  psgnuni  17919  odnncl  17964  odmulg  17973  odbezout  17975  sylow1lem1  18013  sylow2alem2  18033  efgsres  18151  efgredleme  18156  efgredlemc  18158  odadd1  18251  odadd2  18252  cyggeninv  18285  gsummptshft  18336  ablfacrp  18465  pgpfac1lem3  18476  srgbinomlem3  18542  srgbinomlem4  18543  zringmulg  19826  zringlpirlem1  19832  zringlpirlem3  19834  prmirredlem  19841  zndvds0  19899  znf1o  19900  znunit  19912  cayhamlem1  20671  tgpmulg  21897  zdis  22619  uniioombllem3  23353  mbfi1fseqlem4  23485  dvexp3  23741  aareccl  24081  aalioulem1  24087  geolim3  24094  aaliou3lem2  24098  aaliou3lem6  24103  ulmshft  24144  sineq0  24273  efif1olem2  24289  igamz  24774  wilthlem1  24794  wilthlem2  24795  basellem3  24809  mumul  24907  musum  24917  musumsum  24918  muinv  24919  ppiub  24929  chtub  24937  logfac2  24942  chpchtsum  24944  dchrptlem1  24989  pcbcctr  25001  bcmono  25002  bposlem5  25013  bposlem6  25014  lgslem1  25022  lgsval2lem  25032  lgsval4a  25044  lgsneg  25046  lgsneg1  25047  lgsmod  25048  lgsdirprm  25056  lgsdir  25057  lgsdilem2  25058  lgsdi  25059  lgsne0  25060  lgsabs1  25061  lgssq  25062  lgssq2  25063  lgsmulsqcoprm  25068  lgsdirnn0  25069  lgsdinn0  25070  lgsqrlem1  25071  gausslemma2dlem1a  25090  gausslemma2dlem1  25091  gausslemma2dlem4  25094  gausslemma2dlem5a  25095  gausslemma2dlem5  25096  gausslemma2dlem6  25097  gausslemma2d  25099  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisenlem4  25103  lgsquadlem1  25105  lgsquad2lem1  25109  lgsquad3  25112  2lgslem1b  25117  2lgsoddprmlem2  25134  2sqlem3  25145  2sqlem4  25146  2sqlem8a  25150  2sqlem8  25151  2sqlem11  25154  2sqblem  25156  dchrisumlem1  25178  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasum2lem  25185  mudivsum  25219  mulogsum  25221  mulog2sumlem2  25224  selberglem1  25234  selberglem3  25236  selberg  25237  pntpbnd2  25276  pntlemf  25294  padicabvcxp  25321  axlowdimlem14  25835  axlowdimlem16  25837  pthdadjvtx  26626  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  crctcshlem4  26712  crctcsh  26716  clwwisshclwws  26928  eucrctshift  27103  znsqcld  29512  fzspl  29550  bcm1n  29554  numdenneg  29563  divnumden2  29564  ltesubnnd  29568  2sqn0  29646  2sqmod  29648  archiabllem1  29747  archiabllem2c  29749  zrhnm  30013  cnzh  30014  rezh  30015  qqhval2lem  30025  qqhghm  30032  qqhrhm  30033  qqhnm  30034  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemic  30568  ballotlem1c  30569  ballotlemsgt1  30572  ballotlemsdom  30573  ballotlemsel1i  30574  ballotlemsf1o  30575  ballotlemsima  30577  ballotlemfrceq  30590  ballotlemfrcn0  30591  ballotlem1ri  30596  signsplypnf  30627  itgexpif  30684  fsum2dsub  30685  breprexplemc  30710  vtsprod  30717  circlemeth  30718  divcnvlin  31618  fwddifnp1  32272  knoppndvlem2  32504  knoppndvlem7  32509  knoppndvlem14  32516  knoppndvlem16  32518  ltflcei  33397  poimirlem1  33410  poimirlem2  33411  poimirlem7  33416  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem24  33433  poimirlem31  33440  poimirlem32  33441  fdc  33541  mettrifi  33553  caushft  33557  cntotbnd  33595  mzpsubmpt  37306  lzenom  37333  diophun  37337  eqrabdioph  37341  irrapxlem2  37387  irrapxlem3  37388  pellexlem6  37398  pell1234qrreccl  37418  pellfund14  37462  rmxyneg  37485  rmxyadd  37486  rmxp1  37497  rmxm1  37499  rmym1  37500  rmxluc  37501  rmyluc  37502  rmyluc2  37503  rmxdbl  37504  rmydbl  37505  congadd  37533  congsub  37537  congabseq  37541  acongrep  37547  acongeq  37550  jm2.18  37555  jm2.19lem1  37556  jm2.19lem2  37557  jm2.19lem3  37558  jm2.22  37562  jm2.23  37563  jm2.20nn  37564  jm2.25  37566  jm2.26lem3  37568  jm2.27c  37574  nzss  38516  hashnzfz  38519  hashnzfz2  38520  hashnzfzclim  38521  uzmptshftfval  38545  sineq0ALT  39173  fzisoeu  39514  fperiodmul  39518  fmul01lt1lem2  39817  sumnnodd  39862  dvdsn1add  40154  dvnmul  40158  dvnprodlem1  40161  stoweidlem11  40228  stoweidlem26  40243  dirkertrigeqlem1  40315  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkeritg  40319  fourierdlem26  40350  fourierdlem48  40371  fourierdlem49  40372  fourierdlem79  40402  fourierdlem91  40414  fourierdlem103  40426  fourierdlem104  40427  fouriersw  40448  etransclem1  40452  etransclem4  40455  etransclem8  40459  etransclem9  40460  etransclem15  40466  etransclem17  40468  etransclem18  40469  etransclem20  40471  etransclem21  40472  etransclem22  40473  etransclem23  40474  etransclem24  40475  etransclem25  40476  etransclem35  40486  etransclem38  40489  etransclem41  40492  etransclem44  40495  etransclem45  40496  etransclem46  40497  etransclem47  40498  etransclem48  40499  2elfz2melfz  41328  fsumsplitsndif  41343  iccpartgtprec  41356  fargshiftf1  41377  fargshiftfo  41378  pfxfv  41399  ccatpfx  41409  pfxccatin12lem2  41424  pwdif  41501  mod42tp1mod8  41519  sfprmdvdsmersenne  41520  lighneallem3  41524  lighneallem4b  41526  modexp2m1d  41529  dfodd6  41550  onego  41559  m1expoddALTV  41561  zofldiv2ALTV  41574  oddflALTV  41575  oexpnegALTV  41588  omoeALTV  41596  omeoALTV  41597  epoo  41612  emoo  41613  epee  41614  emee  41615  evensumeven  41616  evenltle  41626  even3prm2  41628  mogoldbblem  41629  sbgoldbst  41666  sbgoldbaltlem2  41668  sgoldbeven3prm  41671  nnsum3primesprm  41678  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbndlem2  41694  bgoldbtbndlem4  41696  bgoldbtbnd  41697  2zrngamnd  41941  2zrngacmnd  41942  2zrngagrp  41943  2zrngALT  41948  2zrngnmlid  41949  2zrngnmlid2  41951  ztprmneprm  42125  altgsumbcALT  42131  fldivmod  42313  m1modmmod  42316  zofldiv2  42325  fllogbd  42354  nnpw2blen  42374  blen1b  42382  blennngt2o2  42386  blennn0e2  42388  dig2nn1st  42399  dignn0flhalflem1  42409