Theorem 1zzd 11408

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 11407	. 2 ⊢ 1 ∈ ℤ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 1990  1c1 9937  ℤcz 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-z 11378

This theorem is referenced by:  fzm1  12420  fzoss2  12496  fz1fzo0m1  12515  fzo1fzo0n0  12518  elfznelfzo  12573  negmod  12715  addmodid  12718  modnegd  12725  2submod  12731  sermono  12833  seqf1olem2  12841  bcp1nk  13104  eqwrds3  13704  climuni  14283  isercoll  14398  telfsumo  14534  fsumparts  14538  binomlem  14561  climcndslem2  14582  climcnds  14583  divcnv  14585  supcvg  14588  arisum  14592  trireciplem  14594  trirecip  14595  expcnv  14596  geo2sum  14604  geo2lim  14606  geoisum1  14610  geoisum1c  14611  mertenslem1  14616  mertenslem2  14617  fprodser  14679  fprodzcl  14684  risefacval2  14741  fallfacval2  14742  binomfallfaclem2  14771  bpolydiflem  14785  ege2le3  14820  rpnnen2lem12  14954  nn0o1gt2  15097  pwp1fsum  15114  bitscmp  15160  dvdsnprmd  15403  hashdvds  15480  phiprmpw  15481  prmdiv  15490  odzdvds  15500  odzphi  15501  modprm1div  15502  iserodd  15540  pcid  15577  pcmptcl  15595  pockthlem  15609  prmreclem4  15623  prmreclem6  15625  vdwapun  15678  prmdvdsprmo  15746  prmodvdslcmf  15751  prmgapprmo  15766  gsumpr12val  17282  mulgpropd  17584  sylow1lem1  18013  sylow3lem6  18047  pgpfac1lem2  18474  zringcyg  19839  mulgrhm2  19847  znunit  19912  znrrg  19914  frgpcyg  19922  cpmadugsumlemF  20681  lmcnp  21108  lmmo  21184  1stcelcls  21264  1stccnp  21265  1stckgenlem  21356  1stckgen  21357  clmvneg1  22899  clmmulg  22901  lmnn  23061  cmetcaulem  23086  iscmet2  23092  causs  23096  nglmle  23100  caubl  23106  iscmet3i  23110  ovolsf  23241  ovoliunlem1  23270  ovoliun  23273  ovoliun2  23274  ovolicc2lem2  23286  ovolicc2lem3  23287  ovolicc2lem4  23288  voliunlem2  23319  voliunlem3  23320  ioombl1lem4  23329  uniioombllem2  23351  uniioombllem3  23353  uniioombllem6  23356  vitalilem4  23380  itg1climres  23481  mbfi1fseqlem6  23487  mbfi1flimlem  23489  mbfmullem2  23491  itg2monolem1  23517  itg2i1fseq  23522  itg2i1fseq2  23523  itg2addlem  23525  plyeq0lem  23966  dvply1  24039  dvtaylp  24124  pserdvlem2  24182  pserdv2  24184  advlogexp  24401  logtayl  24406  logtaylsum  24407  logtayl2  24408  atantayl  24664  leibpilem2  24668  leibpi  24669  birthdaylem2  24679  dfef2  24697  divsqrtsumlem  24706  emcllem4  24725  emcllem6  24727  emcllem7  24728  zetacvg  24741  lgamgulmlem4  24758  lgamgulmlem6  24760  lgamgulm2  24762  lgamcvglem  24766  lgamcvg2  24781  gamcvg  24782  regamcl  24787  relgamcl  24788  wilthlem1  24794  wilthlem2  24795  basellem6  24812  basellem7  24813  basellem8  24814  basellem9  24815  mersenne  24952  perfectlem1  24954  perfectlem2  24955  lgslem1  25022  lgsqrlem1  25071  gausslemma2dlem4  25094  gausslemma2dlem6  25097  gausslemma2dlem7  25098  lgseisenlem1  25100  lgsquad2lem1  25109  lgsquad3  25112  m1lgs  25113  2sqlem11  25154  dchrisumlema  25177  dchrisumlem3  25180  dchrmusum2  25183  dchrvmasumiflem1  25190  dchrvmaeq0  25193  dchrisum0re  25202  dchrisum0lem1b  25204  dchrisum0lem2a  25206  logdivsum  25222  pntrlog2bndlem1  25266  pntpbnd2  25276  axlowdimlem6  25827  axlowdim  25841  upgrewlkle2  26502  redwlk  26569  pthdadjvtx  26626  pthdlem1  26662  wwlksnextproplem2  26805  clwlksfclwwlk  26962  minvecolem3  27732  minvecolem4b  27734  minvecolem4  27736  h2hcau  27836  h2hlm  27837  hlimadd  28050  hhsscms  28136  occllem  28162  nlelchi  28920  opsqrlem4  29002  hmopidmchi  29010  fzspl  29550  fzsplit3  29553  archirngz  29743  archiabllem1a  29745  smatrcl  29862  submateqlem1  29873  submateqlem2  29874  mdetlap  29898  rge0scvg  29995  lmxrge0  29998  lmdvg  29999  qqhval2lem  30025  esumfsupre  30133  esumpcvgval  30140  esumcvg  30148  eulerpartlems  30422  fiblem  30460  ballotlemfp1  30553  ballotlemimin  30567  ballotlemic  30568  ballotlem1c  30569  ballotlemsdom  30573  ballotlemsel1i  30574  ballotlemsima  30577  ballotlemfrceq  30590  ballotlemfrcn0  30591  chtvalz  30707  sinccvg  31567  circum  31568  divcnvlin  31618  bcprod  31624  iprodgam  31628  faclimlem2  31630  faclim  31632  iprodfac  31633  faclim2  31634  fwddifnp1  32272  lmclim2  33554  geomcau  33555  heibor1lem  33608  heibor1  33609  bfplem1  33621  bfplem2  33622  rrncmslem  33631  rrncms  33632  fzsplit1nn0  37317  eldioph2lem1  37323  pellexlem6  37398  rmspecnonsq  37472  jm2.22  37562  jm2.23  37563  jm2.25  37566  dvradcnv2  38546  binomcxplemnn0  38548  binomcxplemrat  38549  binomcxplemnotnn0  38555  oddfl  39489  uzubioo  39794  fmuldfeq  39815  fmul01lt1lem2  39817  fmul01lt1  39818  clim1fr1  39833  sumnnodd  39862  limsup10exlem  40004  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  dvnmul  40158  stoweidlem3  40220  stoweidlem7  40224  stoweidlem11  40228  stoweidlem14  40231  stoweidlem20  40237  stoweidlem26  40243  stoweidlem34  40251  stoweidlem51  40268  wallispilem5  40286  wallispi  40287  stirlinglem1  40291  stirlinglem5  40295  stirlinglem7  40297  stirlinglem8  40298  stirlinglem10  40300  stirlinglem12  40302  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  stirlingr  40307  fourierdlem4  40328  fourierdlem11  40335  fourierdlem26  40350  fourierdlem41  40365  fourierdlem42  40366  fourierdlem48  40371  fourierdlem49  40372  fourierdlem79  40402  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  etransclem15  40466  etransclem28  40479  etransclem35  40486  etransclem38  40489  etransclem44  40495  etransclem48  40499  sge0ad2en  40648  voliunsge0lem  40689  caragenunicl  40738  caratheodorylem2  40741  ovolval2lem  40857  ovolval2  40858  vonioolem2  40895  vonicclem2  40898  iccpartiltu  41358  iccpartgt  41363  fmtnoge3  41442  fmtnoprmfac1lem  41476  pwdif  41501  2pwp1prm  41503  sfprmdvdsmersenne  41520  lighneallem2  41523  perfectALTVlem2  41631  nnsum3primesprm  41678  bgoldbtbndlem3  41695  2even  41933  fldivexpfllog2  42359  nnlog2ge0lt1  42360  logbpw2m1  42361  blenpw2m1  42373  blennnt2  42383  nnolog2flm1  42384  blennn0e2  42388  digexp  42401  dignn0flhalflem1  42409  dignn0flhalflem2  42410