Theorem zcnd 12696

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11125  ℤcz 12586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-resscn 11184

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-neg 11467  df-z 12587

This theorem is referenced by:  zsupss  12951  rpnnen1lem5  12995  fzm1  13622  fzrevral  13627  fzshftral  13630  nn0disj  13659  predfz  13668  fzoss2  13702  elfzo0suble  13721  fzo0addelr  13733  elfzoext  13736  fzosubel  13738  fzosubel3  13740  fzocatel  13743  fzosplitsnm1  13754  elfzom1elp1fzo1  13781  2tnp1ge0ge0  13844  quoremz  13870  intfrac2  13873  intfracq  13874  flpmodeq  13889  moddiffl  13897  modmul1  13940  modmul12d  13941  modfzo0difsn  13959  modsumfzodifsn  13960  addmodlteq  13962  uzrdgxfr  13983  fzen2  13985  monoord2  14049  seqf1olem1  14057  seqf1olem2  14058  seqz  14066  expaddzlem  14121  znsqcld  14178  modexp  14254  sqoddm1div8  14259  bcm1k  14331  bcp1nk  14333  bcval5  14334  bcpasc  14337  hashfz  14443  hashfzo  14445  hashfzp1  14447  hashbclem  14468  seqcoll  14480  ccatval3  14595  ccatlid  14602  ccatass  14604  ccatalpha  14609  swrdfv0  14665  swrdfv2  14677  swrds1  14682  ccatswrd  14684  pfxfv  14698  ccatpfx  14717  swrdpfx  14723  pfxccatin12lem2  14747  spllen  14770  revccat  14782  revrev  14783  cshwidxmod  14819  cshwidxm1  14823  cshweqrep  14837  2cshwcshw  14842  cshimadifsn0  14847  swrds2m  14958  seqshft  15102  fzomaxdif  15360  climshft2  15596  iserex  15671  isercoll2  15683  serf0  15695  iseraltlem2  15697  iseraltlem3  15698  iseralt  15699  sumrblem  15725  fsumm1  15765  fsumsplitsnun  15769  fsump1  15770  fsumshftm  15795  fsumrev2  15796  telfsumo  15816  fsumparts  15820  binomlem  15843  isumshft  15853  isumsplit  15854  isum1p  15855  arisum  15874  pwdif  15882  cvgrat  15897  mertenslem1  15898  ntrivcvg  15911  ntrivcvgtail  15914  prodrblem  15943  fprodser  15963  fprodm1  15981  fprodp1  15983  fprodrev  15991  fprodmodd  16011  fallfacval3  16026  fallfacfwd  16050  0fallfac  16051  binomfallfaclem2  16054  fallfacval4  16057  fsumkthpow  16070  eirrlem  16220  sqrt2irrlem  16264  addmulmodb  16283  dvds2ln  16306  dvdsadd2b  16323  fsumdvds  16325  fzocongeq  16341  addmodlteqALT  16342  dvdsexp  16345  dvdsmod  16346  3dvds  16348  fprodfvdvdsd  16351  odd2np1  16358  oddm1even  16360  oexpneg  16362  mod2eq1n2dvds  16364  mulsucdiv2z  16370  zob  16376  ltoddhalfle  16378  sumodd  16405  pwp1fsum  16408  divalglem0  16410  divalglem4  16413  divalglem8  16417  divalgb  16421  divalgmod  16423  modremain  16425  flodddiv4  16432  bitsp1  16448  bitsfzo  16452  bitsmod  16453  bitsinv1lem  16458  bitsf1  16463  sadaddlem  16483  bitsres  16490  bitsuz  16491  bitsshft  16492  smumullem  16509  modgcd  16549  gcdmultipled  16551  dvdsgcdidd  16554  bezoutlem1  16556  bezoutlem2  16557  bezoutlem3  16558  bezoutlem4  16559  dvdsmulgcd  16573  rplpwr  16575  lcmid  16626  absprodnn  16635  mulgcddvds  16672  divgcdcoprm0  16682  cncongr1  16684  cncongr2  16685  dvdszzq  16738  rpexp  16739  prmdvdsbc  16743  qmuldeneqnum  16764  numdensq  16771  qden1elz  16774  numdenexp  16777  hashdvds  16792  phiprm  16794  eulerthlem2  16799  fermltl  16801  prmdiv  16802  prmdiveq  16803  hashgcdlem  16805  odzdvds  16813  vfermltlALT  16820  modprm0  16823  modprmn0modprm0  16825  pythagtriplem6  16839  pythagtriplem7  16840  pythagtriplem15  16847  pcpremul  16861  pceulem  16863  pczpre  16865  pcdiv  16870  pcqmul  16871  pcqdiv  16875  pcexp  16877  pcaddlem  16906  pcadd  16907  fldivp1  16915  pcfac  16917  pcbc  16918  prmpwdvds  16922  prmreclem4  16937  4sqlem5  16960  4sqlem8  16963  4sqlem9  16964  4sqlem10  16965  4sqlem11  16973  4sqlem14  16976  4sqlem16  16978  4sqlem17  16979  vdwapun  16992  vdwnnlem2  17014  prmop1  17056  prmdvdsprmo  17060  prmgaplem7  17075  prmlem0  17123  mulgsubcl  19069  mulgdirlem  19086  mulgdir  19087  mulgass  19092  mulgmodid  19094  mulgsubdir  19095  psgnunilem5  19473  psgnunilem2  19474  psgnunilem4  19476  m1expaddsub  19477  psgnuni  19478  odnncl  19524  odmulg  19535  odbezout  19537  sylow1lem1  19577  sylow2alem2  19597  efgsres  19717  efgredleme  19722  efgredlemc  19724  odadd1  19827  odadd2  19828  cyggeninv  19862  gsummptshft  19915  ablfacrp  20047  pgpfac1lem3  20058  fincygsubgodd  20093  srgbinomlem3  20186  srgbinomlem4  20187  zringmulg  21415  zringlpirlem1  21421  zringlpirlem3  21423  prmirredlem  21431  fermltlchr  21488  zndvds0  21509  znf1o  21510  znunit  21522  cayhamlem1  22802  tgpmulg  24029  zdis  24754  uniioombllem3  25536  mbfi1fseqlem4  25669  dvexp3  25932  aareccl  26284  aalioulem1  26290  geolim3  26297  aaliou3lem2  26301  aaliou3lem6  26306  ulmshft  26349  sineq0  26483  efif1olem2  26502  igamz  27008  wilthlem1  27028  wilthlem2  27029  basellem3  27043  mumul  27141  musum  27151  musumsum  27152  muinv  27153  ppiub  27165  chtub  27173  logfac2  27178  chpchtsum  27180  dchrptlem1  27225  pcbcctr  27237  bcmono  27238  bposlem5  27249  bposlem6  27250  lgslem1  27258  lgsval2lem  27268  lgsval4a  27280  lgsneg  27282  lgsneg1  27283  lgsmod  27284  lgsdirprm  27292  lgsdir  27293  lgsdilem2  27294  lgsdi  27295  lgsne0  27296  lgsabs1  27297  lgssq  27298  lgssq2  27299  lgsmulsqcoprm  27304  lgsdirnn0  27305  lgsdinn0  27306  lgsqrlem1  27307  gausslemma2dlem1a  27326  gausslemma2dlem1  27327  gausslemma2dlem4  27330  gausslemma2dlem5a  27331  gausslemma2dlem5  27332  gausslemma2dlem6  27333  gausslemma2d  27335  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgseisenlem4  27339  lgsquadlem1  27341  lgsquad2lem1  27345  lgsquad3  27348  2lgslem1b  27353  2lgsoddprmlem2  27370  2sqlem3  27381  2sqlem4  27382  2sqlem8a  27386  2sqlem8  27387  2sqlem11  27390  2sqblem  27392  2sqn0  27395  2sqmod  27397  dchrisumlem1  27450  dchrmusum2  27455  dchrvmasumlem1  27456  dchrvmasum2lem  27457  mudivsum  27491  mulogsum  27493  mulog2sumlem2  27496  selberglem1  27506  selberglem3  27508  selberg  27509  pntpbnd2  27548  pntlemf  27566  padicabvcxp  27593  axlowdimlem14  28880  axlowdimlem16  28882  pthdadjvtx  29656  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  crctcshlem4  29748  crctcsh  29752  clwwlkccatlem  29916  clwwisshclwws  29942  eucrctshift  30170  fzm1ne1  32711  fzspl  32712  bcm1n  32718  fzom1ne1  32724  elq2  32736  znumd  32737  zdend  32738  numdenneg  32739  divnumden2  32740  ltesubnnd  32747  ccatf1  32870  swrdrn3  32877  swrdf1  32878  cshwrnid  32883  chnlt  32939  gsumzrsum  32999  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2  33090  archiabllem1  33137  archiabllem2c  33139  elrgspnlem1  33183  elrgspnlem2  33184  znfermltl  33327  zringidom  33512  zringfrac  33515  zconstr  33744  cos9thpiminplylem2  33763  zrhnm  33944  cnzh  33945  rezh  33946  zrhcntr  33956  qqhval2lem  33958  qqhghm  33965  qqhrhm  33966  qqhnm  33967  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemic  34485  ballotlem1c  34486  ballotlemsgt1  34489  ballotlemsdom  34490  ballotlemsel1i  34491  ballotlemsf1o  34492  ballotlemsima  34494  ballotlemfrceq  34507  ballotlemfrcn0  34508  ballotlem1ri  34513  signsplypnf  34528  itgexpif  34584  fsum2dsub  34585  breprexplemc  34610  vtsprod  34617  circlemeth  34618  revpfxsfxrev  35084  swrdrevpfx  35085  revwlk  35093  swrdwlk  35095  divcnvlin  35696  fwddifnp1  36129  knoppndvlem2  36477  knoppndvlem7  36482  knoppndvlem14  36489  knoppndvlem16  36491  ltflcei  37578  poimirlem1  37591  poimirlem2  37592  poimirlem7  37597  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem24  37614  poimirlem31  37621  poimirlem32  37622  fdc  37715  mettrifi  37727  caushft  37731  cntotbnd  37766  fzsplitnd  41941  lcmineqlem6  41993  lcmineqlem18  42005  aks4d1p1p1  42022  aks4d1p8d3  42045  aks4d1p8  42046  primrootscoprmpow  42058  posbezout  42059  primrootscoprbij  42061  primrootspoweq0  42065  hashscontpow1  42080  aks6d1c3  42082  aks6d1c4  42083  aks6d1c5lem1  42095  aks6d1c5lem2  42097  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  aks6d1c6lem3  42131  unitscyglem2  42155  unitscyglem4  42157  metakunt12  42175  metakunt15  42178  metakunt16  42179  metakunt28  42191  sumcubes  42309  oexpreposd  42318  exp11d  42322  dvdsexpb  42331  mzpsubmpt  42713  lzenom  42740  diophun  42743  eqrabdioph  42747  irrapxlem2  42793  irrapxlem3  42794  pellexlem6  42804  pell1234qrreccl  42824  pellfund14  42868  rmxyneg  42891  rmxyadd  42892  rmxp1  42903  rmxm1  42905  rmym1  42906  rmxluc  42907  rmyluc  42908  rmyluc2  42909  rmxdbl  42910  rmydbl  42911  congadd  42937  congsub  42941  congabseq  42945  acongrep  42951  acongeq  42954  jm2.18  42959  jm2.19lem1  42960  jm2.19lem2  42961  jm2.19lem3  42962  jm2.22  42966  jm2.23  42967  jm2.20nn  42968  jm2.25  42970  jm2.26lem3  42972  jm2.27c  42978  nzss  44289  hashnzfz  44292  hashnzfz2  44293  hashnzfzclim  44294  uzmptshftfval  44318  sineq0ALT  44909  fzisoeu  45277  fperiodmul  45281  monoord2xrv  45458  fmul01lt1lem2  45562  sumnnodd  45607  dvdsn1add  45916  dvnmul  45920  dvnprodlem1  45923  stoweidlem11  45988  stoweidlem26  46003  dirkertrigeqlem1  46075  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkeritg  46079  fourierdlem26  46110  fourierdlem48  46131  fourierdlem49  46132  fourierdlem79  46162  fourierdlem91  46174  fourierdlem103  46186  fourierdlem104  46187  fouriersw  46208  etransclem1  46212  etransclem4  46215  etransclem8  46219  etransclem9  46220  etransclem15  46226  etransclem17  46228  etransclem18  46229  etransclem20  46231  etransclem21  46232  etransclem22  46233  etransclem23  46234  etransclem24  46235  etransclem25  46236  etransclem35  46246  etransclem38  46249  etransclem41  46252  etransclem44  46255  etransclem45  46256  etransclem46  46257  etransclem47  46258  etransclem48  46259  2elfz2melfz  47295  ceilbi  47310  fldivmod  47315  submodaddmod  47318  zplusmodne  47320  m1modne  47325  minusmod5ne  47326  submodlt  47327  minusmodnep2tmod  47330  fsumsplitsndif  47335  iccpartgtprec  47382  fargshiftf1  47403  fargshiftfo  47404  mod42tp1mod8  47564  sfprmdvdsmersenne  47565  lighneallem3  47569  lighneallem4b  47571  modexp2m1d  47574  dfodd6  47599  onego  47608  m1expoddALTV  47610  zofldiv2ALTV  47624  oddflALTV  47625  oexpnegALTV  47639  omoeALTV  47647  omeoALTV  47648  epoo  47665  emoo  47666  epee  47667  emee  47668  evensumeven  47669  evenltle  47679  even3prm2  47681  mogoldbblem  47682  fppr2odd  47693  fpprwppr  47701  fpprwpprb  47702  sbgoldbst  47740  sbgoldbaltlem2  47742  sgoldbeven3prm  47745  nnsum3primesprm  47752  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  bgoldbtbndlem2  47768  bgoldbtbndlem4  47770  bgoldbtbnd  47771  gpgedgvtx1  48014  gpgvtxedg0  48015  gpgvtxedg1  48016  gpg3nbgrvtxlem  48017  gpg5nbgrvtx13starlem2  48022  gpg3nbgrvtx0  48026  2zrngamnd  48170  2zrngacmnd  48171  2zrngagrp  48172  2zrngALT  48177  2zrngnmlid  48178  2zrngnmlid2  48180  ztprmneprm  48270  altgsumbcALT  48276  m1modmmod  48449  zofldiv2  48459  fllogbd  48488  nnpw2blen  48508  blen1b  48516  blennngt2o2  48520  blennn0e2  48522  dig2nn1st  48533  dignn0flhalflem1  48543