![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nnre | Unicode version |
Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
Ref | Expression |
---|---|
nnre |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnssre 8937 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | sseli 3163 |
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-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 ax-sep 4133 ax-cnex 7916 ax-resscn 7917 ax-1re 7919 ax-addrcl 7922 |
This theorem depends on definitions: df-bi 117 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ral 2470 df-v 2751 df-in 3147 df-ss 3154 df-int 3857 df-inn 8934 |
This theorem is referenced by: nnrei 8942 peano2nn 8945 nn1suc 8952 nnge1 8956 nnle1eq1 8957 nngt0 8958 nnnlt1 8959 nnap0 8962 nn2ge 8966 nn1gt1 8967 nndivre 8969 nnrecgt0 8971 nnsub 8972 arch 9187 nnrecl 9188 bndndx 9189 nn0ge0 9215 0mnnnnn0 9222 nnnegz 9270 elnnz 9277 elz2 9338 gtndiv 9362 prime 9366 btwnz 9386 qre 9639 elpq 9662 elpqb 9663 nnrp 9677 nnledivrp 9780 fzo1fzo0n0 10197 elfzo0le 10199 fzonmapblen 10201 ubmelfzo 10214 fzonn0p1p1 10227 elfzom1p1elfzo 10228 ubmelm1fzo 10240 subfzo0 10256 adddivflid 10306 flltdivnn0lt 10318 intfracq 10334 flqdiv 10335 m1modnnsub1 10384 addmodid 10386 modfzo0difsn 10409 nnlesq 10638 facndiv 10733 faclbnd 10735 faclbnd3 10737 bcval5 10757 seq3coll 10836 caucvgre 11004 efaddlem 11696 nndivdvds 11817 nno 11925 nnoddm1d2 11929 divalglemnn 11937 divalg2 11945 ndvdsadd 11950 gcdmultiple 12035 gcdmultiplez 12036 gcdzeq 12037 sqgcd 12044 dvdssqlem 12045 lcmgcdlem 12091 coprmgcdb 12102 qredeq 12110 qredeu 12111 prmdvdsfz 12153 sqrt2irr 12176 divdenle 12211 phibndlem 12230 hashgcdlem 12252 oddprm 12273 pythagtriplem10 12283 pythagtriplem12 12289 pythagtriplem14 12291 pythagtriplem16 12293 pythagtriplem19 12296 pclemub 12301 pc2dvds 12343 pcmpt 12355 fldivp1 12360 pcbc 12363 infpnlem1 12371 oddennn 12407 exmidunben 12441 mulgnegnn 13025 lgsval4a 14719 |
Copyright terms: Public domain | W3C validator |