Theorem nn0le2msqi

Description: The square function on nonnegative integers is monotonic. (Contributed by Raph Levien, 10-Dec-2002)

	Ref	Expression
Hypotheses	nn0le2msqi.1	⊢ 𝐴 ∈ ℕ0
	nn0le2msqi.2	⊢ 𝐵 ∈ ℕ0
Assertion	nn0le2msqi	⊢ ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0le2msqi.1	⊢ 𝐴 ∈ ℕ0
2		nn0le2msqi.2	⊢ 𝐵 ∈ ℕ0
3	1	nn0ge0i	⊢ 0 ≤ 𝐴
4	2	nn0ge0i	⊢ 0 ≤ 𝐵
5	1	nn0rei	⊢ 𝐴 ∈ ℝ
6	2	nn0rei	⊢ 𝐵 ∈ ℝ
7	5 6	le2sqi	⊢ ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐵 ↑ 2 ) ) )
8	3 4 7	mp2an	⊢ ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐵 ↑ 2 ) )
9	1	nn0cni	⊢ 𝐴 ∈ ℂ
10	9	sqvali	⊢ ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 )
11	2	nn0cni	⊢ 𝐵 ∈ ℂ
12	11	sqvali	⊢ ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 )
13	10 12	breq12i	⊢ ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 ↑ 2 ) ↔ ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐵 ) )
14	8 13	bitri	⊢ ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐵 ) )