Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nnre | GIF version |
Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
Ref | Expression |
---|---|
nnre | ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnssre 8837 | . 2 ⊢ ℕ ⊆ ℝ | |
2 | 1 | sseli 3124 | 1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2128 ℝcr 7731 ℕcn 8833 |
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 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 ax-sep 4082 ax-cnex 7823 ax-resscn 7824 ax-1re 7826 ax-addrcl 7829 |
This theorem depends on definitions: df-bi 116 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ral 2440 df-v 2714 df-in 3108 df-ss 3115 df-int 3808 df-inn 8834 |
This theorem is referenced by: nnrei 8842 peano2nn 8845 nn1suc 8852 nnge1 8856 nnle1eq1 8857 nngt0 8858 nnnlt1 8859 nnap0 8862 nn2ge 8866 nn1gt1 8867 nndivre 8869 nnrecgt0 8871 nnsub 8872 arch 9087 nnrecl 9088 bndndx 9089 nn0ge0 9115 0mnnnnn0 9122 nnnegz 9170 elnnz 9177 elz2 9235 gtndiv 9259 prime 9263 btwnz 9283 qre 9534 elpq 9557 elpqb 9558 nnrp 9570 nnledivrp 9673 fzo1fzo0n0 10082 elfzo0le 10084 fzonmapblen 10086 ubmelfzo 10099 fzonn0p1p1 10112 elfzom1p1elfzo 10113 ubmelm1fzo 10125 subfzo0 10141 adddivflid 10191 flltdivnn0lt 10203 intfracq 10219 flqdiv 10220 m1modnnsub1 10269 addmodid 10271 modfzo0difsn 10294 nnlesq 10522 facndiv 10613 faclbnd 10615 faclbnd3 10617 bcval5 10637 seq3coll 10713 caucvgre 10881 efaddlem 11571 nndivdvds 11692 nno 11797 nnoddm1d2 11801 divalglemnn 11809 divalg2 11817 ndvdsadd 11822 gcdmultiple 11904 gcdmultiplez 11905 gcdzeq 11906 sqgcd 11913 dvdssqlem 11914 lcmgcdlem 11954 coprmgcdb 11965 qredeq 11973 qredeu 11974 prmdvdsfz 12016 sqrt2irr 12037 divdenle 12072 phibndlem 12091 hashgcdlem 12113 oddennn 12132 exmidunben 12166 |
Copyright terms: Public domain | W3C validator |