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	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≤ ( 𝑁 ↑ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
2	1	mulridd	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 · 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 ) )