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 8688 | . 2 | |
2 | 1 | sseli 3063 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 cr 7587 cn 8684 |
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 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 ax-sep 4016 ax-cnex 7679 ax-resscn 7680 ax-1re 7682 ax-addrcl 7685 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-ral 2398 df-v 2662 df-in 3047 df-ss 3054 df-int 3742 df-inn 8685 |
This theorem is referenced by: nnrei 8693 peano2nn 8696 nn1suc 8703 nnge1 8707 nnle1eq1 8708 nngt0 8709 nnnlt1 8710 nnap0 8713 nn2ge 8717 nn1gt1 8718 nndivre 8720 nnrecgt0 8722 nnsub 8723 arch 8932 nnrecl 8933 bndndx 8934 nn0ge0 8960 0mnnnnn0 8967 nnnegz 9015 elnnz 9022 elz2 9080 gtndiv 9104 prime 9108 btwnz 9128 qre 9373 nnrp 9406 nnledivrp 9508 fzo1fzo0n0 9915 elfzo0le 9917 fzonmapblen 9919 ubmelfzo 9932 fzonn0p1p1 9945 elfzom1p1elfzo 9946 ubmelm1fzo 9958 subfzo0 9974 adddivflid 10020 flltdivnn0lt 10032 intfracq 10048 flqdiv 10049 m1modnnsub1 10098 addmodid 10100 modfzo0difsn 10123 nnlesq 10351 facndiv 10440 faclbnd 10442 faclbnd3 10444 bcval5 10464 seq3coll 10540 caucvgre 10708 efaddlem 11294 nndivdvds 11411 nno 11515 nnoddm1d2 11519 divalglemnn 11527 divalg2 11535 ndvdsadd 11540 gcdmultiple 11620 gcdmultiplez 11621 gcdzeq 11622 sqgcd 11629 dvdssqlem 11630 lcmgcdlem 11670 coprmgcdb 11681 qredeq 11689 qredeu 11690 prmdvdsfz 11731 sqrt2irr 11752 divdenle 11786 phibndlem 11803 hashgcdlem 11814 oddennn 11816 exmidunben 11850 |
Copyright terms: Public domain | W3C validator |