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

Metamath Proof Explorer

Theorem nnlesq

Description: A positive integer is less than or equal to its square. For general integers, see zzlesq . (Contributed by NM, 15-Sep-1999) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion nnlesq ⊢ N ∈ ℕ → N ≤ N 2

Proof

Step Hyp Ref Expression
1 nncn ⊢ N ∈ ℕ → N ∈ ℂ
2 1 mulridd ⊢ N ∈ ℕ → N ⋅ 1 = N
3 nnge1 ⊢ N ∈ ℕ → 1 ≤ N
4 1red ⊢ N ∈ ℕ → 1 ∈ ℝ
5 nnre ⊢ N ∈ ℕ → N ∈ ℝ
6 nngt0 ⊢ N ∈ ℕ → 0 < N
7 lemul2 ⊢ 1 ∈ ℝ ∧ N ∈ ℝ ∧ N ∈ ℝ ∧ 0 < N → 1 ≤ N ↔ N ⋅ 1 ≤ N ⋅ N
8 4 5 5 6 7 syl112anc ⊢ N ∈ ℕ → 1 ≤ N ↔ N ⋅ 1 ≤ N ⋅ N
9 3 8 mpbid ⊢ N ∈ ℕ → N ⋅ 1 ≤ N ⋅ N
10 2 9 eqbrtrrd ⊢ N ∈ ℕ → N ≤ N ⋅ N
11 sqval ⊢ N ∈ ℂ → N 2 = N ⋅ N
12 1 11 syl ⊢ N ∈ ℕ → N 2 = N ⋅ N
13 10 12 breqtrrd ⊢ N ∈ ℕ → N ≤ N 2