Metamath Proof Explorer

Theorem nnssre

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
Assertion nnssre 
|- NN C_ RR

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 peano2re 
 |-  ( x e. RR -> ( x + 1 ) e. RR )
3 2 rgen 
 |-  A. x e. RR ( x + 1 ) e. RR
4 peano5nni 
 |-  ( ( 1 e. RR /\ A. x e. RR ( x + 1 ) e. RR ) -> NN C_ RR )
5 1 3 4 mp2an 
 |-  NN C_ RR