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 8882 | . 2 ⊢ ℕ ⊆ ℝ | |
2 | 1 | sseli 3143 | 1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2141 ℝcr 7773 ℕcn 8878 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 ax-sep 4107 ax-cnex 7865 ax-resscn 7866 ax-1re 7868 ax-addrcl 7871 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-v 2732 df-in 3127 df-ss 3134 df-int 3832 df-inn 8879 |
This theorem is referenced by: nnrei 8887 peano2nn 8890 nn1suc 8897 nnge1 8901 nnle1eq1 8902 nngt0 8903 nnnlt1 8904 nnap0 8907 nn2ge 8911 nn1gt1 8912 nndivre 8914 nnrecgt0 8916 nnsub 8917 arch 9132 nnrecl 9133 bndndx 9134 nn0ge0 9160 0mnnnnn0 9167 nnnegz 9215 elnnz 9222 elz2 9283 gtndiv 9307 prime 9311 btwnz 9331 qre 9584 elpq 9607 elpqb 9608 nnrp 9620 nnledivrp 9723 fzo1fzo0n0 10139 elfzo0le 10141 fzonmapblen 10143 ubmelfzo 10156 fzonn0p1p1 10169 elfzom1p1elfzo 10170 ubmelm1fzo 10182 subfzo0 10198 adddivflid 10248 flltdivnn0lt 10260 intfracq 10276 flqdiv 10277 m1modnnsub1 10326 addmodid 10328 modfzo0difsn 10351 nnlesq 10579 facndiv 10673 faclbnd 10675 faclbnd3 10677 bcval5 10697 seq3coll 10777 caucvgre 10945 efaddlem 11637 nndivdvds 11758 nno 11865 nnoddm1d2 11869 divalglemnn 11877 divalg2 11885 ndvdsadd 11890 gcdmultiple 11975 gcdmultiplez 11976 gcdzeq 11977 sqgcd 11984 dvdssqlem 11985 lcmgcdlem 12031 coprmgcdb 12042 qredeq 12050 qredeu 12051 prmdvdsfz 12093 sqrt2irr 12116 divdenle 12151 phibndlem 12170 hashgcdlem 12192 oddprm 12213 pythagtriplem10 12223 pythagtriplem12 12229 pythagtriplem14 12231 pythagtriplem16 12233 pythagtriplem19 12236 pclemub 12241 pc2dvds 12283 pcmpt 12295 fldivp1 12300 pcbc 12303 infpnlem1 12311 oddennn 12347 exmidunben 12381 lgsval4a 13717 |
Copyright terms: Public domain | W3C validator |