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 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐴 ) < ( 𝐵 · 𝐵 ) ) )

Proof

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