Metamath Proof Explorer


Theorem zzlesq

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

Ref Expression
Assertion zzlesq N N N 2

Proof

Step Hyp Ref Expression
1 elznn N N N N 0
2 animorrl N N N N N 0
3 olc N N 0 N N N 0
4 2 3 jaodan N N N 0 N N N 0
5 1 4 sylbi N N N N 0
6 nnlesq N N N 2
7 simpl N N 0 N
8 0red N N 0 0
9 7 resqcld N N 0 N 2
10 nn0ge0 N 0 0 N
11 le0neg1 N N 0 0 N
12 11 biimpar N 0 N N 0
13 10 12 sylan2 N N 0 N 0
14 7 sqge0d N N 0 0 N 2
15 7 8 9 13 14 letrd N N 0 N N 2
16 6 15 jaoi N N N 0 N N 2
17 5 16 syl N N N 2