![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nnrei | Structured version Visualization version GIF version |
Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.) |
Ref | Expression |
---|---|
nnre.1 | ⊢ 𝐴 ∈ ℕ |
Ref | Expression |
---|---|
nnrei | ⊢ 𝐴 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnre.1 | . 2 ⊢ 𝐴 ∈ ℕ | |
2 | nnre 11320 | . 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2157 ℝcr 10223 ℕcn 11312 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183 ax-1cn 10282 ax-icn 10283 ax-addcl 10284 ax-addrcl 10285 ax-mulcl 10286 ax-mulrcl 10287 ax-i2m1 10292 ax-1ne0 10293 ax-rrecex 10296 ax-cnre 10297 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-ral 3094 df-rex 3095 df-reu 3096 df-rab 3098 df-v 3387 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-pss 3785 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-tp 4373 df-op 4375 df-uni 4629 df-iun 4712 df-br 4844 df-opab 4906 df-mpt 4923 df-tr 4946 df-id 5220 df-eprel 5225 df-po 5233 df-so 5234 df-fr 5271 df-we 5273 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-pred 5898 df-ord 5944 df-on 5945 df-lim 5946 df-suc 5947 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-ov 6881 df-om 7300 df-wrecs 7645 df-recs 7707 df-rdg 7745 df-nn 11313 |
This theorem is referenced by: nncniOLD 11324 nnne0i 11353 10reOLD 11803 numlt 11809 numltc 11810 faclbnd4lem1 13333 ef01bndlem 15250 dvdslelem 15370 divalglem6 15457 pockthi 15944 modsubi 16109 prmlem1 16142 prmlem2 16154 strleun 16293 strle1 16294 oppchomfval 16688 oppcbas 16692 rescco 16806 opprlem 18944 sralem 19500 opsrbaslem 19800 zlmlem 20187 znbaslem 20208 tnglem 22772 log2ublem1 25025 log2ublem2 25026 log2ub 25028 bpos1lem 25359 bposlem8 25368 bposlem9 25369 ttgval 26112 ttglem 26113 cchhllem 26124 slotsbaseefdif 26230 structvtxvallem 26255 lmat22e12 30401 lmat22e21 30402 lmat22e22 30403 ballotlem2 31067 ballotlem5 31078 ballotth 31116 chtvalz 31227 hgt750lem 31249 tgoldbachgt 31261 cnndvlem1 33036 hlhilslem 37959 jm2.27dlem2 38362 bgoldbtbndlem1 42475 tgblthelfgott 42485 tgoldbachlt 42486 |
Copyright terms: Public domain | W3C validator |