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 ) ) |