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

Theorem ltm1d 11564
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 11474 . 2 (𝐴 ∈ ℝ → (𝐴 − 1) < 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 − 1) < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107   class class class wbr 5057  (class class class)co 7148  cr 10528  1c1 10530   < clt 10667  cmin 10862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865
This theorem is referenced by:  suprzcl  12054  fzsuc2  12957  fzm1  12979  m1modnnsub1  13277  cshwidxm1  14161  fsumm1  15098  isumsplit  15187  climcndslem1  15196  bitsfzolem  15775  fldivp1  16225  4sqlem12  16284  ram0  16350  sylow1lem1  18715  dgreq0  24847  atanlogsublem  25485  birthdaylem3  25523  wilthlem1  25637  ftalem5  25646  basellem5  25654  lgsval2lem  25875  lgsqrlem2  25915  gausslemma2dlem0c  25926  lgsquadlem1  25948  lgsquadlem2  25949  pntrsumbnd2  26135  axlowdimlem16  26735  pthdlem1  27539  clwwlkel  27817  clwwlknonex2lem2  27879  xlt2addrd  30474  cycpmco2lem6  30766  cvmliftlem6  32525  cvmliftlem8  32527  cvmliftlem9  32528  cvmliftlem10  32529  bcprod  32958  iooelexlt  34630  poimirlem1  34880  poimirlem2  34881  poimirlem6  34885  poimirlem7  34886  poimirlem8  34887  poimirlem12  34891  poimirlem15  34894  poimirlem16  34895  poimirlem17  34896  poimirlem19  34898  poimirlem20  34899  poimirlem21  34900  poimirlem22  34901  poimirlem23  34902  poimirlem26  34905  mettrifi  35019  irrapxlem1  39404  rmspecsqrtnq  39488  acongeq  39565  monoords  41548  fzisoeu  41551  fzdifsuc2  41561  infleinflem2  41623  unb2ltle  41673  limsupre3lem  41997  xlimxrre  42096  xlimmnfv  42099  iblspltprt  42242  itgspltprt  42248  stoweidlem11  42281  stoweidlem14  42284  fourierdlem11  42388  fourierdlem12  42389  fourierdlem15  42392  fourierdlem41  42418  fourierdlem48  42424  fourierdlem49  42425  fourierdlem50  42426  fourierdlem79  42455  ioorrnopnxrlem  42576  iundjiun  42727  lswn0  43589  bgoldbtbndlem4  43958  m1modmmod  44566  logbpw2m1  44612
  Copyright terms: Public domain W3C validator