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

Theorem ltm1d 11788
Description: A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
ltp1d.1 (𝜑𝐴 ∈ ℝ)
Assertion
Ref Expression
ltm1d (𝜑 → (𝐴 − 1) < 𝐴)

Proof of Theorem ltm1d
StepHypRef Expression
1 ltp1d.1 . 2 (𝜑𝐴 ∈ ℝ)
2 ltm1 11698 . 2 (𝐴 ∈ ℝ → (𝐴 − 1) < 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 − 1) < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111   class class class wbr 5067  (class class class)co 7231  cr 10752  1c1 10754   < clt 10891  cmin 11086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-resscn 10810  ax-1cn 10811  ax-icn 10812  ax-addcl 10813  ax-addrcl 10814  ax-mulcl 10815  ax-mulrcl 10816  ax-mulcom 10817  ax-addass 10818  ax-mulass 10819  ax-distr 10820  ax-i2m1 10821  ax-1ne0 10822  ax-1rid 10823  ax-rnegex 10824  ax-rrecex 10825  ax-cnre 10826  ax-pre-lttri 10827  ax-pre-lttrn 10828  ax-pre-ltadd 10829  ax-pre-mulgt0 10830
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-br 5068  df-opab 5130  df-mpt 5150  df-id 5469  df-po 5482  df-so 5483  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-riota 7188  df-ov 7234  df-oprab 7235  df-mpo 7236  df-er 8411  df-en 8647  df-dom 8648  df-sdom 8649  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896  df-le 10897  df-sub 11088  df-neg 11089
This theorem is referenced by:  suprzcl  12281  fzsuc2  13194  fzm1  13216  m1modnnsub1  13514  cshwidxm1  14396  fsumm1  15339  isumsplit  15428  climcndslem1  15437  bitsfzolem  16017  fldivp1  16474  4sqlem12  16533  ram0  16599  sylow1lem1  19011  dgreq0  25183  atanlogsublem  25822  birthdaylem3  25860  wilthlem1  25974  ftalem5  25983  basellem5  25991  lgsval2lem  26212  lgsqrlem2  26252  gausslemma2dlem0c  26263  lgsquadlem1  26285  lgsquadlem2  26286  pntrsumbnd2  26472  axlowdimlem16  27072  pthdlem1  27877  clwwlkel  28153  clwwlknonex2lem2  28215  xlt2addrd  30825  cycpmco2lem6  31141  cvmliftlem6  32988  cvmliftlem8  32990  cvmliftlem9  32991  cvmliftlem10  32992  bcprod  33446  iooelexlt  35296  poimirlem1  35541  poimirlem2  35542  poimirlem6  35546  poimirlem7  35547  poimirlem8  35548  poimirlem12  35552  poimirlem15  35555  poimirlem16  35556  poimirlem17  35557  poimirlem19  35559  poimirlem20  35560  poimirlem21  35561  poimirlem22  35562  poimirlem23  35563  poimirlem26  35566  mettrifi  35678  aks4d1p1  39843  sticksstones10  39862  sticksstones12a  39864  metakunt18  39893  metakunt20  39895  metakunt24  39899  irrapxlem1  40375  rmspecsqrtnq  40459  acongeq  40536  monoords  42537  fzisoeu  42540  fzdifsuc2  42550  infleinflem2  42611  unb2ltle  42656  limsupre3lem  42976  xlimxrre  43075  xlimmnfv  43078  iblspltprt  43217  itgspltprt  43223  stoweidlem11  43255  stoweidlem14  43258  fourierdlem11  43362  fourierdlem12  43363  fourierdlem15  43366  fourierdlem41  43392  fourierdlem48  43398  fourierdlem49  43399  fourierdlem50  43400  fourierdlem79  43429  ioorrnopnxrlem  43550  iundjiun  43701  lswn0  44597  bgoldbtbndlem4  44961  m1modmmod  45568  logbpw2m1  45614
  Copyright terms: Public domain W3C validator