MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1zzd Structured version   Visualization version   GIF version

Theorem 1zzd 11600
Description: 1 is an integer, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
1zzd (𝜑 → 1 ∈ ℤ)

Proof of Theorem 1zzd
StepHypRef Expression
1 1z 11599 . 2 1 ∈ ℤ
21a1i 11 1 (𝜑 → 1 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  1c1 10129  cz 11569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-z 11570
This theorem is referenced by:  fzm1  12613  fzoss2  12690  fz1fzo0m1  12710  fzo1fzo0n0  12713  elfznelfzo  12767  negmod  12909  addmodid  12912  modnegd  12919  2submod  12925  sermono  13027  seqf1olem2  13035  bcp1nk  13298  eqwrds3  13905  climuni  14482  isercoll  14597  telfsumo  14733  fsumparts  14737  binomlem  14760  climcndslem2  14781  climcnds  14782  divcnv  14784  supcvg  14787  arisum  14791  trireciplem  14793  trirecip  14794  expcnv  14795  geo2sum  14803  geo2lim  14805  geoisum1  14809  geoisum1c  14810  mertenslem1  14815  mertenslem2  14816  fprodser  14878  fprodzcl  14883  risefacval2  14940  fallfacval2  14941  binomfallfaclem2  14970  bpolydiflem  14984  ege2le3  15019  rpnnen2lem12  15153  nn0o1gt2  15299  pwp1fsum  15316  bitscmp  15362  dvdsnprmd  15605  hashdvds  15682  phiprmpw  15683  prmdiv  15692  odzdvds  15702  odzphi  15703  modprm1div  15704  iserodd  15742  pcid  15779  pcmptcl  15797  pockthlem  15811  prmreclem4  15825  prmreclem6  15827  vdwapun  15880  prmdvdsprmo  15948  prmodvdslcmf  15953  prmgapprmo  15968  gsumpr12val  17483  mulgpropd  17785  sylow1lem1  18213  sylow3lem6  18247  pgpfac1lem2  18674  zringcyg  20041  mulgrhm2  20049  znunit  20114  znrrg  20116  frgpcyg  20124  cpmadugsumlemF  20883  lmcnp  21310  lmmo  21386  1stcelcls  21466  1stccnp  21467  1stckgenlem  21558  1stckgen  21559  clmvneg1  23099  clmmulg  23101  lmnn  23261  cmetcaulem  23286  iscmet2  23292  causs  23296  nglmle  23300  caubl  23306  iscmet3i  23310  ovolsf  23441  ovoliunlem1  23470  ovoliun  23473  ovoliun2  23474  ovolicc2lem2  23486  ovolicc2lem3  23487  ovolicc2lem4  23488  voliunlem2  23519  voliunlem3  23520  ioombl1lem4  23529  uniioombllem2  23551  uniioombllem3  23553  uniioombllem6  23556  vitalilem4  23579  itg1climres  23680  mbfi1fseqlem6  23686  mbfi1flimlem  23688  mbfmullem2  23690  itg2monolem1  23716  itg2i1fseq  23721  itg2i1fseq2  23722  itg2addlem  23724  plyeq0lem  24165  dvply1  24238  dvtaylp  24323  pserdvlem2  24381  pserdv2  24383  advlogexp  24600  logtayl  24605  logtaylsum  24606  logtayl2  24607  atantayl  24863  leibpilem2  24867  leibpi  24868  birthdaylem2  24878  dfef2  24896  divsqrtsumlem  24905  emcllem4  24924  emcllem6  24926  emcllem7  24927  zetacvg  24940  lgamgulmlem4  24957  lgamgulmlem6  24959  lgamgulm2  24961  lgamcvglem  24965  lgamcvg2  24980  gamcvg  24981  regamcl  24986  relgamcl  24987  wilthlem1  24993  wilthlem2  24994  basellem6  25011  basellem7  25012  basellem8  25013  basellem9  25014  mersenne  25151  perfectlem1  25153  perfectlem2  25154  lgslem1  25221  lgsqrlem1  25270  gausslemma2dlem4  25293  gausslemma2dlem6  25296  gausslemma2dlem7  25297  lgseisenlem1  25299  lgsquad2lem1  25308  lgsquad3  25311  m1lgs  25312  2sqlem11  25353  dchrisumlema  25376  dchrisumlem3  25379  dchrmusum2  25382  dchrvmasumiflem1  25389  dchrvmaeq0  25392  dchrisum0re  25401  dchrisum0lem1b  25403  dchrisum0lem2a  25405  logdivsum  25421  pntrlog2bndlem1  25465  pntpbnd2  25475  axlowdimlem6  26026  axlowdim  26040  upgrewlkle2  26712  redwlk  26779  pthdadjvtx  26836  pthdlem1  26872  wwlksnextproplem2  27028  clwlksfclwwlkOLD  27216  minvecolem3  28041  minvecolem4b  28043  minvecolem4  28045  h2hcau  28145  h2hlm  28146  hlimadd  28359  hhsscms  28445  occllem  28471  nlelchi  29229  opsqrlem4  29311  hmopidmchi  29319  fzspl  29859  fzsplit3  29862  archirngz  30052  archiabllem1a  30054  smatrcl  30171  submateqlem1  30182  submateqlem2  30183  mdetlap  30207  rge0scvg  30304  lmxrge0  30307  lmdvg  30308  qqhval2lem  30334  esumfsupre  30442  esumpcvgval  30449  esumcvg  30457  eulerpartlems  30731  fiblem  30769  ballotlemfp1  30862  ballotlemimin  30876  ballotlemic  30877  ballotlem1c  30878  ballotlemsdom  30882  ballotlemsel1i  30883  ballotlemsima  30886  ballotlemfrceq  30899  ballotlemfrcn0  30900  chtvalz  31016  sinccvg  31874  circum  31875  divcnvlin  31925  bcprod  31931  iprodgam  31935  faclimlem2  31937  faclim  31939  iprodfac  31940  faclim2  31941  fwddifnp1  32578  lmclim2  33867  geomcau  33868  heibor1lem  33921  heibor1  33922  bfplem1  33934  bfplem2  33935  rrncmslem  33944  rrncms  33945  fzsplit1nn0  37819  eldioph2lem1  37825  pellexlem6  37900  rmspecnonsq  37974  jm2.22  38064  jm2.23  38065  jm2.25  38068  dvradcnv2  39048  binomcxplemnn0  39050  binomcxplemrat  39051  binomcxplemnotnn0  39057  oddfl  39988  uzubioo  40297  fmuldfeq  40318  fmul01lt1lem2  40320  fmul01lt1  40321  clim1fr1  40336  sumnnodd  40365  limsup10exlem  40507  fprodsubrecnncnvlem  40624  fprodaddrecnncnvlem  40626  dvnmul  40661  stoweidlem3  40723  stoweidlem7  40727  stoweidlem11  40731  stoweidlem14  40734  stoweidlem20  40740  stoweidlem26  40746  stoweidlem34  40754  stoweidlem51  40771  wallispilem5  40789  wallispi  40790  stirlinglem1  40794  stirlinglem5  40798  stirlinglem7  40800  stirlinglem8  40801  stirlinglem10  40803  stirlinglem12  40805  stirlinglem13  40806  stirlinglem14  40807  stirlinglem15  40808  stirlingr  40810  fourierdlem4  40831  fourierdlem11  40838  fourierdlem26  40853  fourierdlem41  40868  fourierdlem42  40869  fourierdlem48  40874  fourierdlem49  40875  fourierdlem79  40905  fourierdlem97  40923  fourierdlem103  40929  fourierdlem104  40930  fourierdlem112  40938  sqwvfoura  40948  sqwvfourb  40949  fouriersw  40951  etransclem15  40969  etransclem28  40982  etransclem35  40989  etransclem38  40992  etransclem44  40998  etransclem48  41002  sge0ad2en  41151  voliunsge0lem  41192  caragenunicl  41244  caratheodorylem2  41247  ovolval2lem  41363  ovolval2  41364  vonioolem2  41401  vonicclem2  41404  iccpartiltu  41868  iccpartgt  41873  fmtnoge3  41952  fmtnoprmfac1lem  41986  pwdif  42011  2pwp1prm  42013  sfprmdvdsmersenne  42030  lighneallem2  42033  perfectALTVlem2  42141  nnsum3primesprm  42188  bgoldbtbndlem3  42205  2even  42443  fldivexpfllog2  42869  nnlog2ge0lt1  42870  logbpw2m1  42871  blenpw2m1  42883  blennnt2  42893  nnolog2flm1  42894  blennn0e2  42898  digexp  42911  dignn0flhalflem1  42919  dignn0flhalflem2  42920
  Copyright terms: Public domain W3C validator