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 A0AB0BA<BAA<BB

Proof

Step Hyp Ref Expression
1 lt2msq1 A0ABA<BAA<BB
2 1 3expia A0ABA<BAA<BB
3 2 adantrr A0AB0BA<BAA<BB
4 id A=BA=B
5 4 4 oveq12d A=BAA=BB
6 5 a1i A0AB0BA=BAA=BB
7 lt2msq1 B0BAB<ABB<AA
8 7 3expia B0BAB<ABB<AA
9 8 adantrr B0BA0AB<ABB<AA
10 9 ancoms A0AB0BB<ABB<AA
11 6 10 orim12d A0AB0BA=BB<AAA=BBBB<AA
12 11 con3d A0AB0B¬AA=BBBB<AA¬A=BB<A
13 simpll A0AB0BA
14 13 13 remulcld A0AB0BAA
15 simprl A0AB0BB
16 15 15 remulcld A0AB0BBB
17 14 16 lttrid A0AB0BAA<BB¬AA=BBBB<AA
18 13 15 lttrid A0AB0BA<B¬A=BB<A
19 12 17 18 3imtr4d A0AB0BAA<BBA<B
20 3 19 impbid A0AB0BA<BAA<BB