This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 e. NN -> N <_ ( N ^ 2 ) )

Proof

Step Hyp Ref Expression
1 nncn 
 |-  ( N e. NN -> N e. CC )
2 1 mulridd 
 |-  ( 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 ) )