Theorem nnlesq

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

	Ref	Expression
Assertion	nnlesq	|- ( N e. NN -> N <_ ( N ^ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		nncn	|- ( N e. NN -> N e. CC )
2	1	mulid1d	|- ( N e. NN -> ( N x. 1 ) = N )
3		nnge1	|- ( N e. NN -> 1 <_ N )
4		1red	|- ( N e. NN -> 1 e. RR )
5		nnre	|- ( N e. NN -> N e. RR )
6		nngt0	|- ( N e. NN -> 0 < N )
7		lemul2	|- ( ( 1 e. RR /\ N e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( 1 <_ N <-> ( N x. 1 ) <_ ( N x. N ) ) )
8	4 5 5 6 7	syl112anc	|- ( N e. NN -> ( 1 <_ N <-> ( N x. 1 ) <_ ( N x. N ) ) )
9	3 8	mpbid	|- ( N e. NN -> ( N x. 1 ) <_ ( N x. N ) )
10	2 9	eqbrtrrd	|- ( N e. NN -> N <_ ( N x. N ) )
11		sqval	|- ( N e. CC -> ( N ^ 2 ) = ( N x. N ) )
12	1 11	syl	|- ( N e. NN -> ( N ^ 2 ) = ( N x. N ) )
13	10 12	breqtrrd	|- ( N e. NN -> N <_ ( N ^ 2 ) )