Theorem zzlesq

Description: An integer is less than or equal to its square. (Contributed by BJ, 6-Feb-2025)

	Ref	Expression
Assertion	zzlesq	|- ( N e. ZZ -> N <_ ( N ^ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		elznn	|- ( N e. ZZ <-> ( N e. RR /\ ( N e. NN \/ -u N e. NN0 ) ) )
2		animorrl	|- ( ( N e. RR /\ N e. NN ) -> ( N e. NN \/ ( N e. RR /\ -u N e. NN0 ) ) )
3		olc	|- ( ( N e. RR /\ -u N e. NN0 ) -> ( N e. NN \/ ( N e. RR /\ -u N e. NN0 ) ) )
4	2 3	jaodan	|- ( ( N e. RR /\ ( N e. NN \/ -u N e. NN0 ) ) -> ( N e. NN \/ ( N e. RR /\ -u N e. NN0 ) ) )
5	1 4	sylbi	|- ( N e. ZZ -> ( N e. NN \/ ( N e. RR /\ -u N e. NN0 ) ) )
6		nnlesq	|- ( N e. NN -> N <_ ( N ^ 2 ) )
7		simpl	|- ( ( N e. RR /\ -u N e. NN0 ) -> N e. RR )
8		0red	|- ( ( N e. RR /\ -u N e. NN0 ) -> 0 e. RR )
9	7	resqcld	|- ( ( N e. RR /\ -u N e. NN0 ) -> ( N ^ 2 ) e. RR )
10		nn0ge0	|- ( -u N e. NN0 -> 0 <_ -u N )
11		le0neg1	|- ( N e. RR -> ( N <_ 0 <-> 0 <_ -u N ) )
12	11	biimpar	|- ( ( N e. RR /\ 0 <_ -u N ) -> N <_ 0 )
13	10 12	sylan2	|- ( ( N e. RR /\ -u N e. NN0 ) -> N <_ 0 )
14	7	sqge0d	|- ( ( N e. RR /\ -u N e. NN0 ) -> 0 <_ ( N ^ 2 ) )
15	7 8 9 13 14	letrd	|- ( ( N e. RR /\ -u N e. NN0 ) -> N <_ ( N ^ 2 ) )
16	6 15	jaoi	|- ( ( N e. NN \/ ( N e. RR /\ -u N e. NN0 ) ) -> N <_ ( N ^ 2 ) )
17	5 16	syl	|- ( N e. ZZ -> N <_ ( N ^ 2 ) )