Metamath Proof Explorer


Theorem xltneg

Description: Extended real version of ltneg . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xltneg A * B * A < B B < A

Proof

Step Hyp Ref Expression
1 xltnegi A * B * A < B B < A
2 1 3expia A * B * A < B B < A
3 xnegcl B * B *
4 xnegcl A * A *
5 xltnegi B * A * B < A A < B
6 5 3expia B * A * B < A A < B
7 3 4 6 syl2anr A * B * B < A A < B
8 xnegneg A * A = A
9 xnegneg B * B = B
10 8 9 breqan12d A * B * A < B A < B
11 7 10 sylibd A * B * B < A A < B
12 2 11 impbid A * B * A < B B < A