Metamath Proof Explorer


Theorem nnlesq

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

Ref Expression
Assertion nnlesq ( 𝑁 ∈ ℕ → 𝑁 ≤ ( 𝑁 ↑ 2 ) )

Proof

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