Metamath Proof Explorer

Theorem lt2sq

Description: The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 24-Feb-2006)

Ref Expression
Assertion lt2sq ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A < B ↔ A 2 < B 2

Proof

Step Hyp Ref Expression
1 lt2msq ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A < B ↔ A ⁢ A < B ⁢ B
2 recn ⊢ A ∈ ℝ → A ∈ ℂ
3 recn ⊢ B ∈ ℝ → B ∈ ℂ
4 sqval ⊢ A ∈ ℂ → A 2 = A ⁢ A
5 sqval ⊢ B ∈ ℂ → B 2 = B ⁢ B
6 4 5 breqan12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 < B 2 ↔ A ⁢ A < B ⁢ B
7 2 3 6 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A 2 < B 2 ↔ A ⁢ A < B ⁢ B
8 7 ad2ant2r ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A 2 < B 2 ↔ A ⁢ A < B ⁢ B
9 1 8 bitr4d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A < B ↔ A 2 < B 2