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	$$⊢\mathbb{N}\subseteq ℝ$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		peano2re	$$⊢x\in ℝ\to x+1\in ℝ$$
3	2	rgen	$$⊢\forall x\in ℝx+1\in ℝ$$
4		peano5nni	$$⊢\left(1\in ℝ\wedge \forall x\in ℝx+1\in ℝ\right)\to \mathbb{N}\subseteq ℝ$$
5	1 3 4	mp2an	$$⊢\mathbb{N}\subseteq ℝ$$