Theorem 1zzd 9381

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

Syntax hints:   → wi 4   ∈ wcel 2175  1c1 7908  ℤcz 9354

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4478  ax-setind 4583  ax-cnex 7998  ax-resscn 7999  ax-1cn 8000  ax-1re 8001  ax-icn 8002  ax-addcl 8003  ax-addrcl 8004  ax-mulcl 8005  ax-addcom 8007  ax-addass 8009  ax-distr 8011  ax-i2m1 8012  ax-0lt1 8013  ax-0id 8015  ax-rnegex 8016  ax-cnre 8018  ax-pre-ltirr 8019  ax-pre-ltwlin 8020  ax-pre-lttrn 8021  ax-pre-ltadd 8023

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-nel 2471  df-ral 2488  df-rex 2489  df-reu 2490  df-rab 2492  df-v 2773  df-sbc 2998  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-opab 4105  df-id 4338  df-xp 4679  df-rel 4680  df-cnv 4681  df-co 4682  df-dm 4683  df-iota 5229  df-fun 5270  df-fv 5276  df-riota 5889  df-ov 5937  df-oprab 5938  df-mpo 5939  df-pnf 8091  df-mnf 8092  df-xr 8093  df-ltxr 8094  df-le 8095  df-sub 8227  df-neg 8228  df-inn 9019  df-z 9355

This theorem is referenced by:  uzm1  9661  elfz1b  10194  fzm1  10204  fzoss2  10277  fzo1fzo0n0  10288  nninfdcex  10361  qnegmod  10495  addmodid  10498  q2submod  10511  ser3mono  10613  seq3f1olemqsumkj  10637  seqf1oglem2  10646  exp3vallem  10666  exp3val  10667  exp1  10671  facnn  10853  fac0  10854  fac1  10855  bcp1nk  10888  hashfiv01gt1  10908  fseq1hash  10927  hashfz  10947  zfz1isolemsplit  10964  seq3coll  10968  resqrexlemf  11237  resqrexlemf1  11238  resqrexlemnmsq  11247  resqrexlemcvg  11249  climuni  11523  climrecvg1n  11578  climcvg1nlem  11579  nnf1o  11606  summodclem2a  11611  summodclem2  11612  summodc  11613  zsumdc  11614  fsum3  11617  sum0  11618  fisumss  11622  fsumcl2lem  11628  fsumadd  11636  sumsnf  11639  fsummulc2  11678  telfsumo  11696  fsumparts  11700  binomlem  11713  divcnv  11727  arisum  11728  arisum2  11729  trireciplem  11730  trirecip  11731  expcnvap0  11732  expcnv  11734  geo2sum  11744  geo2lim  11746  geoisum1  11749  geoisum1c  11750  cvgratnnlemseq  11756  cvgratnnlemsumlt  11758  cvgratnnlemrate  11760  cvgratnn  11761  cvgratz  11762  mertenslemub  11764  mertenslemi1  11765  mertenslem2  11766  prodmodclem3  11805  prodmodclem2a  11806  prodmodclem2  11807  zproddc  11809  fprodseq  11813  fprodssdc  11820  prodsnf  11822  fprodzcl  11839  fprodfac  11845  ege2le3  11901  modm1div  12030  nn0o1gt2  12135  bitsfzolem  12184  bitscmp  12188  gcdsupex  12197  gcdsupcl  12198  gcdaddm  12224  nnmindc  12274  nnminle  12275  uzwodc  12277  lcmval  12304  lcmcllem  12308  lcmledvds  12311  isprm3  12359  isprm4  12360  prmind2  12361  dvdsnprmd  12366  rpexp  12394  pw2dvds  12407  phivalfi  12453  phicl2  12455  hashdvds  12462  phiprmpw  12463  phimullem  12466  eulerthlemfi  12469  eulerthlemh  12472  eulerthlemth  12473  eulerth  12474  prmdiv  12476  dvdsfi  12480  hashgcdeq  12481  odzcllem  12484  odzdvds  12487  odzphi  12488  pcid  12566  pcmptcl  12584  pcmpt  12585  pcfac  12592  pcbc  12593  pockthlem  12598  infpnlem2  12602  1arith  12609  4sqlem11  12643  4sqlem13m  12645  4sqlem14  12646  4sqlem17  12649  4sqlem18  12650  nninfdclemf  12739  gsumpr12val  13150  mulgval  13376  mulgfng  13378  mulgnngsum  13381  mulg1  13383  mulgnnsubcl  13388  mulgpropdg  13418  mulgrhm  14289  mulgrhm2  14290  znunit  14339  znrrg  14340  lmtopcnp  14640  dvply1  15155  relogbval  15341  relogbzcl  15342  nnlogbexp  15349  wilthlem1  15370  mersenne  15387  perfectlem1  15389  perfectlem2  15390  lgslem1  15395  lgsval  15399  lgsfvalg  15400  lgscllem  15402  lgsval2lem  15405  lgsval4a  15417  lgsneg  15419  lgsdir2  15428  lgsdir  15430  lgsdilem2  15431  lgsdi  15432  lgsne0  15433  gausslemma2dlem1  15456  gausslemma2dlem4  15459  gausslemma2dlem6  15462  gausslemma2dlem7  15463  lgseisenlem1  15465  lgseisenlem2  15466  lgseisenlem3  15467  lgseisenlem4  15468  lgseisen  15469  lgsquadlemsfi  15470  lgsquadlem1  15472  lgsquadlem2  15473  lgsquadlem3  15474  lgsquad2lem1  15476  lgsquad3  15479  m1lgs  15480  2lgsoddprm  15508  cvgcmp2nlemabs  15835  cvgcmp2n  15836  trilpolemcl  15840  trilpolemisumle  15841  trilpolemeq1  15843  trilpolemlt1  15844  dceqnconst  15863  dcapnconst  15864  nconstwlpolemgt0  15867