Theorem 1zzd 9347

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

Syntax hints:   → wi 4   ∈ wcel 2164  1c1 7875  ℤcz 9320

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-setind 4570  ax-cnex 7965  ax-resscn 7966  ax-1cn 7967  ax-1re 7968  ax-icn 7969  ax-addcl 7970  ax-addrcl 7971  ax-mulcl 7972  ax-addcom 7974  ax-addass 7976  ax-distr 7978  ax-i2m1 7979  ax-0lt1 7980  ax-0id 7982  ax-rnegex 7983  ax-cnre 7985  ax-pre-ltirr 7986  ax-pre-ltwlin 7987  ax-pre-lttrn 7988  ax-pre-ltadd 7990

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2987  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-int 3872  df-br 4031  df-opab 4092  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-iota 5216  df-fun 5257  df-fv 5263  df-riota 5874  df-ov 5922  df-oprab 5923  df-mpo 5924  df-pnf 8058  df-mnf 8059  df-xr 8060  df-ltxr 8061  df-le 8062  df-sub 8194  df-neg 8195  df-inn 8985  df-z 9321

This theorem is referenced by:  uzm1  9626  elfz1b  10159  fzm1  10169  fzoss2  10242  fzo1fzo0n0  10253  qnegmod  10443  addmodid  10446  q2submod  10459  ser3mono  10561  seq3f1olemqsumkj  10585  seqf1oglem2  10594  exp3vallem  10614  exp3val  10615  exp1  10619  facnn  10801  fac0  10802  fac1  10803  bcp1nk  10836  hashfiv01gt1  10856  fseq1hash  10875  hashfz  10895  zfz1isolemsplit  10912  seq3coll  10916  resqrexlemf  11154  resqrexlemf1  11155  resqrexlemnmsq  11164  resqrexlemcvg  11166  climuni  11439  climrecvg1n  11494  climcvg1nlem  11495  nnf1o  11522  summodclem2a  11527  summodclem2  11528  summodc  11529  zsumdc  11530  fsum3  11533  sum0  11534  fisumss  11538  fsumcl2lem  11544  fsumadd  11552  sumsnf  11555  fsummulc2  11594  telfsumo  11612  fsumparts  11616  binomlem  11629  divcnv  11643  arisum  11644  arisum2  11645  trireciplem  11646  trirecip  11647  expcnvap0  11648  expcnv  11650  geo2sum  11660  geo2lim  11662  geoisum1  11665  geoisum1c  11666  cvgratnnlemseq  11672  cvgratnnlemsumlt  11674  cvgratnnlemrate  11676  cvgratnn  11677  cvgratz  11678  mertenslemub  11680  mertenslemi1  11681  mertenslem2  11682  prodmodclem3  11721  prodmodclem2a  11722  prodmodclem2  11723  zproddc  11725  fprodseq  11729  fprodssdc  11736  prodsnf  11738  fprodzcl  11755  fprodfac  11761  ege2le3  11817  modm1div  11946  nn0o1gt2  12049  nninfdcex  12093  gcdsupex  12097  gcdsupcl  12098  gcdaddm  12124  nnmindc  12174  nnminle  12175  uzwodc  12177  lcmval  12204  lcmcllem  12208  lcmledvds  12211  isprm3  12259  isprm4  12260  prmind2  12261  dvdsnprmd  12266  rpexp  12294  pw2dvds  12307  phivalfi  12353  phicl2  12355  hashdvds  12362  phiprmpw  12363  phimullem  12366  eulerthlemfi  12369  eulerthlemh  12372  eulerthlemth  12373  eulerth  12374  prmdiv  12376  hashgcdeq  12380  phisum  12381  odzcllem  12383  odzdvds  12386  odzphi  12387  pcid  12465  pcmptcl  12483  pcmpt  12484  pcfac  12491  pcbc  12492  pockthlem  12497  infpnlem2  12501  1arith  12508  4sqlem11  12542  4sqlem13m  12544  4sqlem14  12545  4sqlem17  12548  4sqlem18  12549  nninfdclemf  12609  gsumpr12val  12986  mulgval  13195  mulgfng  13197  mulgnngsum  13200  mulg1  13202  mulgnnsubcl  13207  mulgpropdg  13237  mulgrhm  14108  mulgrhm2  14109  znunit  14158  znrrg  14159  lmtopcnp  14429  dvply1  14943  relogbval  15124  relogbzcl  15125  nnlogbexp  15132  wilthlem1  15153  lgslem1  15157  lgsval  15161  lgsfvalg  15162  lgscllem  15164  lgsval2lem  15167  lgsval4a  15179  lgsneg  15181  lgsdir2  15190  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  gausslemma2dlem1  15218  gausslemma2dlem4  15221  gausslemma2dlem6  15224  gausslemma2dlem7  15225  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgseisen  15231  lgsquadlemsfi  15232  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem1  15238  lgsquad3  15241  m1lgs  15242  2lgsoddprm  15270  cvgcmp2nlemabs  15592  cvgcmp2n  15593  trilpolemcl  15597  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  dceqnconst  15620  dcapnconst  15621  nconstwlpolemgt0  15624