Theorem 1zzd 9675

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  1c1 8180  ℤcz 9648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-cnex 8270  ax-resscn 8271  ax-1cn 8272  ax-1re 8273  ax-icn 8274  ax-addcl 8275  ax-addrcl 8276  ax-mulcl 8277  ax-addcom 8279  ax-addass 8281  ax-distr 8283  ax-i2m1 8284  ax-0lt1 8285  ax-0id 8287  ax-rnegex 8288  ax-cnre 8290  ax-pre-ltirr 8291  ax-pre-ltwlin 8292  ax-pre-lttrn 8293  ax-pre-ltadd 8295

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4131  df-opab 4193  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-iota 5337  df-fun 5379  df-fv 5385  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-pnf 8362  df-mnf 8363  df-xr 8364  df-ltxr 8365  df-le 8366  df-sub 8500  df-neg 8501  df-inn 9307  df-z 9649

This theorem is used by:  uzm1  9962  fzsplit3  10468  fzspl  10486  elfz1b  10507  fzm1  10517  fzoss2  10591  fzo1fzo0n0  10605  nninfdcex  10682  qnegmod  10819  addmodid  10822  q2submod  10835  ser3mono  10937  seq3f1olemqsumkj  10961  seqf1oglem2  10970  exp3vallem  10990  exp3val  10991  exp1  10995  facnn  11179  fac0  11180  fac1  11181  bcp1nk  11214  hashfiv01gt1  11235  fseq1hash  11255  hashfz  11276  sseqn  11293  zfz1isolemsplit  11304  seq3coll  11308  wrdind  11508  wrd2ind  11509  resqrexlemf  11787  resqrexlemf1  11788  resqrexlemnmsq  11797  resqrexlemcvg  11799  climuni  12075  climrecvg1n  12130  climcvg1nlem  12131  nnf1o  12159  summodclem2a  12164  summodclem2  12165  summodc  12166  zsumdc  12167  fsum3  12170  sum0  12171  fisumss  12175  fsumcl2lem  12181  fsumadd  12189  sumsnf  12192  fsummulc2  12231  telfsumo  12249  fsumparts  12253  binomlem  12266  divcnv  12280  arisum  12281  arisum2  12282  trireciplem  12283  trirecip  12284  expcnvap0  12285  expcnv  12287  geo2sum  12297  geo2lim  12299  geoisum1  12302  geoisum1c  12303  cvgratnnlemseq  12309  cvgratnnlemsumlt  12311  cvgratnnlemrate  12313  cvgratnn  12314  cvgratz  12315  mertenslemub  12317  mertenslemi1  12318  mertenslem2  12319  prodmodclem3  12358  prodmodclem2a  12359  prodmodclem2  12360  zproddc  12362  fprodseq  12366  fprodssdc  12373  prodsnf  12375  fprodzcl  12392  fprodfac  12398  ege2le3  12454  modm1div  12583  nn0o1gt2  12688  bitsfzolem  12737  bitscmp  12741  gcdsupex  12750  gcdsupcl  12751  gcdaddm  12777  nnmindc  12827  nnminle  12828  uzwodc  12830  lcmval  12857  lcmcllem  12861  lcmledvds  12864  isprm3  12912  isprm4  12913  prmind2  12914  dvdsnprmd  12919  rpexp  12948  pwbdvds  12961  phivalfi  13010  phicl2  13012  hashdvds  13019  phiprmpw  13020  phimullem  13023  eulerthlemfi  13026  eulerthlemh  13029  eulerthlemth  13030  eulerth  13031  prmdiv  13033  dvdsfi  13037  hashgcdeq  13038  odzcllem  13041  odzdvds  13044  odzphi  13045  pcid  13123  pcmptcl  13141  pcmpt  13142  pcfac  13149  pcbc  13150  pockthlem  13155  infpnlem2  13159  1arith  13166  4sqlem11  13200  4sqlem13m  13202  4sqlem14  13203  4sqlem17  13206  4sqlem18  13207  ballotfilemcinfi  13273  ballotfilemdifcfi  13274  ballotfilemfp1  13280  ballotfilemafi  13287  ballotfilembfi  13288  ballotfilemiex  13293  ballotfilemimin  13298  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemsdom  13304  ballotfilemsel1i  13305  ballotfilemsima  13308  ballotfilemfg  13318  ballotfilemfrceq  13321  ballotfilemfrcn0  13322  ballotfilemth  13330  nninfdclemf  13389  mulgval  13974  mulgfng  13976  mulgnngzsum  13979  mulg1  13981  mulgnnsubcl  13986  mulgpropdg  14016  gzsumshift  14198  gsumvalfi  14201  gzsumgsum1  14202  gzsumgsum  14204  gsumsncmn  14205  gsump1  14206  gsumf1ofi  14209  gsummhmfi  14213  gsumressfi  14216  mulgrhm  14993  mulgrhm2  14994  znunit  15043  znrrg  15044  lmtopcnp  15400  dvply1  15915  logfac  16048  relogbval  16106  relogbzcl  16107  nnlogbexp  16114  birthdaylem1g  16144  birthdaylem2  16145  birthdaylem3  16146  wilthlem1  16151  prmdvdsfi  16159  ppiqub  16194  mersenne  16195  perfectlem1  16197  perfectlem2  16198  bposlem1  16209  bposlem2  16210  bposlem5  16213  lgslem1  16217  lgsval  16221  lgsfvalg  16222  lgscllem  16224  lgsval2lem  16227  lgsval4a  16239  lgsneg  16241  lgsdir2  16250  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  gausslemma2dlem1  16278  gausslemma2dlem4  16281  gausslemma2dlem6  16284  gausslemma2dlem7  16285  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgseisen  16291  lgsquadlemsfi  16292  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad2lem1  16298  lgsquad3  16301  m1lgs  16302  2lgsoddprm  16330  clwwlkccatlem  16739  clwwlknonex2lem2  16777  konigsberglem1  16827  cvgcmp2nlemabs  17179  cvgcmp2n  17180  trilpolemcl  17184  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  dceqnconst  17208  dcapnconst  17209  nconstwlpolemgt0  17212