Theorem ltm1d 12063

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

Step	Hyp	Ref	Expression
1		ltp1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltm1 11972	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 − 1) < 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 − 1) < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5095  (class class class)co 7354  ℝcr 11014  1c1 11016   < clt 11155   − cmin 11353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676  ax-resscn 11072  ax-1cn 11073  ax-icn 11074  ax-addcl 11075  ax-addrcl 11076  ax-mulcl 11077  ax-mulrcl 11078  ax-mulcom 11079  ax-addass 11080  ax-mulass 11081  ax-distr 11082  ax-i2m1 11083  ax-1ne0 11084  ax-1rid 11085  ax-rnegex 11086  ax-rrecex 11087  ax-cnre 11088  ax-pre-lttri 11089  ax-pre-lttrn 11090  ax-pre-ltadd 11091  ax-pre-mulgt0 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-riota 7311  df-ov 7357  df-oprab 7358  df-mpo 7359  df-er 8630  df-en 8878  df-dom 8879  df-sdom 8880  df-pnf 11157  df-mnf 11158  df-xr 11159  df-ltxr 11160  df-le 11161  df-sub 11355  df-neg 11356

This theorem is referenced by:  suprzcl  12561  fzsuc2  13486  fzm1  13511  m1modnnsub1  13828  cshwidxm1  14718  fsumm1  15662  isumsplit  15751  climcndslem1  15760  bitsfzolem  16349  fldivp1  16813  4sqlem12  16872  ram0  16938  chnub  18532  chnccat  18536  sylow1lem1  19514  dgreq0  26201  atanlogsublem  26855  birthdaylem3  26893  wilthlem1  27008  ftalem5  27017  basellem5  27025  lgsval2lem  27248  lgsqrlem2  27288  gausslemma2dlem0c  27299  lgsquadlem1  27321  lgsquadlem2  27322  pntrsumbnd2  27508  axlowdimlem16  28939  pthdlem1  29748  clwwlkel  30030  clwwlknonex2lem2  30092  xlt2addrd  32748  cycpmco2lem6  33109  cvmliftlem6  35357  cvmliftlem8  35359  cvmliftlem9  35360  cvmliftlem10  35361  bcprod  35805  iooelexlt  37429  poimirlem1  37684  poimirlem2  37685  poimirlem6  37689  poimirlem7  37690  poimirlem8  37691  poimirlem12  37695  poimirlem15  37698  poimirlem16  37699  poimirlem17  37700  poimirlem19  37702  poimirlem20  37703  poimirlem21  37704  poimirlem22  37705  poimirlem23  37706  poimirlem26  37709  mettrifi  37820  aks4d1p1  42192  primrootlekpowne0  42221  sticksstones10  42271  sticksstones12a  42273  aks6d1c6lem3  42288  unitscyglem2  42312  irrapxlem1  42942  rmspecsqrtnq  43026  acongeq  43103  monoords  45425  fzisoeu  45428  fzdifsuc2  45438  infleinflem2  45496  unb2ltle  45540  limsupre3lem  45857  xlimxrre  45956  xlimmnfv  45959  iblspltprt  46098  itgspltprt  46104  stoweidlem11  46136  stoweidlem14  46139  fourierdlem11  46243  fourierdlem12  46244  fourierdlem15  46247  fourierdlem41  46273  fourierdlem48  46279  fourierdlem49  46280  fourierdlem50  46281  fourierdlem79  46310  ioorrnopnxrlem  46431  iundjiun  46585  chnsubseq  47005  m1modmmod  47485  lswn0  47571  bgoldbtbndlem4  47935  gpgedgvtx0  48188  logbpw2m1  48695