Metamath Proof Explorer

Theorem lt2msq

Description: Two nonnegative numbers compare the same as their squares. (Contributed by Roy F. Longton, 8-Aug-2005) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion lt2msq ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A < B ↔ A ⁢ A < B ⁢ B

Proof

Step Hyp Ref Expression
1 lt2msq1 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ A < B → A ⁢ A < B ⁢ B
2 1 3expia ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ → A < B → A ⁢ A < B ⁢ B
3 2 adantrr ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A < B → A ⁢ A < B ⁢ B
4 id ⊢ A = B → A = B
5 4 4 oveq12d ⊢ A = B → A ⁢ A = B ⁢ B
6 5 a1i ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A = B → A ⁢ A = B ⁢ B
7 lt2msq1 ⊢ B ∈ ℝ ∧ 0 ≤ B ∧ A ∈ ℝ ∧ B < A → B ⁢ B < A ⁢ A
8 7 3expia ⊢ B ∈ ℝ ∧ 0 ≤ B ∧ A ∈ ℝ → B < A → B ⁢ B < A ⁢ A
9 8 adantrr ⊢ B ∈ ℝ ∧ 0 ≤ B ∧ A ∈ ℝ ∧ 0 ≤ A → B < A → B ⁢ B < A ⁢ A
10 9 ancoms ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → B < A → B ⁢ B < A ⁢ A
11 6 10 orim12d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A = B ∨ B < A → A ⁢ A = B ⁢ B ∨ B ⁢ B < A ⁢ A
12 11 con3d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → ¬ A ⁢ A = B ⁢ B ∨ B ⁢ B < A ⁢ A → ¬ A = B ∨ B < A
13 simpll ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ∈ ℝ
14 13 13 remulcld ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ⁢ A ∈ ℝ
15 simprl ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → B ∈ ℝ
16 15 15 remulcld ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → B ⁢ B ∈ ℝ
17 14 16 lttrid ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ⁢ A < B ⁢ B ↔ ¬ A ⁢ A = B ⁢ B ∨ B ⁢ B < A ⁢ A
18 13 15 lttrid ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A < B ↔ ¬ A = B ∨ B < A
19 12 17 18 3imtr4d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ⁢ A < B ⁢ B → A < B
20 3 19 impbid ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A < B ↔ A ⁢ A < B ⁢ B