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

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

Proof of Theorem 1zzd
StepHypRef Expression
1 1z 12540 . 2 1 ∈ ℤ
21a1i 11 1 (𝜑 → 1 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  1c1 11059  cz 12506
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-i2m1 11126  ax-1ne0 11127  ax-rrecex 11130  ax-cnre 11131
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-neg 11395  df-nn 12161  df-z 12507
This theorem is referenced by:  fzm1  13528  fzoss2  13607  fzo1fzo0n0  13630  elfznelfzo  13684  negmod  13828  addmodid  13831  modnegd  13838  2submod  13844  sermono  13947  seqf1olem2  13955  bcp1nk  14224  eqwrds3  14857  climuni  15441  isercoll  15559  telfsumo  15694  fsumparts  15698  binomlem  15721  climcndslem2  15742  climcnds  15743  divcnv  15745  supcvg  15748  arisum  15752  trireciplem  15754  trirecip  15755  expcnv  15756  pwdif  15760  geo2sum  15765  geo2lim  15767  geoisum1  15771  geoisum1c  15772  mertenslem1  15776  mertenslem2  15777  fprodser  15839  fprodzcl  15844  risefacval2  15900  fallfacval2  15901  binomfallfaclem2  15930  bpolydiflem  15944  ege2le3  15979  rpnnen2lem12  16114  modm1div  16155  nn0o1gt2  16270  pwp1fsum  16280  bitscmp  16325  dvdsnprmd  16573  2mulprm  16576  hashdvds  16654  phiprmpw  16655  prmdiv  16664  odzdvds  16674  odzphi  16675  iserodd  16714  pcid  16752  pcmptcl  16770  pockthlem  16784  prmreclem4  16798  prmreclem6  16800  vdwapun  16853  prmdvdsprmo  16921  prmodvdslcmf  16926  prmgapprmo  16941  gsumpr12val  18551  mulgpropd  18925  cycsubggend  19005  odm1inv  19342  sylow1lem1  19387  sylow3lem6  19421  pgpfac1lem2  19861  ablsimpgfindlem1  19893  zringcyg  20906  mulgrhm2  20915  znunit  20986  znrrg  20988  frgpcyg  20996  cpmadugsumlemF  22241  lmcnp  22671  lmmo  22747  1stcelcls  22828  1stccnp  22829  1stckgenlem  22920  1stckgen  22921  clmvneg1  24478  clmmulg  24480  lmnn  24643  cmetcaulem  24668  iscmet2  24674  causs  24678  nglmle  24682  caubl  24688  iscmet3i  24692  ovolsf  24852  ovoliunlem1  24882  ovoliun  24885  ovoliun2  24886  ovolicc2lem2  24898  ovolicc2lem3  24899  ovolicc2lem4  24900  voliunlem2  24931  voliunlem3  24932  ioombl1lem4  24941  uniioombllem2  24963  uniioombllem3  24965  uniioombllem6  24968  vitalilem4  24991  itg1climres  25095  mbfi1fseqlem6  25101  mbfi1flimlem  25103  mbfmullem2  25105  itg2monolem1  25131  itg2i1fseq  25136  itg2i1fseq2  25137  itg2addlem  25139  plyeq0lem  25587  dvply1  25660  dvtaylp  25745  pserdvlem2  25803  pserdv2  25805  advlogexp  26026  logtayl  26031  logtaylsum  26032  logtayl2  26033  atantayl  26303  leibpilem2  26307  leibpi  26308  birthdaylem2  26318  dfef2  26336  divsqrtsumlem  26345  emcllem4  26364  emcllem6  26366  emcllem7  26367  zetacvg  26380  lgamgulmlem4  26397  lgamgulmlem6  26399  lgamgulm2  26401  lgamcvglem  26405  lgamcvg2  26420  gamcvg  26421  regamcl  26426  relgamcl  26427  wilthlem1  26433  wilthlem2  26434  basellem6  26451  basellem7  26452  basellem8  26453  basellem9  26454  mersenne  26591  perfectlem1  26593  perfectlem2  26594  lgslem1  26661  lgsqrlem1  26710  gausslemma2dlem4  26733  gausslemma2dlem6  26736  gausslemma2dlem7  26737  lgseisenlem1  26739  lgsquad2lem1  26748  lgsquad3  26751  m1lgs  26752  2sqlem11  26793  dchrisumlema  26852  dchrisumlem3  26855  dchrmusum2  26858  dchrvmasumiflem1  26865  dchrvmaeq0  26868  dchrisum0re  26877  dchrisum0lem1b  26879  dchrisum0lem2a  26881  logdivsum  26897  pntrlog2bndlem1  26941  pntpbnd2  26951  axlowdimlem6  27938  axlowdim  27952  upgrewlkle2  28596  redwlk  28662  pthdadjvtx  28720  pthdlem1  28756  wwlksnextproplem2  28897  clwwlkccatlem  28975  minvecolem3  29860  minvecolem4b  29862  minvecolem4  29864  h2hcau  29963  h2hlm  29964  hlimadd  30177  hhsscms  30262  occllem  30287  nlelchi  31045  opsqrlem4  31127  hmopidmchi  31135  fzm1ne1  31734  fzspl  31735  fzsplit3  31739  prmdvdsbc  31754  pfxlsw2ccat  31848  tocycfvres1  32001  tocycfvres2  32002  cycpmfvlem  32003  cycpmfv1  32004  cycpmfv2  32005  cycpmfv3  32006  cycpmcl  32007  tocyc01  32009  cycpmco2lem6  32022  cycpmco2lem7  32023  cycpmconjv  32033  cycpmrn  32034  cycpmconjslem1  32045  cycpmconjslem2  32046  archirngz  32067  archiabllem1a  32069  smatrcl  32417  submateqlem1  32428  submateqlem2  32429  mdetlap  32453  rge0scvg  32570  lmxrge0  32573  lmdvg  32574  qqhval2lem  32602  esumfsupre  32710  esumpcvgval  32717  esumcvg  32725  eulerpartlems  33000  fiblem  33038  ballotlemfp1  33131  ballotlemimin  33145  ballotlemic  33146  ballotlem1c  33147  ballotlemsdom  33151  ballotlemsel1i  33152  ballotlemsima  33155  ballotlemfrceq  33168  ballotlemfrcn0  33169  chtvalz  33282  sinccvg  34301  circum  34302  divcnvlin  34344  bcprod  34350  iprodgam  34354  faclimlem2  34356  faclim  34358  iprodfac  34359  faclim2  34360  fwddifnp1  34779  lmclim2  36246  geomcau  36247  heibor1lem  36297  heibor1  36298  bfplem1  36310  bfplem2  36311  rrncmslem  36320  rrncms  36321  fzsplitnd  40469  lcmineqlem4  40518  lcmineqlem13  40527  lcmineqlem23  40537  dvrelogpow2b  40554  aks4d1p1p7  40560  aks4d1p1  40562  aks4d1p3  40564  aks4d1p5  40566  aks4d1p7  40569  aks4d1p8d2  40571  aks4d1p8  40573  aks4d1p9  40574  sticksstones6  40588  sticksstones7  40589  sticksstones9  40591  sticksstones10  40592  sticksstones11  40593  sticksstones12a  40594  sticksstones12  40595  metakunt1  40606  metakunt2  40607  metakunt3  40608  metakunt5  40610  metakunt7  40612  metakunt10  40615  metakunt15  40620  metakunt16  40621  metakunt19  40624  metakunt21  40626  metakunt22  40627  metakunt24  40629  metakunt25  40630  metakunt26  40631  metakunt28  40633  metakunt29  40634  metakunt30  40635  metakunt32  40637  metakunt33  40638  fzsplit1nn0  41106  eldioph2lem1  41112  pellexlem6  41186  rmspecnonsq  41259  jm2.22  41348  jm2.23  41349  jm2.25  41352  dvradcnv2  42701  binomcxplemnn0  42703  binomcxplemrat  42704  binomcxplemnotnn0  42710  oddfl  43585  uzubioo  43879  fmuldfeq  43898  fmul01lt1lem2  43900  fmul01lt1  43901  clim1fr1  43916  sumnnodd  43945  limsup10exlem  44087  fprodsubrecnncnvlem  44222  fprodaddrecnncnvlem  44224  dvnmul  44258  stoweidlem3  44318  stoweidlem7  44322  stoweidlem11  44326  stoweidlem14  44329  stoweidlem20  44335  stoweidlem26  44341  stoweidlem34  44349  stoweidlem51  44366  wallispilem5  44384  wallispi  44385  stirlinglem1  44389  stirlinglem5  44393  stirlinglem7  44395  stirlinglem8  44396  stirlinglem10  44398  stirlinglem12  44400  stirlinglem13  44401  stirlinglem14  44402  stirlinglem15  44403  stirlingr  44405  fourierdlem4  44426  fourierdlem11  44433  fourierdlem26  44448  fourierdlem41  44463  fourierdlem42  44464  fourierdlem48  44469  fourierdlem49  44470  fourierdlem79  44500  fourierdlem97  44518  fourierdlem103  44524  fourierdlem104  44525  fourierdlem112  44533  sqwvfoura  44543  sqwvfourb  44544  fouriersw  44546  etransclem15  44564  etransclem28  44577  etransclem35  44584  etransclem38  44587  etransclem44  44593  etransclem48  44597  sge0ad2en  44746  voliunsge0lem  44787  caragenunicl  44839  caratheodorylem2  44842  ovolval2lem  44958  ovolval2  44959  vonioolem2  44996  vonicclem2  44999  upwordnul  45193  iccpartiltu  45688  iccpartgt  45693  fmtnoge3  45796  fmtnoprmfac1lem  45830  2pwp1prm  45855  sfprmdvdsmersenne  45869  lighneallem2  45872  perfectALTVlem2  45988  fpprwpprb  46006  nnsum3primesprm  46056  bgoldbtbndlem3  46073  2even  46305  fldivexpfllog2  46725  nnlog2ge0lt1  46726  logbpw2m1  46727  blenpw2m1  46739  blennnt2  46749  nnolog2flm1  46750  blennn0e2  46754  digexp  46767  dignn0flhalflem1  46775  dignn0flhalflem2  46776
  Copyright terms: Public domain W3C validator