Theorem 1zzd 8875

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

Syntax hints:   → wi 4   ∈ wcel 1445  1c1 7448  ℤcz 8848

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-setind 4381  ax-cnex 7533  ax-resscn 7534  ax-1cn 7535  ax-1re 7536  ax-icn 7537  ax-addcl 7538  ax-addrcl 7539  ax-mulcl 7540  ax-addcom 7542  ax-addass 7544  ax-distr 7546  ax-i2m1 7547  ax-0lt1 7548  ax-0id 7550  ax-rnegex 7551  ax-cnre 7553  ax-pre-ltirr 7554  ax-pre-ltwlin 7555  ax-pre-lttrn 7556  ax-pre-ltadd 7558

This theorem depends on definitions:  df-bi 116  df-3or 928  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-nel 2358  df-ral 2375  df-rex 2376  df-reu 2377  df-rab 2379  df-v 2635  df-sbc 2855  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-int 3711  df-br 3868  df-opab 3922  df-id 4144  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-iota 5014  df-fun 5051  df-fv 5057  df-riota 5646  df-ov 5693  df-oprab 5694  df-mpt2 5695  df-pnf 7621  df-mnf 7622  df-xr 7623  df-ltxr 7624  df-le 7625  df-sub 7752  df-neg 7753  df-inn 8521  df-z 8849

This theorem is referenced by:  uzm1  9148  elfz1b  9653  fzm1  9663  fzoss2  9732  fzo1fzo0n0  9743  qnegmod  9925  addmodid  9928  q2submod  9941  ser3mono  10028  seq3f1olemqsumkj  10048  exp3vallem  10071  exp3val  10072  exp1  10076  facnn  10250  fac0  10251  fac1  10252  bcp1nk  10285  hashfiv01gt1  10305  fseq1hash  10324  hashfz  10344  zfz1isolemsplit  10358  seq3coll  10362  resqrexlemf  10555  resqrexlemf1  10556  resqrexlemnmsq  10565  resqrexlemcvg  10567  climuni  10836  climrecvg1n  10891  climcvg1nlem  10892  isummolemnm  10922  summodclem2a  10924  summodclem2  10925  summodc  10926  zsumdc  10927  fsum3  10930  sum0  10931  fisumss  10935  fsumcl2lem  10941  fsumadd  10949  sumsnf  10952  fsummulc2  10991  telfsumo  11009  fsumparts  11013  binomlem  11026  divcnv  11040  arisum  11041  arisum2  11042  trireciplem  11043  trirecip  11044  expcnvap0  11045  expcnv  11047  geo2sum  11057  geo2lim  11059  geoisum1  11062  geoisum1c  11063  cvgratnnlemseq  11069  cvgratnnlemsumlt  11071  cvgratnnlemrate  11073  cvgratnn  11074  cvgratz  11075  mertenslemub  11077  mertenslemi1  11078  mertenslem2  11079  ege2le3  11110  nn0o1gt2  11332  gcdsupex  11376  gcdsupcl  11377  gcdaddm  11402  lcmval  11472  lcmcllem  11476  lcmledvds  11479  isprm3  11527  isprm4  11528  prmind2  11529  dvdsnprmd  11534  rpexp  11559  pw2dvds  11571  phivalfi  11615  phicl2  11617  hashdvds  11624  phiprmpw  11625  phimullem  11628  hashgcdeq  11631  lmtopcnp  12101