Theorem ltm1d 12086

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 11995	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 − 1) < 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 − 1) < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5079  (class class class)co 7363  ℝcr 11035  1c1 11037   < clt 11177   − cmin 11375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378

This theorem is referenced by:  suprzcl  12607  fzsuc2  13534  fzm1  13559  m1modnnsub1  13877  cshwidxm1  14767  fsumm1  15711  isumsplit  15803  climcndslem1  15812  bitsfzolem  16401  fldivp1  16866  4sqlem12  16925  ram0  16991  chnub  18586  chnccat  18590  sylow1lem1  19571  dgreq0  26255  atanlogsublem  26904  birthdaylem3  26942  wilthlem1  27056  ftalem5  27065  basellem5  27073  lgsval2lem  27295  lgsqrlem2  27335  gausslemma2dlem0c  27346  lgsquadlem1  27368  lgsquadlem2  27369  pntrsumbnd2  27555  axlowdimlem16  29051  pthdlem1  29859  clwwlkel  30141  clwwlknonex2lem2  30203  xlt2addrd  32858  cycpmco2lem6  33219  cvmliftlem6  35525  cvmliftlem8  35527  cvmliftlem9  35528  cvmliftlem10  35529  bcprod  35973  iooelexlt  37731  poimirlem1  37995  poimirlem2  37996  poimirlem6  38000  poimirlem7  38001  poimirlem8  38002  poimirlem12  38006  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem21  38015  poimirlem22  38016  poimirlem23  38017  poimirlem26  38020  mettrifi  38131  aks4d1p1  42568  primrootlekpowne0  42597  sticksstones10  42647  sticksstones12a  42649  aks6d1c6lem3  42664  unitscyglem2  42688  irrapxlem1  43274  rmspecsqrtnq  43358  acongeq  43435  monoords  45752  fzisoeu  45755  fzdifsuc2  45765  infleinflem2  45822  unb2ltle  45865  limsupre3lem  46182  xlimxrre  46281  xlimmnfv  46284  iblspltprt  46423  itgspltprt  46429  stoweidlem11  46461  stoweidlem14  46464  fourierdlem11  46568  fourierdlem12  46569  fourierdlem15  46572  fourierdlem41  46598  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem79  46635  ioorrnopnxrlem  46756  iundjiun  46910  chnsubseq  47332  m1modmmod  47834  lswn0  47926  bgoldbtbndlem4  48306  gpgedgvtx0  48559  logbpw2m1  49065