Theorem 1zzd 9496

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

Syntax hints:   → wi 4   ∈ wcel 2200  1c1 8023  ℤcz 9469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-cnex 8113  ax-resscn 8114  ax-1cn 8115  ax-1re 8116  ax-icn 8117  ax-addcl 8118  ax-addrcl 8119  ax-mulcl 8120  ax-addcom 8122  ax-addass 8124  ax-distr 8126  ax-i2m1 8127  ax-0lt1 8128  ax-0id 8130  ax-rnegex 8131  ax-cnre 8133  ax-pre-ltirr 8134  ax-pre-ltwlin 8135  ax-pre-lttrn 8136  ax-pre-ltadd 8138

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2802  df-sbc 3030  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-int 3927  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-iota 5284  df-fun 5326  df-fv 5332  df-riota 5966  df-ov 6016  df-oprab 6017  df-mpo 6018  df-pnf 8206  df-mnf 8207  df-xr 8208  df-ltxr 8209  df-le 8210  df-sub 8342  df-neg 8343  df-inn 9134  df-z 9470

This theorem is referenced by:  uzm1  9777  elfz1b  10315  fzm1  10325  fzoss2  10399  fzo1fzo0n0  10412  nninfdcex  10487  qnegmod  10621  addmodid  10624  q2submod  10637  ser3mono  10739  seq3f1olemqsumkj  10763  seqf1oglem2  10772  exp3vallem  10792  exp3val  10793  exp1  10797  facnn  10979  fac0  10980  fac1  10981  bcp1nk  11014  hashfiv01gt1  11034  fseq1hash  11054  hashfz  11075  zfz1isolemsplit  11092  seq3coll  11096  wrdind  11293  wrd2ind  11294  resqrexlemf  11558  resqrexlemf1  11559  resqrexlemnmsq  11568  resqrexlemcvg  11570  climuni  11844  climrecvg1n  11899  climcvg1nlem  11900  nnf1o  11927  summodclem2a  11932  summodclem2  11933  summodc  11934  zsumdc  11935  fsum3  11938  sum0  11939  fisumss  11943  fsumcl2lem  11949  fsumadd  11957  sumsnf  11960  fsummulc2  11999  telfsumo  12017  fsumparts  12021  binomlem  12034  divcnv  12048  arisum  12049  arisum2  12050  trireciplem  12051  trirecip  12052  expcnvap0  12053  expcnv  12055  geo2sum  12065  geo2lim  12067  geoisum1  12070  geoisum1c  12071  cvgratnnlemseq  12077  cvgratnnlemsumlt  12079  cvgratnnlemrate  12081  cvgratnn  12082  cvgratz  12083  mertenslemub  12085  mertenslemi1  12086  mertenslem2  12087  prodmodclem3  12126  prodmodclem2a  12127  prodmodclem2  12128  zproddc  12130  fprodseq  12134  fprodssdc  12141  prodsnf  12143  fprodzcl  12160  fprodfac  12166  ege2le3  12222  modm1div  12351  nn0o1gt2  12456  bitsfzolem  12505  bitscmp  12509  gcdsupex  12518  gcdsupcl  12519  gcdaddm  12545  nnmindc  12595  nnminle  12596  uzwodc  12598  lcmval  12625  lcmcllem  12629  lcmledvds  12632  isprm3  12680  isprm4  12681  prmind2  12682  dvdsnprmd  12687  rpexp  12715  pw2dvds  12728  phivalfi  12774  phicl2  12776  hashdvds  12783  phiprmpw  12784  phimullem  12787  eulerthlemfi  12790  eulerthlemh  12793  eulerthlemth  12794  eulerth  12795  prmdiv  12797  dvdsfi  12801  hashgcdeq  12802  odzcllem  12805  odzdvds  12808  odzphi  12809  pcid  12887  pcmptcl  12905  pcmpt  12906  pcfac  12913  pcbc  12914  pockthlem  12919  infpnlem2  12923  1arith  12930  4sqlem11  12964  4sqlem13m  12966  4sqlem14  12967  4sqlem17  12970  4sqlem18  12971  nninfdclemf  13060  gsumpr12val  13473  mulgval  13699  mulgfng  13701  mulgnngsum  13704  mulg1  13706  mulgnnsubcl  13711  mulgpropdg  13741  mulgrhm  14613  mulgrhm2  14614  znunit  14663  znrrg  14664  lmtopcnp  14964  dvply1  15479  relogbval  15665  relogbzcl  15666  nnlogbexp  15673  wilthlem1  15694  mersenne  15711  perfectlem1  15713  perfectlem2  15714  lgslem1  15719  lgsval  15723  lgsfvalg  15724  lgscllem  15726  lgsval2lem  15729  lgsval4a  15741  lgsneg  15743  lgsdir2  15752  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  gausslemma2dlem1  15780  gausslemma2dlem4  15783  gausslemma2dlem6  15786  gausslemma2dlem7  15787  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgseisen  15793  lgsquadlemsfi  15794  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem1  15800  lgsquad3  15803  m1lgs  15804  2lgsoddprm  15832  clwwlkccatlem  16195  clwwlknonex2lem2  16233  cvgcmp2nlemabs  16572  cvgcmp2n  16573  trilpolemcl  16577  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  dceqnconst  16600  dcapnconst  16601  nconstwlpolemgt0  16604