Theorem zcnd 12437

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 10879  ℤcz 12329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-resscn 10938

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3431  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5074  df-iota 6384  df-fv 6434  df-ov 7270  df-neg 11218  df-z 12330

This theorem is referenced by:  zsupss  12687  rpnnen1lem5  12731  fzm1  13346  fzrevral  13351  fzshftral  13354  nn0disj  13382  predfz  13391  fzoss2  13425  fzo0addelr  13452  fzosubel  13456  fzosubel3  13458  fzocatel  13461  fzosplitsnm1  13472  elfzom1elp1fzo1  13497  2tnp1ge0ge0  13559  quoremz  13585  intfrac2  13588  intfracq  13589  flpmodeq  13604  moddiffl  13612  modmul1  13654  modmul12d  13655  modfzo0difsn  13673  modsumfzodifsn  13674  addmodlteq  13676  uzrdgxfr  13697  fzen2  13699  monoord2  13764  seqf1olem1  13772  seqf1olem2  13773  seqz  13781  expaddzlem  13836  znsqcld  13890  modexp  13963  sqoddm1div8  13968  bcm1k  14039  bcp1nk  14041  bcval5  14042  bcpasc  14045  hashfz  14152  hashfzo  14154  hashfzp1  14156  hashbclem  14174  seqcoll  14188  ccatval3  14294  ccatlid  14301  ccatass  14303  ccatalpha  14308  swrdfv0  14372  swrdfv2  14384  swrds1  14389  ccatswrd  14391  pfxfv  14405  ccatpfx  14424  swrdpfx  14430  pfxccatin12lem2  14454  spllen  14477  revccat  14489  revrev  14490  cshwidxmod  14526  cshwidxm1  14530  cshweqrep  14544  2cshwcshw  14548  cshimadifsn0  14553  swrds2m  14664  seqshft  14806  fzomaxdif  15065  climshft2  15301  iserex  15378  isercoll2  15390  serf0  15402  iseraltlem2  15404  iseraltlem3  15405  iseralt  15406  sumrblem  15433  fsumm1  15473  fsumsplitsnun  15477  fsump1  15478  fsumshftm  15503  fsumrev2  15504  telfsumo  15524  fsumparts  15528  binomlem  15551  isumshft  15561  isumsplit  15562  isum1p  15563  arisum  15582  pwdif  15590  cvgrat  15605  mertenslem1  15606  ntrivcvg  15619  ntrivcvgtail  15622  prodrblem  15649  fprodser  15669  fprodm1  15687  fprodp1  15689  fprodrev  15697  fprodmodd  15717  fallfacval3  15732  fallfacfwd  15756  0fallfac  15757  binomfallfaclem2  15760  fallfacval4  15763  fsumkthpow  15776  eirrlem  15923  sqrt2irrlem  15967  dvds2ln  16008  dvdsadd2b  16025  fsumdvds  16027  fzocongeq  16043  addmodlteqALT  16044  dvdsexp  16047  dvdsmod  16048  3dvds  16050  fprodfvdvdsd  16053  odd2np1  16060  oddm1even  16062  oexpneg  16064  mod2eq1n2dvds  16066  mulsucdiv2z  16072  zob  16078  ltoddhalfle  16080  sumodd  16107  pwp1fsum  16110  divalglem0  16112  divalglem4  16115  divalglem8  16119  divalgb  16123  divalgmod  16125  modremain  16127  flodddiv4  16132  bitsp1  16148  bitsfzo  16152  bitsmod  16153  bitsinv1lem  16158  bitsf1  16163  sadaddlem  16183  bitsres  16190  bitsuz  16191  bitsshft  16192  smumullem  16209  modgcd  16250  gcdmultipled  16252  dvdsgcdidd  16255  bezoutlem1  16257  bezoutlem2  16258  bezoutlem3  16259  bezoutlem4  16260  dvdsmulgcd  16275  rplpwr  16277  lcmid  16324  absprodnn  16333  mulgcddvds  16370  divgcdcoprm0  16380  cncongr1  16382  cncongr2  16383  rpexp  16437  qmuldeneqnum  16461  numdensq  16468  qden1elz  16471  hashdvds  16486  phiprm  16488  eulerthlem2  16493  fermltl  16495  prmdiv  16496  prmdiveq  16497  hashgcdlem  16499  odzdvds  16506  vfermltlALT  16513  modprm0  16516  modprmn0modprm0  16518  pythagtriplem6  16532  pythagtriplem7  16533  pythagtriplem15  16540  pcpremul  16554  pceulem  16556  pczpre  16558  pcdiv  16563  pcqmul  16564  pcqdiv  16568  pcexp  16570  pcaddlem  16599  pcadd  16600  fldivp1  16608  pcfac  16610  pcbc  16611  prmpwdvds  16615  prmreclem4  16630  4sqlem5  16653  4sqlem8  16656  4sqlem9  16657  4sqlem10  16658  4sqlem11  16666  4sqlem14  16669  4sqlem16  16671  4sqlem17  16672  vdwapun  16685  vdwnnlem2  16707  prmop1  16749  prmdvdsprmo  16753  prmgaplem7  16768  prmlem0  16817  mulgsubcl  18728  mulgdirlem  18744  mulgdir  18745  mulgass  18750  mulgmodid  18752  mulgsubdir  18753  psgnunilem5  19112  psgnunilem2  19113  psgnunilem4  19115  m1expaddsub  19116  psgnuni  19117  odnncl  19163  odmulg  19173  odbezout  19175  sylow1lem1  19213  sylow2alem2  19233  efgsres  19354  efgredleme  19359  efgredlemc  19361  odadd1  19459  odadd2  19460  cyggeninv  19493  gsummptshft  19547  ablfacrp  19679  pgpfac1lem3  19690  fincygsubgodd  19725  srgbinomlem3  19788  srgbinomlem4  19789  zringmulg  20688  zringlpirlem1  20694  zringlpirlem3  20696  prmirredlem  20704  zndvds0  20768  znf1o  20769  znunit  20781  cayhamlem1  22025  tgpmulg  23254  zdis  23989  uniioombllem3  24759  mbfi1fseqlem4  24893  dvexp3  25152  aareccl  25496  aalioulem1  25502  geolim3  25509  aaliou3lem2  25513  aaliou3lem6  25518  ulmshft  25559  sineq0  25690  efif1olem2  25709  igamz  26207  wilthlem1  26227  wilthlem2  26228  basellem3  26242  mumul  26340  musum  26350  musumsum  26351  muinv  26352  ppiub  26362  chtub  26370  logfac2  26375  chpchtsum  26377  dchrptlem1  26422  pcbcctr  26434  bcmono  26435  bposlem5  26446  bposlem6  26447  lgslem1  26455  lgsval2lem  26465  lgsval4a  26477  lgsneg  26479  lgsneg1  26480  lgsmod  26481  lgsdirprm  26489  lgsdir  26490  lgsdilem2  26491  lgsdi  26492  lgsne0  26493  lgsabs1  26494  lgssq  26495  lgssq2  26496  lgsmulsqcoprm  26501  lgsdirnn0  26502  lgsdinn0  26503  lgsqrlem1  26504  gausslemma2dlem1a  26523  gausslemma2dlem1  26524  gausslemma2dlem4  26527  gausslemma2dlem5a  26528  gausslemma2dlem5  26529  gausslemma2dlem6  26530  gausslemma2d  26532  lgseisenlem1  26533  lgseisenlem2  26534  lgseisenlem3  26535  lgseisenlem4  26536  lgsquadlem1  26538  lgsquad2lem1  26542  lgsquad3  26545  2lgslem1b  26550  2lgsoddprmlem2  26567  2sqlem3  26578  2sqlem4  26579  2sqlem8a  26583  2sqlem8  26584  2sqlem11  26587  2sqblem  26589  2sqn0  26592  2sqmod  26594  dchrisumlem1  26647  dchrmusum2  26652  dchrvmasumlem1  26653  dchrvmasum2lem  26654  mudivsum  26688  mulogsum  26690  mulog2sumlem2  26693  selberglem1  26703  selberglem3  26705  selberg  26706  pntpbnd2  26745  pntlemf  26763  padicabvcxp  26790  axlowdimlem14  27333  axlowdimlem16  27335  pthdadjvtx  28106  crctcshwlkn0lem4  28186  crctcshwlkn0lem5  28187  crctcshlem4  28193  crctcsh  28197  clwwlkccatlem  28361  clwwisshclwws  28387  eucrctshift  28615  fzm1ne1  31118  fzspl  31119  bcm1n  31124  fzom1ne1  31130  dvdszzq  31137  prmdvdsbc  31138  numdenneg  31139  divnumden2  31140  ltesubnnd  31144  ccatf1  31231  swrdrn3  31235  swrdf1  31236  cshwrnid  31241  cycpmco2lem3  31403  cycpmco2lem4  31404  cycpmco2lem5  31405  cycpmco2lem6  31406  cycpmco2  31408  archiabllem1  31455  archiabllem2c  31457  znfermltl  31570  zrhnm  31927  cnzh  31928  rezh  31929  qqhval2lem  31939  qqhghm  31946  qqhrhm  31947  qqhnm  31948  ballotlemfc0  32467  ballotlemfcc  32468  ballotlemic  32481  ballotlem1c  32482  ballotlemsgt1  32485  ballotlemsdom  32486  ballotlemsel1i  32487  ballotlemsf1o  32488  ballotlemsima  32490  ballotlemfrceq  32503  ballotlemfrcn0  32504  ballotlem1ri  32509  signsplypnf  32537  itgexpif  32594  fsum2dsub  32595  breprexplemc  32620  vtsprod  32627  circlemeth  32628  revpfxsfxrev  33085  swrdrevpfx  33086  revwlk  33094  swrdwlk  33096  divcnvlin  33706  fwddifnp1  34475  knoppndvlem2  34701  knoppndvlem7  34706  knoppndvlem14  34713  knoppndvlem16  34715  ltflcei  35773  poimirlem1  35786  poimirlem2  35787  poimirlem7  35792  poimirlem16  35801  poimirlem17  35802  poimirlem19  35804  poimirlem20  35805  poimirlem24  35809  poimirlem31  35816  poimirlem32  35817  fdc  35911  mettrifi  35923  caushft  35927  cntotbnd  35962  fzsplitnd  39999  lcmineqlem6  40050  lcmineqlem18  40062  aks4d1p1p1  40079  aks4d1p8d3  40102  aks4d1p8  40103  sticksstones10  40119  sticksstones12a  40121  sticksstones12  40122  metakunt12  40144  metakunt15  40147  metakunt16  40148  metakunt28  40160  oexpreposd  40329  exp11d  40333  numdenexp  40345  dvdsexpb  40350  mzpsubmpt  40573  lzenom  40600  diophun  40603  eqrabdioph  40607  irrapxlem2  40653  irrapxlem3  40654  pellexlem6  40664  pell1234qrreccl  40684  pellfund14  40728  rmxyneg  40750  rmxyadd  40751  rmxp1  40762  rmxm1  40764  rmym1  40765  rmxluc  40766  rmyluc  40767  rmyluc2  40768  rmxdbl  40769  rmydbl  40770  congadd  40796  congsub  40800  congabseq  40804  acongrep  40810  acongeq  40813  jm2.18  40818  jm2.19lem1  40819  jm2.19lem2  40820  jm2.19lem3  40821  jm2.22  40825  jm2.23  40826  jm2.20nn  40827  jm2.25  40829  jm2.26lem3  40831  jm2.27c  40837  nzss  41916  hashnzfz  41919  hashnzfz2  41920  hashnzfzclim  41921  uzmptshftfval  41945  sineq0ALT  42538  fzisoeu  42820  fperiodmul  42824  monoord2xrv  43005  fmul01lt1lem2  43107  sumnnodd  43152  dvdsn1add  43461  dvnmul  43465  dvnprodlem1  43468  stoweidlem11  43533  stoweidlem26  43548  dirkertrigeqlem1  43620  dirkertrigeqlem2  43621  dirkertrigeqlem3  43622  dirkertrigeq  43623  dirkeritg  43624  fourierdlem26  43655  fourierdlem48  43676  fourierdlem49  43677  fourierdlem79  43707  fourierdlem91  43719  fourierdlem103  43731  fourierdlem104  43732  fouriersw  43753  etransclem1  43757  etransclem4  43760  etransclem8  43764  etransclem9  43765  etransclem15  43771  etransclem17  43773  etransclem18  43774  etransclem20  43776  etransclem21  43777  etransclem22  43778  etransclem23  43779  etransclem24  43780  etransclem25  43781  etransclem35  43791  etransclem38  43794  etransclem41  43797  etransclem44  43800  etransclem45  43801  etransclem46  43802  etransclem47  43803  etransclem48  43804  2elfz2melfz  44788  fsumsplitsndif  44803  iccpartgtprec  44850  fargshiftf1  44871  fargshiftfo  44872  mod42tp1mod8  45032  sfprmdvdsmersenne  45033  lighneallem3  45037  lighneallem4b  45039  modexp2m1d  45042  dfodd6  45067  onego  45076  m1expoddALTV  45078  zofldiv2ALTV  45092  oddflALTV  45093  oexpnegALTV  45107  omoeALTV  45115  omeoALTV  45116  epoo  45133  emoo  45134  epee  45135  emee  45136  evensumeven  45137  evenltle  45147  even3prm2  45149  mogoldbblem  45150  fppr2odd  45161  fpprwppr  45169  fpprwpprb  45170  sbgoldbst  45208  sbgoldbaltlem2  45210  sgoldbeven3prm  45213  nnsum3primesprm  45220  nnsum4primesodd  45226  nnsum4primesoddALTV  45227  nnsum4primeseven  45230  nnsum4primesevenALTV  45231  bgoldbtbndlem2  45236  bgoldbtbndlem4  45238  bgoldbtbnd  45239  2zrngamnd  45477  2zrngacmnd  45478  2zrngagrp  45479  2zrngALT  45484  2zrngnmlid  45485  2zrngnmlid2  45487  ztprmneprm  45661  altgsumbcALT  45667  fldivmod  45842  m1modmmod  45845  zofldiv2  45855  fllogbd  45884  nnpw2blen  45904  blen1b  45912  blennngt2o2  45916  blennn0e2  45918  dig2nn1st  45929  dignn0flhalflem1  45939