Theorem ltp1d 9016

Description: A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
ltp1d.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
ltp1d	⊢ (𝜑 → 𝐴 < (𝐴 + 1))

Proof of Theorem ltp1d

Step	Hyp	Ref	Expression
1		ltp1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltp1 8930	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐴 < (𝐴 + 1))

Syntax hints:   → wi 4   ∈ wcel 2177   class class class wbr 4048  (class class class)co 5954  ℝcr 7937  1c1 7939   + caddc 7941   < clt 8120

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4167  ax-pow 4223  ax-pr 4258  ax-un 4485  ax-setind 4590  ax-cnex 8029  ax-resscn 8030  ax-1cn 8031  ax-1re 8032  ax-icn 8033  ax-addcl 8034  ax-addrcl 8035  ax-mulcl 8036  ax-addcom 8038  ax-addass 8040  ax-i2m1 8043  ax-0lt1 8044  ax-0id 8046  ax-rnegex 8047  ax-pre-ltadd 8054

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-nel 2473  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-dif 3170  df-un 3172  df-in 3174  df-ss 3181  df-pw 3620  df-sn 3641  df-pr 3642  df-op 3644  df-uni 3854  df-br 4049  df-opab 4111  df-xp 4686  df-iota 5238  df-fv 5285  df-ov 5957  df-pnf 8122  df-mnf 8123  df-ltxr 8125

This theorem is referenced by:  zltp1le  9440  fznatpl1  10211  fzp1disj  10215  fzneuz  10236  fzp1nel  10239  fzonn0p1  10353  zssinfcl  10388  rebtwn2z  10410  seq3f1olemqsumk  10670  seqf1oglem1  10677  seqf1oglem2  10678  bernneq3  10820  bcp1nk  10920  bcpasc  10924  hashfzp1  10982  seq3coll  11000  resqrexlemover  11371  fsum1p  11779  cvgratnnlembern  11884  cvgratnnlemseq  11887  cvgratnnlemfm  11890  cvgratz  11893  mertenslemi1  11896  fprodntrivap  11945  fprod1p  11960  fprodeq0  11978  efcllemp  12019  nno  12267  sqrt2irr  12534  pcprendvds  12663  pcmpt  12716  1arith  12740  4sqlem11  12774  exmidunben  12847  nninfdclemp1  12871  suplociccreex  15146  perfectlem2  15522  gausslemma2dlem4  15591  gausslemma2dlem6  15594  lgsquadlem2  15605  cvgcmp2nlemabs  16086