Theorem 1zzd 11285

Description: 1 is an integer, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1zzd	⊢ (𝜑 → 1 ∈ ℤ)

Proof of Theorem 1zzd

Step	Hyp	Ref	Expression
1		1z 11284	. 2 ⊢ 1 ∈ ℤ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 1977  1c1 9816  ℤcz 11254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-z 11255

This theorem is referenced by:  elfz1b  12279  fzm1  12289  fzoss2  12365  fz1fzo0m1  12383  fzo1fzo0n0  12386  elfznelfzo  12439  negmod  12577  addmodid  12580  modnegd  12587  2submod  12593  sermono  12695  seqf1olem2  12703  bcp1nk  12966  eqwrds3  13552  climuni  14131  isercoll  14246  telfsumo  14375  fsumparts  14379  binomlem  14400  climcndslem2  14421  climcnds  14422  divcnv  14424  supcvg  14427  arisum  14431  trireciplem  14433  trirecip  14434  expcnv  14435  geo2sum  14443  geo2lim  14445  geoisum1  14449  geoisum1c  14450  mertenslem1  14455  mertenslem2  14456  fprodser  14518  fprodzcl  14523  risefacval2  14580  fallfacval2  14581  binomfallfaclem2  14610  bpolydiflem  14624  ege2le3  14659  rpnnen2lem12  14793  nn0o1gt2  14935  pwp1fsum  14952  bitscmp  14998  dvdsnprmd  15241  hashdvds  15318  phiprmpw  15319  prmdiv  15328  odzdvds  15338  odzphi  15339  modprm1div  15340  iserodd  15378  pcid  15415  pcmptcl  15433  pockthlem  15447  prmreclem4  15461  prmreclem6  15463  vdwapun  15516  prmdvdsprmo  15584  prmodvdslcmf  15589  prmgapprmo  15604  gsumpr12val  17105  mulgpropd  17407  sylow1lem1  17836  sylow3lem6  17870  pgpfac1lem2  18297  zringcyg  19658  mulgrhm2  19666  znunit  19731  znrrg  19733  frgpcyg  19741  cpmadugsumlemF  20500  lmcnp  20918  lmmo  20994  1stcelcls  21074  1stccnp  21075  1stckgenlem  21166  1stckgen  21167  clmvneg1  22707  clmmulg  22709  lmnn  22869  cmetcaulem  22894  iscmet2  22900  causs  22904  nglmle  22908  caubl  22914  iscmet3i  22918  ovolsf  23048  ovoliunlem1  23077  ovoliun  23080  ovoliun2  23081  ovolicc2lem2  23093  ovolicc2lem3  23094  ovolicc2lem4  23095  voliunlem2  23126  voliunlem3  23127  ioombl1lem4  23136  uniioombllem2  23157  uniioombllem3  23159  uniioombllem6  23162  vitalilem4  23186  itg1climres  23287  mbfi1fseqlem6  23293  mbfi1flimlem  23295  mbfmullem2  23297  itg2monolem1  23323  itg2i1fseq  23328  itg2i1fseq2  23329  itg2addlem  23331  plyeq0lem  23770  dvply1  23843  dvtaylp  23928  pserdvlem2  23986  pserdv2  23988  advlogexp  24201  logtayl  24206  logtaylsum  24207  logtayl2  24208  atantayl  24464  leibpilem2  24468  leibpi  24469  birthdaylem2  24479  dfef2  24497  divsqrtsumlem  24506  emcllem4  24525  emcllem6  24527  emcllem7  24528  zetacvg  24541  lgamgulmlem4  24558  lgamgulmlem6  24560  lgamgulm2  24562  lgamcvglem  24566  lgamcvg2  24581  gamcvg  24582  regamcl  24587  relgamcl  24588  wilthlem1  24594  wilthlem2  24595  basellem6  24612  basellem7  24613  basellem8  24614  basellem9  24615  mersenne  24752  perfectlem1  24754  perfectlem2  24755  lgslem1  24822  lgsqrlem1  24871  gausslemma2dlem4  24894  gausslemma2dlem6  24897  gausslemma2dlem7  24898  lgseisenlem1  24900  lgsquad2lem1  24909  lgsquad3  24912  m1lgs  24913  2sqlem11  24954  dchrisumlema  24977  dchrisumlem3  24980  dchrmusum2  24983  dchrvmasumiflem1  24990  dchrvmaeq0  24993  dchrisum0re  25002  dchrisum0lem1b  25004  dchrisum0lem2a  25006  logdivsum  25022  pntrlog2bndlem1  25066  pntpbnd2  25076  axlowdimlem6  25627  axlowdim  25641  redwlk  26136  wwlkextproplem1  26269  wwlkextproplem2  26270  clwlkfclwwlk  26371  minvecolem3  27116  minvecolem4b  27118  minvecolem4  27120  h2hcau  27220  h2hlm  27221  hlimadd  27434  hhsscms  27520  occllem  27546  nlelchi  28304  opsqrlem4  28386  hmopidmchi  28394  fzspl  28938  fzsplit3  28940  archirngz  29074  archiabllem1a  29076  smatrcl  29190  submateqlem1  29201  submateqlem2  29202  mdetlap  29226  rge0scvg  29323  lmxrge0  29326  lmdvg  29327  qqhval2lem  29353  esumfsupre  29460  esumpcvgval  29467  esumcvg  29475  eulerpartlems  29749  fiblem  29787  ballotlemfp1  29880  ballotlemimin  29894  ballotlemic  29895  ballotlem1c  29896  ballotlemsdom  29900  ballotlemsel1i  29901  ballotlemsima  29904  ballotlemfrceq  29917  ballotlemfrcn0  29918  sinccvg  30821  circum  30822  divcnvlin  30871  bcprod  30877  iprodgam  30881  faclimlem2  30883  faclim  30885  iprodfac  30886  faclim2  30887  fwddifnp1  31442  lmclim2  32724  geomcau  32725  heibor1lem  32778  heibor1  32779  bfplem1  32791  bfplem2  32792  rrncmslem  32801  rrncms  32802  fzsplit1nn0  36335  eldioph2lem1  36341  pellexlem6  36416  rmspecnonsq  36490  jm2.22  36580  jm2.23  36581  jm2.25  36584  dvradcnv2  37568  binomcxplemnn0  37570  binomcxplemrat  37571  binomcxplemnotnn0  37577  oddfl  38430  fmuldfeq  38650  fmul01lt1lem2  38652  fmul01lt1  38653  clim1fr1  38668  sumnnodd  38697  fprodsubrecnncnvlem  38794  fprodaddrecnncnvlem  38796  dvnmul  38833  stoweidlem3  38896  stoweidlem7  38900  stoweidlem11  38904  stoweidlem14  38907  stoweidlem20  38913  stoweidlem26  38919  stoweidlem34  38927  stoweidlem51  38944  wallispilem5  38962  wallispi  38963  stirlinglem1  38967  stirlinglem5  38971  stirlinglem7  38973  stirlinglem8  38974  stirlinglem10  38976  stirlinglem12  38978  stirlinglem13  38979  stirlinglem14  38980  stirlinglem15  38981  stirlingr  38983  fourierdlem4  39004  fourierdlem11  39011  fourierdlem26  39026  fourierdlem41  39041  fourierdlem42  39042  fourierdlem48  39047  fourierdlem49  39048  fourierdlem79  39078  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  etransclem15  39142  etransclem28  39155  etransclem35  39162  etransclem38  39165  etransclem44  39171  etransclem48  39175  sge0ad2en  39324  voliunsge0lem  39365  caragenunicl  39414  caratheodorylem2  39417  ovolval2lem  39533  ovolval2  39534  vonioolem2  39572  vonicclem2  39575  iccpartiltu  39960  iccpartgt  39965  fmtnoge3  39980  fmtnoprmfac1lem  40014  pwdif  40039  2pwp1prm  40041  sfprmdvdsmersenne  40058  lighneallem2  40061  perfectALTVlem2  40165  nnsum3primesprm  40206  bgoldbtbndlem3  40223  upgrewlkle2  40808  red1wlk  40881  pthdadjvtx  40936  pthdlem1  40972  wwlksnextproplem2  41116  clwlksfclwwlk  41269  2even  41723  fldivexpfllog2  42157  nnlog2ge0lt1  42158  logbpw2m1  42159  blenpw2m1  42171  blennnt2  42181  nnolog2flm1  42182  blennn0e2  42186  digexp  42199  dignn0flhalflem1  42207  dignn0flhalflem2  42208