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

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