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