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≤N2

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≤N2
7 simpl ⊢N∈ℝ∧−N∈ℕ0→N∈ℝ
8 0red ⊢N∈ℝ∧−N∈ℕ0→0∈ℝ
9 7 resqcld ⊢N∈ℝ∧−N∈ℕ0→N2∈ℝ
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≤N2
15 7 8 9 13 14 letrd ⊢N∈ℝ∧−N∈ℕ0→N≤N2
16 6 15 jaoi ⊢N∈ℕ∨N∈ℝ∧−N∈ℕ0→N≤N2
17 5 16 syl ⊢N∈ℤ→N≤N2