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 8724 | . 2 | |
2 | 1 | sseli 3093 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 cr 7619 cn 8720 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-cnex 7711 ax-resscn 7712 ax-1re 7714 ax-addrcl 7717 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ral 2421 df-v 2688 df-in 3077 df-ss 3084 df-int 3772 df-inn 8721 |
This theorem is referenced by: nnrei 8729 peano2nn 8732 nn1suc 8739 nnge1 8743 nnle1eq1 8744 nngt0 8745 nnnlt1 8746 nnap0 8749 nn2ge 8753 nn1gt1 8754 nndivre 8756 nnrecgt0 8758 nnsub 8759 arch 8974 nnrecl 8975 bndndx 8976 nn0ge0 9002 0mnnnnn0 9009 nnnegz 9057 elnnz 9064 elz2 9122 gtndiv 9146 prime 9150 btwnz 9170 qre 9417 nnrp 9451 nnledivrp 9553 fzo1fzo0n0 9960 elfzo0le 9962 fzonmapblen 9964 ubmelfzo 9977 fzonn0p1p1 9990 elfzom1p1elfzo 9991 ubmelm1fzo 10003 subfzo0 10019 adddivflid 10065 flltdivnn0lt 10077 intfracq 10093 flqdiv 10094 m1modnnsub1 10143 addmodid 10145 modfzo0difsn 10168 nnlesq 10396 facndiv 10485 faclbnd 10487 faclbnd3 10489 bcval5 10509 seq3coll 10585 caucvgre 10753 efaddlem 11380 nndivdvds 11499 nno 11603 nnoddm1d2 11607 divalglemnn 11615 divalg2 11623 ndvdsadd 11628 gcdmultiple 11708 gcdmultiplez 11709 gcdzeq 11710 sqgcd 11717 dvdssqlem 11718 lcmgcdlem 11758 coprmgcdb 11769 qredeq 11777 qredeu 11778 prmdvdsfz 11819 sqrt2irr 11840 divdenle 11875 phibndlem 11892 hashgcdlem 11903 oddennn 11905 exmidunben 11939 |
Copyright terms: Public domain | W3C validator |