Theorem zcnd 12436

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 10878  ℤcz 12328

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-resscn 10937

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 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287  df-neg 11217  df-z 12329

This theorem is referenced by:  zsupss  12686  rpnnen1lem5  12730  fzm1  13345  fzrevral  13350  fzshftral  13353  nn0disj  13381  predfz  13390  fzoss2  13424  fzo0addelr  13451  fzosubel  13455  fzosubel3  13457  fzocatel  13460  fzosplitsnm1  13471  elfzom1elp1fzo1  13496  2tnp1ge0ge0  13558  quoremz  13584  intfrac2  13587  intfracq  13588  flpmodeq  13603  moddiffl  13611  modmul1  13653  modmul12d  13654  modfzo0difsn  13672  modsumfzodifsn  13673  addmodlteq  13675  uzrdgxfr  13696  fzen2  13698  monoord2  13763  seqf1olem1  13771  seqf1olem2  13772  seqz  13780  expaddzlem  13835  znsqcld  13889  modexp  13962  sqoddm1div8  13967  bcm1k  14038  bcp1nk  14040  bcval5  14041  bcpasc  14044  hashfz  14151  hashfzo  14153  hashfzp1  14155  hashbclem  14173  seqcoll  14187  ccatval3  14293  ccatlid  14300  ccatass  14302  ccatalpha  14307  swrdfv0  14371  swrdfv2  14383  swrds1  14388  ccatswrd  14390  pfxfv  14404  ccatpfx  14423  swrdpfx  14429  pfxccatin12lem2  14453  spllen  14476  revccat  14488  revrev  14489  cshwidxmod  14525  cshwidxm1  14529  cshweqrep  14543  2cshwcshw  14547  cshimadifsn0  14552  swrds2m  14663  seqshft  14805  fzomaxdif  15064  climshft2  15300  iserex  15377  isercoll2  15389  serf0  15401  iseraltlem2  15403  iseraltlem3  15404  iseralt  15405  sumrblem  15432  fsumm1  15472  fsumsplitsnun  15476  fsump1  15477  fsumshftm  15502  fsumrev2  15503  telfsumo  15523  fsumparts  15527  binomlem  15550  isumshft  15560  isumsplit  15561  isum1p  15562  arisum  15581  pwdif  15589  cvgrat  15604  mertenslem1  15605  ntrivcvg  15618  ntrivcvgtail  15621  prodrblem  15648  fprodser  15668  fprodm1  15686  fprodp1  15688  fprodrev  15696  fprodmodd  15716  fallfacval3  15731  fallfacfwd  15755  0fallfac  15756  binomfallfaclem2  15759  fallfacval4  15762  fsumkthpow  15775  eirrlem  15922  sqrt2irrlem  15966  dvds2ln  16007  dvdsadd2b  16024  fsumdvds  16026  fzocongeq  16042  addmodlteqALT  16043  dvdsexp  16046  dvdsmod  16047  3dvds  16049  fprodfvdvdsd  16052  odd2np1  16059  oddm1even  16061  oexpneg  16063  mod2eq1n2dvds  16065  mulsucdiv2z  16071  zob  16077  ltoddhalfle  16079  sumodd  16106  pwp1fsum  16109  divalglem0  16111  divalglem4  16114  divalglem8  16118  divalgb  16122  divalgmod  16124  modremain  16126  flodddiv4  16131  bitsp1  16147  bitsfzo  16151  bitsmod  16152  bitsinv1lem  16157  bitsf1  16162  sadaddlem  16182  bitsres  16189  bitsuz  16190  bitsshft  16191  smumullem  16208  modgcd  16249  gcdmultipled  16251  dvdsgcdidd  16254  bezoutlem1  16256  bezoutlem2  16257  bezoutlem3  16258  bezoutlem4  16259  dvdsmulgcd  16274  rplpwr  16276  lcmid  16323  absprodnn  16332  mulgcddvds  16369  divgcdcoprm0  16379  cncongr1  16381  cncongr2  16382  rpexp  16436  qmuldeneqnum  16460  numdensq  16467  qden1elz  16470  hashdvds  16485  phiprm  16487  eulerthlem2  16492  fermltl  16494  prmdiv  16495  prmdiveq  16496  hashgcdlem  16498  odzdvds  16505  vfermltlALT  16512  modprm0  16515  modprmn0modprm0  16517  pythagtriplem6  16531  pythagtriplem7  16532  pythagtriplem15  16539  pcpremul  16553  pceulem  16555  pczpre  16557  pcdiv  16562  pcqmul  16563  pcqdiv  16567  pcexp  16569  pcaddlem  16598  pcadd  16599  fldivp1  16607  pcfac  16609  pcbc  16610  prmpwdvds  16614  prmreclem4  16629  4sqlem5  16652  4sqlem8  16655  4sqlem9  16656  4sqlem10  16657  4sqlem11  16665  4sqlem14  16668  4sqlem16  16670  4sqlem17  16671  vdwapun  16684  vdwnnlem2  16706  prmop1  16748  prmdvdsprmo  16752  prmgaplem7  16767  prmlem0  16816  mulgsubcl  18727  mulgdirlem  18743  mulgdir  18744  mulgass  18749  mulgmodid  18751  mulgsubdir  18752  psgnunilem5  19111  psgnunilem2  19112  psgnunilem4  19114  m1expaddsub  19115  psgnuni  19116  odnncl  19162  odmulg  19172  odbezout  19174  sylow1lem1  19212  sylow2alem2  19232  efgsres  19353  efgredleme  19358  efgredlemc  19360  odadd1  19458  odadd2  19459  cyggeninv  19492  gsummptshft  19546  ablfacrp  19678  pgpfac1lem3  19689  fincygsubgodd  19724  srgbinomlem3  19787  srgbinomlem4  19788  zringmulg  20687  zringlpirlem1  20693  zringlpirlem3  20695  prmirredlem  20703  zndvds0  20767  znf1o  20768  znunit  20780  cayhamlem1  22024  tgpmulg  23253  zdis  23988  uniioombllem3  24758  mbfi1fseqlem4  24892  dvexp3  25151  aareccl  25495  aalioulem1  25501  geolim3  25508  aaliou3lem2  25512  aaliou3lem6  25517  ulmshft  25558  sineq0  25689  efif1olem2  25708  igamz  26206  wilthlem1  26226  wilthlem2  26227  basellem3  26241  mumul  26339  musum  26349  musumsum  26350  muinv  26351  ppiub  26361  chtub  26369  logfac2  26374  chpchtsum  26376  dchrptlem1  26421  pcbcctr  26433  bcmono  26434  bposlem5  26445  bposlem6  26446  lgslem1  26454  lgsval2lem  26464  lgsval4a  26476  lgsneg  26478  lgsneg1  26479  lgsmod  26480  lgsdirprm  26488  lgsdir  26489  lgsdilem2  26490  lgsdi  26491  lgsne0  26492  lgsabs1  26493  lgssq  26494  lgssq2  26495  lgsmulsqcoprm  26500  lgsdirnn0  26501  lgsdinn0  26502  lgsqrlem1  26503  gausslemma2dlem1a  26522  gausslemma2dlem1  26523  gausslemma2dlem4  26526  gausslemma2dlem5a  26527  gausslemma2dlem5  26528  gausslemma2dlem6  26529  gausslemma2d  26531  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem3  26534  lgseisenlem4  26535  lgsquadlem1  26537  lgsquad2lem1  26541  lgsquad3  26544  2lgslem1b  26549  2lgsoddprmlem2  26566  2sqlem3  26577  2sqlem4  26578  2sqlem8a  26582  2sqlem8  26583  2sqlem11  26586  2sqblem  26588  2sqn0  26591  2sqmod  26593  dchrisumlem1  26646  dchrmusum2  26651  dchrvmasumlem1  26652  dchrvmasum2lem  26653  mudivsum  26687  mulogsum  26689  mulog2sumlem2  26692  selberglem1  26702  selberglem3  26704  selberg  26705  pntpbnd2  26744  pntlemf  26762  padicabvcxp  26789  axlowdimlem14  27332  axlowdimlem16  27334  pthdadjvtx  28107  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  crctcshlem4  28194  crctcsh  28198  clwwlkccatlem  28362  clwwisshclwws  28388  eucrctshift  28616  fzm1ne1  31119  fzspl  31120  bcm1n  31125  fzom1ne1  31131  dvdszzq  31138  prmdvdsbc  31139  numdenneg  31140  divnumden2  31141  ltesubnnd  31145  ccatf1  31232  swrdrn3  31236  swrdf1  31237  cshwrnid  31242  cycpmco2lem3  31404  cycpmco2lem4  31405  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2  31409  archiabllem1  31456  archiabllem2c  31458  znfermltl  31571  zrhnm  31928  cnzh  31929  rezh  31930  qqhval2lem  31940  qqhghm  31947  qqhrhm  31948  qqhnm  31949  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemic  32482  ballotlem1c  32483  ballotlemsgt1  32486  ballotlemsdom  32487  ballotlemsel1i  32488  ballotlemsf1o  32489  ballotlemsima  32491  ballotlemfrceq  32504  ballotlemfrcn0  32505  ballotlem1ri  32510  signsplypnf  32538  itgexpif  32595  fsum2dsub  32596  breprexplemc  32621  vtsprod  32628  circlemeth  32629  revpfxsfxrev  33086  swrdrevpfx  33087  revwlk  33095  swrdwlk  33097  divcnvlin  33707  fwddifnp1  34476  knoppndvlem2  34702  knoppndvlem7  34707  knoppndvlem14  34714  knoppndvlem16  34716  ltflcei  35774  poimirlem1  35787  poimirlem2  35788  poimirlem7  35793  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem24  35810  poimirlem31  35817  poimirlem32  35818  fdc  35912  mettrifi  35924  caushft  35928  cntotbnd  35963  fzsplitnd  39998  lcmineqlem6  40049  lcmineqlem18  40061  aks4d1p1p1  40078  aks4d1p8d3  40101  aks4d1p8  40102  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  metakunt12  40143  metakunt15  40146  metakunt16  40147  metakunt28  40159  oexpreposd  40328  exp11d  40332  numdenexp  40344  dvdsexpb  40349  mzpsubmpt  40572  lzenom  40599  diophun  40602  eqrabdioph  40606  irrapxlem2  40652  irrapxlem3  40653  pellexlem6  40663  pell1234qrreccl  40683  pellfund14  40727  rmxyneg  40749  rmxyadd  40750  rmxp1  40761  rmxm1  40763  rmym1  40764  rmxluc  40765  rmyluc  40766  rmyluc2  40767  rmxdbl  40768  rmydbl  40769  congadd  40795  congsub  40799  congabseq  40803  acongrep  40809  acongeq  40812  jm2.18  40817  jm2.19lem1  40818  jm2.19lem2  40819  jm2.19lem3  40820  jm2.22  40824  jm2.23  40825  jm2.20nn  40826  jm2.25  40828  jm2.26lem3  40830  jm2.27c  40836  nzss  41942  hashnzfz  41945  hashnzfz2  41946  hashnzfzclim  41947  uzmptshftfval  41971  sineq0ALT  42564  fzisoeu  42846  fperiodmul  42850  monoord2xrv  43031  fmul01lt1lem2  43133  sumnnodd  43178  dvdsn1add  43487  dvnmul  43491  dvnprodlem1  43494  stoweidlem11  43559  stoweidlem26  43574  dirkertrigeqlem1  43646  dirkertrigeqlem2  43647  dirkertrigeqlem3  43648  dirkertrigeq  43649  dirkeritg  43650  fourierdlem26  43681  fourierdlem48  43702  fourierdlem49  43703  fourierdlem79  43733  fourierdlem91  43745  fourierdlem103  43757  fourierdlem104  43758  fouriersw  43779  etransclem1  43783  etransclem4  43786  etransclem8  43790  etransclem9  43791  etransclem15  43797  etransclem17  43799  etransclem18  43800  etransclem20  43802  etransclem21  43803  etransclem22  43804  etransclem23  43805  etransclem24  43806  etransclem25  43807  etransclem35  43817  etransclem38  43820  etransclem41  43823  etransclem44  43826  etransclem45  43827  etransclem46  43828  etransclem47  43829  etransclem48  43830  2elfz2melfz  44821  fsumsplitsndif  44836  iccpartgtprec  44883  fargshiftf1  44904  fargshiftfo  44905  mod42tp1mod8  45065  sfprmdvdsmersenne  45066  lighneallem3  45070  lighneallem4b  45072  modexp2m1d  45075  dfodd6  45100  onego  45109  m1expoddALTV  45111  zofldiv2ALTV  45125  oddflALTV  45126  oexpnegALTV  45140  omoeALTV  45148  omeoALTV  45149  epoo  45166  emoo  45167  epee  45168  emee  45169  evensumeven  45170  evenltle  45180  even3prm2  45182  mogoldbblem  45183  fppr2odd  45194  fpprwppr  45202  fpprwpprb  45203  sbgoldbst  45241  sbgoldbaltlem2  45243  sgoldbeven3prm  45246  nnsum3primesprm  45253  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  bgoldbtbndlem2  45269  bgoldbtbndlem4  45271  bgoldbtbnd  45272  2zrngamnd  45510  2zrngacmnd  45511  2zrngagrp  45512  2zrngALT  45517  2zrngnmlid  45518  2zrngnmlid2  45520  ztprmneprm  45694  altgsumbcALT  45700  fldivmod  45875  m1modmmod  45878  zofldiv2  45888  fllogbd  45917  nnpw2blen  45937  blen1b  45945  blennngt2o2  45949  blennn0e2  45951  dig2nn1st  45962  dignn0flhalflem1  45972