Theorem nnlesq

Description: A positive integer is less than or equal to its square. For general integers, see zzlesq . (Contributed by NM, 15-Sep-1999) (Revised by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Assertion	nnlesq	$$⊢N\in \mathbb{N}\to N\le N^2$$

Proof

Step	Hyp	Ref	Expression
1		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
2	1	mulridd	$$⊢N\in \mathbb{N}\to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1=N$$
3		nnge1	$$⊢N\in \mathbb{N}\to 1\le N$$
4		1red	$$⊢N\in \mathbb{N}\to 1\in ℝ$$
5		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
6		nngt0	$$⊢N\in \mathbb{N}\to 0<N$$
7		lemul2	$$⊢\left(1\in ℝ\wedge N\in ℝ\wedge \left(N\in ℝ\wedge 0<N\right)\right)\to \left(1\le N\leftrightarrow \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
8	4 5 5 6 7	syl112anc	$$⊢N\in \mathbb{N}\to \left(1\le N\leftrightarrow \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
9	3 8	mpbid	$$⊢N\in \mathbb{N}\to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
10	2 9	eqbrtrrd	$$⊢N\in \mathbb{N}\to N\le \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
11		sqval	$$⊢N\in ℂ\to N^2=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
12	1 11	syl	$$⊢N\in \mathbb{N}\to N^2=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
13	10 12	breqtrrd	$$⊢N\in \mathbb{N}\to N\le N^2$$