| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > ltp1d | Unicode version | ||
| Description: A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.) |
| Ref | Expression |
|---|---|
| ltp1d.1 |
|
| Ref | Expression |
|---|---|
| ltp1d |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ltp1d.1 |
. 2
| |
| 2 | ltp1 8916 |
. 2
| |
| 3 | 1, 2 | syl 14 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| 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 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-sep 4161 ax-pow 4217 ax-pr 4252 ax-un 4479 ax-setind 4584 ax-cnex 8015 ax-resscn 8016 ax-1cn 8017 ax-1re 8018 ax-icn 8019 ax-addcl 8020 ax-addrcl 8021 ax-mulcl 8022 ax-addcom 8024 ax-addass 8026 ax-i2m1 8029 ax-0lt1 8030 ax-0id 8032 ax-rnegex 8033 ax-pre-ltadd 8040 |
| This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1375 df-fal 1378 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ne 2376 df-nel 2471 df-ral 2488 df-rex 2489 df-rab 2492 df-v 2773 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-br 4044 df-opab 4105 df-xp 4680 df-iota 5231 df-fv 5278 df-ov 5946 df-pnf 8108 df-mnf 8109 df-ltxr 8111 |
| This theorem is referenced by: zltp1le 9426 fznatpl1 10197 fzp1disj 10201 fzneuz 10222 fzp1nel 10225 fzonn0p1 10338 zssinfcl 10373 rebtwn2z 10395 seq3f1olemqsumk 10655 seqf1oglem1 10662 seqf1oglem2 10663 bernneq3 10805 bcp1nk 10905 bcpasc 10909 hashfzp1 10967 seq3coll 10985 resqrexlemover 11292 fsum1p 11700 cvgratnnlembern 11805 cvgratnnlemseq 11808 cvgratnnlemfm 11811 cvgratz 11814 mertenslemi1 11817 fprodntrivap 11866 fprod1p 11881 fprodeq0 11899 efcllemp 11940 nno 12188 sqrt2irr 12455 pcprendvds 12584 pcmpt 12637 1arith 12661 4sqlem11 12695 exmidunben 12768 nninfdclemp1 12792 suplociccreex 15067 perfectlem2 15443 gausslemma2dlem4 15512 gausslemma2dlem6 15515 lgsquadlem2 15526 cvgcmp2nlemabs 15933 |
| Copyright terms: Public domain | W3C validator |