Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nnrecre | Structured version Visualization version GIF version |
Description: The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.) |
Ref | Expression |
---|---|
nnrecre | ⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 10863 | . 2 ⊢ 1 ∈ ℝ | |
2 | nndivre 11901 | . 2 ⊢ ((1 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (1 / 𝑁) ∈ ℝ) | |
3 | 1, 2 | mpan 690 | 1 ⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2112 (class class class)co 7235 ℝcr 10758 1c1 10760 / cdiv 11519 ℕcn 11860 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-sep 5209 ax-nul 5216 ax-pow 5275 ax-pr 5339 ax-un 7545 ax-resscn 10816 ax-1cn 10817 ax-icn 10818 ax-addcl 10819 ax-addrcl 10820 ax-mulcl 10821 ax-mulrcl 10822 ax-mulcom 10823 ax-addass 10824 ax-mulass 10825 ax-distr 10826 ax-i2m1 10827 ax-1ne0 10828 ax-1rid 10829 ax-rnegex 10830 ax-rrecex 10831 ax-cnre 10832 ax-pre-lttri 10833 ax-pre-lttrn 10834 ax-pre-ltadd 10835 ax-pre-mulgt0 10836 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3425 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4255 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5153 df-tr 5179 df-id 5472 df-eprel 5478 df-po 5486 df-so 5487 df-fr 5527 df-we 5529 df-xp 5575 df-rel 5576 df-cnv 5577 df-co 5578 df-dm 5579 df-rn 5580 df-res 5581 df-ima 5582 df-pred 6179 df-ord 6237 df-on 6238 df-lim 6239 df-suc 6240 df-iota 6359 df-fun 6403 df-fn 6404 df-f 6405 df-f1 6406 df-fo 6407 df-f1o 6408 df-fv 6409 df-riota 7192 df-ov 7238 df-oprab 7239 df-mpo 7240 df-om 7667 df-wrecs 8071 df-recs 8132 df-rdg 8170 df-er 8415 df-en 8651 df-dom 8652 df-sdom 8653 df-pnf 10899 df-mnf 10900 df-xr 10901 df-ltxr 10902 df-le 10903 df-sub 11094 df-neg 11095 df-div 11520 df-nn 11861 |
This theorem is referenced by: nnrecred 11911 rpnnen1lem5 12607 fldiv 13465 supcvg 15453 harmonic 15456 rpnnen2lem11 15818 flodddiv4 16007 prmreclem4 16505 prmreclem5 16506 prmreclem6 16507 prmrec 16508 met1stc 23451 pcoass 23953 bcthlem4 24256 vitali 24542 ismbf3d 24583 itg2seq 24672 itg2gt0 24690 plyeq0lem 25136 logtayllem 25579 cxproot 25610 cxpeq 25675 quartlem3 25774 leibpi 25857 emcllem4 25913 emcllem6 25915 basellem6 26000 mulogsumlem 26444 pntpbnd2 26500 ipasslem4 28947 ipasslem5 28948 minvecolem5 28994 subfaclim 32894 faclim 33462 iccioo01 35269 poimirlem29 35580 poimirlem30 35581 xrralrecnnle 42643 xrralrecnnge 42651 iooiinicc 42801 iooiinioc 42815 stirlinglem1 43336 iinhoiicclem 43932 iunhoiioolem 43934 iccvonmbllem 43937 vonioolem1 43939 vonioolem2 43940 vonicclem1 43942 vonicclem2 43943 preimageiingt 43975 preimaleiinlt 43976 salpreimagtge 43979 salpreimaltle 43980 smflimlem6 44029 |
Copyright terms: Public domain | W3C validator |