Theorem zcnd 12748

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11182  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-neg 11523  df-z 12640

This theorem is referenced by:  zsupss  13002  rpnnen1lem5  13046  fzm1  13664  fzrevral  13669  fzshftral  13672  nn0disj  13701  predfz  13710  fzoss2  13744  fzo0addelr  13771  fzosubel  13775  fzosubel3  13777  fzocatel  13780  fzosplitsnm1  13791  elfzom1elp1fzo1  13817  2tnp1ge0ge0  13880  quoremz  13906  intfrac2  13909  intfracq  13910  flpmodeq  13925  moddiffl  13933  modmul1  13975  modmul12d  13976  modfzo0difsn  13994  modsumfzodifsn  13995  addmodlteq  13997  uzrdgxfr  14018  fzen2  14020  monoord2  14084  seqf1olem1  14092  seqf1olem2  14093  seqz  14101  expaddzlem  14156  znsqcld  14212  modexp  14287  sqoddm1div8  14292  bcm1k  14364  bcp1nk  14366  bcval5  14367  bcpasc  14370  hashfz  14476  hashfzo  14478  hashfzp1  14480  hashbclem  14501  seqcoll  14513  ccatval3  14627  ccatlid  14634  ccatass  14636  ccatalpha  14641  swrdfv0  14697  swrdfv2  14709  swrds1  14714  ccatswrd  14716  pfxfv  14730  ccatpfx  14749  swrdpfx  14755  pfxccatin12lem2  14779  spllen  14802  revccat  14814  revrev  14815  cshwidxmod  14851  cshwidxm1  14855  cshweqrep  14869  2cshwcshw  14874  cshimadifsn0  14879  swrds2m  14990  seqshft  15134  fzomaxdif  15392  climshft2  15628  iserex  15705  isercoll2  15717  serf0  15729  iseraltlem2  15731  iseraltlem3  15732  iseralt  15733  sumrblem  15759  fsumm1  15799  fsumsplitsnun  15803  fsump1  15804  fsumshftm  15829  fsumrev2  15830  telfsumo  15850  fsumparts  15854  binomlem  15877  isumshft  15887  isumsplit  15888  isum1p  15889  arisum  15908  pwdif  15916  cvgrat  15931  mertenslem1  15932  ntrivcvg  15945  ntrivcvgtail  15948  prodrblem  15977  fprodser  15997  fprodm1  16015  fprodp1  16017  fprodrev  16025  fprodmodd  16045  fallfacval3  16060  fallfacfwd  16084  0fallfac  16085  binomfallfaclem2  16088  fallfacval4  16091  fsumkthpow  16104  eirrlem  16252  sqrt2irrlem  16296  dvds2ln  16337  dvdsadd2b  16354  fsumdvds  16356  fzocongeq  16372  addmodlteqALT  16373  dvdsexp  16376  dvdsmod  16377  3dvds  16379  fprodfvdvdsd  16382  odd2np1  16389  oddm1even  16391  oexpneg  16393  mod2eq1n2dvds  16395  mulsucdiv2z  16401  zob  16407  ltoddhalfle  16409  sumodd  16436  pwp1fsum  16439  divalglem0  16441  divalglem4  16444  divalglem8  16448  divalgb  16452  divalgmod  16454  modremain  16456  flodddiv4  16461  bitsp1  16477  bitsfzo  16481  bitsmod  16482  bitsinv1lem  16487  bitsf1  16492  sadaddlem  16512  bitsres  16519  bitsuz  16520  bitsshft  16521  smumullem  16538  modgcd  16579  gcdmultipled  16581  dvdsgcdidd  16584  bezoutlem1  16586  bezoutlem2  16587  bezoutlem3  16588  bezoutlem4  16589  dvdsmulgcd  16603  rplpwr  16605  lcmid  16656  absprodnn  16665  mulgcddvds  16702  divgcdcoprm0  16712  cncongr1  16714  cncongr2  16715  dvdszzq  16768  rpexp  16769  prmdvdsbc  16773  qmuldeneqnum  16794  numdensq  16801  qden1elz  16804  numdenexp  16807  hashdvds  16822  phiprm  16824  eulerthlem2  16829  fermltl  16831  prmdiv  16832  prmdiveq  16833  hashgcdlem  16835  odzdvds  16842  vfermltlALT  16849  modprm0  16852  modprmn0modprm0  16854  pythagtriplem6  16868  pythagtriplem7  16869  pythagtriplem15  16876  pcpremul  16890  pceulem  16892  pczpre  16894  pcdiv  16899  pcqmul  16900  pcqdiv  16904  pcexp  16906  pcaddlem  16935  pcadd  16936  fldivp1  16944  pcfac  16946  pcbc  16947  prmpwdvds  16951  prmreclem4  16966  4sqlem5  16989  4sqlem8  16992  4sqlem9  16993  4sqlem10  16994  4sqlem11  17002  4sqlem14  17005  4sqlem16  17007  4sqlem17  17008  vdwapun  17021  vdwnnlem2  17043  prmop1  17085  prmdvdsprmo  17089  prmgaplem7  17104  prmlem0  17153  mulgsubcl  19128  mulgdirlem  19145  mulgdir  19146  mulgass  19151  mulgmodid  19153  mulgsubdir  19154  psgnunilem5  19536  psgnunilem2  19537  psgnunilem4  19539  m1expaddsub  19540  psgnuni  19541  odnncl  19587  odmulg  19598  odbezout  19600  sylow1lem1  19640  sylow2alem2  19660  efgsres  19780  efgredleme  19785  efgredlemc  19787  odadd1  19890  odadd2  19891  cyggeninv  19925  gsummptshft  19978  ablfacrp  20110  pgpfac1lem3  20121  fincygsubgodd  20156  srgbinomlem3  20255  srgbinomlem4  20256  zringmulg  21490  zringlpirlem1  21496  zringlpirlem3  21498  prmirredlem  21506  fermltlchr  21567  zndvds0  21592  znf1o  21593  znunit  21605  cayhamlem1  22893  tgpmulg  24122  zdis  24857  uniioombllem3  25639  mbfi1fseqlem4  25773  dvexp3  26036  aareccl  26386  aalioulem1  26392  geolim3  26399  aaliou3lem2  26403  aaliou3lem6  26408  ulmshft  26451  sineq0  26584  efif1olem2  26603  igamz  27109  wilthlem1  27129  wilthlem2  27130  basellem3  27144  mumul  27242  musum  27252  musumsum  27253  muinv  27254  ppiub  27266  chtub  27274  logfac2  27279  chpchtsum  27281  dchrptlem1  27326  pcbcctr  27338  bcmono  27339  bposlem5  27350  bposlem6  27351  lgslem1  27359  lgsval2lem  27369  lgsval4a  27381  lgsneg  27383  lgsneg1  27384  lgsmod  27385  lgsdirprm  27393  lgsdir  27394  lgsdilem2  27395  lgsdi  27396  lgsne0  27397  lgsabs1  27398  lgssq  27399  lgssq2  27400  lgsmulsqcoprm  27405  lgsdirnn0  27406  lgsdinn0  27407  lgsqrlem1  27408  gausslemma2dlem1a  27427  gausslemma2dlem1  27428  gausslemma2dlem4  27431  gausslemma2dlem5a  27432  gausslemma2dlem5  27433  gausslemma2dlem6  27434  gausslemma2d  27436  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgseisenlem4  27440  lgsquadlem1  27442  lgsquad2lem1  27446  lgsquad3  27449  2lgslem1b  27454  2lgsoddprmlem2  27471  2sqlem3  27482  2sqlem4  27483  2sqlem8a  27487  2sqlem8  27488  2sqlem11  27491  2sqblem  27493  2sqn0  27496  2sqmod  27498  dchrisumlem1  27551  dchrmusum2  27556  dchrvmasumlem1  27557  dchrvmasum2lem  27558  mudivsum  27592  mulogsum  27594  mulog2sumlem2  27597  selberglem1  27607  selberglem3  27609  selberg  27610  pntpbnd2  27649  pntlemf  27667  padicabvcxp  27694  axlowdimlem14  28988  axlowdimlem16  28990  pthdadjvtx  29766  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  crctcshlem4  29853  crctcsh  29857  clwwlkccatlem  30021  clwwisshclwws  30047  eucrctshift  30275  fzm1ne1  32794  fzspl  32795  bcm1n  32800  fzom1ne1  32806  znumd  32816  zdend  32817  numdenneg  32818  divnumden2  32819  ltesubnnd  32826  ccatf1  32915  swrdrn3  32922  swrdf1  32923  cshwrnid  32928  chnlt  32985  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2  33126  archiabllem1  33173  archiabllem2c  33175  znfermltl  33359  zringidom  33544  zringfrac  33547  zrhnm  33915  cnzh  33916  rezh  33917  qqhval2lem  33927  qqhghm  33934  qqhrhm  33935  qqhnm  33936  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemic  34471  ballotlem1c  34472  ballotlemsgt1  34475  ballotlemsdom  34476  ballotlemsel1i  34477  ballotlemsf1o  34478  ballotlemsima  34480  ballotlemfrceq  34493  ballotlemfrcn0  34494  ballotlem1ri  34499  signsplypnf  34527  itgexpif  34583  fsum2dsub  34584  breprexplemc  34609  vtsprod  34616  circlemeth  34617  revpfxsfxrev  35083  swrdrevpfx  35084  revwlk  35092  swrdwlk  35094  divcnvlin  35695  fwddifnp1  36129  knoppndvlem2  36479  knoppndvlem7  36484  knoppndvlem14  36491  knoppndvlem16  36493  ltflcei  37568  poimirlem1  37581  poimirlem2  37582  poimirlem7  37587  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem24  37604  poimirlem31  37611  poimirlem32  37612  fdc  37705  mettrifi  37717  caushft  37721  cntotbnd  37756  fzsplitnd  41939  lcmineqlem6  41991  lcmineqlem18  42003  aks4d1p1p1  42020  aks4d1p8d3  42043  aks4d1p8  42044  primrootscoprmpow  42056  posbezout  42057  primrootscoprbij  42059  primrootspoweq0  42063  hashscontpow1  42078  aks6d1c3  42080  aks6d1c4  42081  aks6d1c5lem1  42093  aks6d1c5lem2  42095  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  aks6d1c6lem3  42129  unitscyglem2  42153  unitscyglem4  42155  metakunt12  42173  metakunt15  42176  metakunt16  42177  metakunt28  42189  sumcubes  42301  oexpreposd  42309  exp11d  42313  dvdsexpb  42322  mzpsubmpt  42699  lzenom  42726  diophun  42729  eqrabdioph  42733  irrapxlem2  42779  irrapxlem3  42780  pellexlem6  42790  pell1234qrreccl  42810  pellfund14  42854  rmxyneg  42877  rmxyadd  42878  rmxp1  42889  rmxm1  42891  rmym1  42892  rmxluc  42893  rmyluc  42894  rmyluc2  42895  rmxdbl  42896  rmydbl  42897  congadd  42923  congsub  42927  congabseq  42931  acongrep  42937  acongeq  42940  jm2.18  42945  jm2.19lem1  42946  jm2.19lem2  42947  jm2.19lem3  42948  jm2.22  42952  jm2.23  42953  jm2.20nn  42954  jm2.25  42956  jm2.26lem3  42958  jm2.27c  42964  nzss  44286  hashnzfz  44289  hashnzfz2  44290  hashnzfzclim  44291  uzmptshftfval  44315  sineq0ALT  44908  fzisoeu  45215  fperiodmul  45219  monoord2xrv  45399  fmul01lt1lem2  45506  sumnnodd  45551  dvdsn1add  45860  dvnmul  45864  dvnprodlem1  45867  stoweidlem11  45932  stoweidlem26  45947  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkeritg  46023  fourierdlem26  46054  fourierdlem48  46075  fourierdlem49  46076  fourierdlem79  46106  fourierdlem91  46118  fourierdlem103  46130  fourierdlem104  46131  fouriersw  46152  etransclem1  46156  etransclem4  46159  etransclem8  46163  etransclem9  46164  etransclem15  46170  etransclem17  46172  etransclem18  46173  etransclem20  46175  etransclem21  46176  etransclem22  46177  etransclem23  46178  etransclem24  46179  etransclem25  46180  etransclem35  46190  etransclem38  46193  etransclem41  46196  etransclem44  46199  etransclem45  46200  etransclem46  46201  etransclem47  46202  etransclem48  46203  2elfz2melfz  47233  fsumsplitsndif  47247  iccpartgtprec  47294  fargshiftf1  47315  fargshiftfo  47316  mod42tp1mod8  47476  sfprmdvdsmersenne  47477  lighneallem3  47481  lighneallem4b  47483  modexp2m1d  47486  dfodd6  47511  onego  47520  m1expoddALTV  47522  zofldiv2ALTV  47536  oddflALTV  47537  oexpnegALTV  47551  omoeALTV  47559  omeoALTV  47560  epoo  47577  emoo  47578  epee  47579  emee  47580  evensumeven  47581  evenltle  47591  even3prm2  47593  mogoldbblem  47594  fppr2odd  47605  fpprwppr  47613  fpprwpprb  47614  sbgoldbst  47652  sbgoldbaltlem2  47654  sgoldbeven3prm  47657  nnsum3primesprm  47664  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbtbndlem2  47680  bgoldbtbndlem4  47682  bgoldbtbnd  47683  2zrngamnd  47970  2zrngacmnd  47971  2zrngagrp  47972  2zrngALT  47977  2zrngnmlid  47978  2zrngnmlid2  47980  ztprmneprm  48072  altgsumbcALT  48078  fldivmod  48252  m1modmmod  48255  zofldiv2  48265  fllogbd  48294  nnpw2blen  48314  blen1b  48322  blennngt2o2  48326  blennn0e2  48328  dig2nn1st  48339  dignn0flhalflem1  48349