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

Metamath Proof Explorer

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 ⊢ ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐵 ) )