Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
Integer powers
zzlesq
Next ⟩
iexpcyc
Metamath Proof Explorer
Ascii
Unicode
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