![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nnssre | Structured version Visualization version GIF version |
Description: The positive integers are a subset of the reals. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.) |
Ref | Expression |
---|---|
nnssre | ⊢ ℕ ⊆ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 10487 | . 2 ⊢ 1 ∈ ℝ | |
2 | peano2re 10660 | . . 3 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ) | |
3 | 2 | rgen 3115 | . 2 ⊢ ∀𝑥 ∈ ℝ (𝑥 + 1) ∈ ℝ |
4 | peano5nni 11489 | . 2 ⊢ ((1 ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝑥 + 1) ∈ ℝ) → ℕ ⊆ ℝ) | |
5 | 1, 3, 4 | mp2an 688 | 1 ⊢ ℕ ⊆ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2081 ∀wral 3105 ⊆ wss 3859 (class class class)co 7016 ℝcr 10382 1c1 10384 + caddc 10386 ℕcn 11486 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-1cn 10441 ax-icn 10442 ax-addcl 10443 ax-addrcl 10444 ax-mulcl 10445 ax-mulrcl 10446 ax-i2m1 10451 ax-1ne0 10452 ax-rrecex 10455 ax-cnre 10456 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-pss 3876 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-tp 4477 df-op 4479 df-uni 4746 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-tr 5064 df-id 5348 df-eprel 5353 df-po 5362 df-so 5363 df-fr 5402 df-we 5404 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-pred 6023 df-ord 6069 df-on 6070 df-lim 6071 df-suc 6072 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-ov 7019 df-om 7437 df-wrecs 7798 df-recs 7860 df-rdg 7898 df-nn 11487 |
This theorem is referenced by: nnre 11493 dfnn3 11500 nnred 11501 nnunb 11741 nn0ssre 11749 isercolllem1 14855 isercolllem2 14856 isercoll 14858 o1fsum 15001 ruc 15429 prmgaplem3 16218 prmgaplem4 16219 gsumval3 18748 ovolctb2 23776 ovolicc2lem3 23803 ovolicc2lem4 23804 iundisj2 23833 iundisj2f 30030 ssnnssfz 30198 iundisjfi 30205 iundisj2fi 30206 xrsmulgzz 30339 ballotlemsup 31379 reprlt 31507 reprgt 31509 erdszelem5 32050 erdszelem7 32052 erdszelem8 32053 incsequz2 34556 stoweidlem34 41861 fourierdlem31 41965 prmdvdsfmtnof1lem1 43228 prmdvdsfmtnof 43230 |
Copyright terms: Public domain | W3C validator |