![]() |
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 8582 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | sseli 3043 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-sep 3986 ax-cnex 7586 ax-resscn 7587 ax-1re 7589 ax-addrcl 7592 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ral 2380 df-v 2643 df-in 3027 df-ss 3034 df-int 3719 df-inn 8579 |
This theorem is referenced by: nnrei 8587 peano2nn 8590 nn1suc 8597 nnge1 8601 nnle1eq1 8602 nngt0 8603 nnnlt1 8604 nnap0 8607 nn2ge 8611 nn1gt1 8612 nndivre 8614 nnrecgt0 8616 nnsub 8617 arch 8826 nnrecl 8827 bndndx 8828 nn0ge0 8854 0mnnnnn0 8861 nnnegz 8909 elnnz 8916 elz2 8974 gtndiv 8998 prime 9002 btwnz 9022 qre 9267 nnrp 9300 nnledivrp 9394 fzo1fzo0n0 9801 elfzo0le 9803 fzonmapblen 9805 ubmelfzo 9818 fzonn0p1p1 9831 elfzom1p1elfzo 9832 ubmelm1fzo 9844 subfzo0 9860 adddivflid 9906 flltdivnn0lt 9918 intfracq 9934 flqdiv 9935 m1modnnsub1 9984 addmodid 9986 modfzo0difsn 10009 nnlesq 10237 facndiv 10326 faclbnd 10328 faclbnd3 10330 bcval5 10350 seq3coll 10426 caucvgre 10593 efaddlem 11178 nndivdvds 11294 nno 11398 nnoddm1d2 11402 divalglemnn 11410 divalg2 11418 ndvdsadd 11423 gcdmultiple 11501 gcdmultiplez 11502 gcdzeq 11503 sqgcd 11510 dvdssqlem 11511 lcmgcdlem 11551 coprmgcdb 11562 qredeq 11570 qredeu 11571 prmdvdsfz 11612 sqrt2irr 11633 divdenle 11667 phibndlem 11684 hashgcdlem 11695 oddennn 11697 exmidunben 11731 |
Copyright terms: Public domain | W3C validator |