Metamath Proof Explorer

Theorem xmulneg1

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

Ref Expression
Assertion xmulneg1 
|- ( ( A e. RR* /\ B e. RR* ) -> ( -e A *e B ) = -e ( A *e B ) )

Proof

Step Hyp Ref Expression
1 xneg0 
 |-  -e 0 = 0
2 1 eqeq2i 
 |-  ( -e A = -e 0 <-> -e A = 0 )
3 0xr 
 |-  0 e. RR*
4 xneg11 
 |-  ( ( A e. RR* /\ 0 e. RR* ) -> ( -e A = -e 0 <-> A = 0 ) )
5 3 4 mpan2 
 |-  ( A e. RR* -> ( -e A = -e 0 <-> A = 0 ) )
6 2 5 bitr3id 
 |-  ( A e. RR* -> ( -e A = 0 <-> A = 0 ) )
7 6 adantr 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e A = 0 <-> A = 0 ) )
8 7 orbi1d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( -e A = 0 \/ B = 0 ) <-> ( A = 0 \/ B = 0 ) ) )
9 8 ifbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> if ( ( -e A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) ) = if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) ) )
10 xnegpnf 
 |-  -e +oo = -oo
11 10 eqeq2i 
 |-  ( -e A = -e +oo <-> -e A = -oo )
12 simpll 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> A e. RR* )
13 pnfxr 
 |-  +oo e. RR*
14 xneg11 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( -e A = -e +oo <-> A = +oo ) )
15 12 13 14 sylancl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( -e A = -e +oo <-> A = +oo ) )
16 11 15 bitr3id 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( -e A = -oo <-> A = +oo ) )
17 16 anbi2d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( 0 < B /\ -e A = -oo ) <-> ( 0 < B /\ A = +oo ) ) )
18 xnegmnf 
 |-  -e -oo = +oo
19 18 eqeq2i 
 |-  ( -e A = -e -oo <-> -e A = +oo )
20 mnfxr 
 |-  -oo e. RR*
21 xneg11 
 |-  ( ( A e. RR* /\ -oo e. RR* ) -> ( -e A = -e -oo <-> A = -oo ) )
22 12 20 21 sylancl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( -e A = -e -oo <-> A = -oo ) )
23 19 22 bitr3id 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( -e A = +oo <-> A = -oo ) )
24 23 anbi2d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( B < 0 /\ -e A = +oo ) <-> ( B < 0 /\ A = -oo ) ) )
25 17 24 orbi12d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) <-> ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) )
26 xlt0neg1 
 |-  ( A e. RR* -> ( A < 0 <-> 0 < -e A ) )
27 26 ad2antrr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( A < 0 <-> 0 < -e A ) )
28 27 bicomd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( 0 < -e A <-> A < 0 ) )
29 28 anbi1d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( 0 < -e A /\ B = -oo ) <-> ( A < 0 /\ B = -oo ) ) )
30 xlt0neg2 
 |-  ( A e. RR* -> ( 0 < A <-> -e A < 0 ) )
31 30 ad2antrr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( 0 < A <-> -e A < 0 ) )
32 31 bicomd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( -e A < 0 <-> 0 < A ) )
33 32 anbi1d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( -e A < 0 /\ B = +oo ) <-> ( 0 < A /\ B = +oo ) ) )
34 29 33 orbi12d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) <-> ( ( A < 0 /\ B = -oo ) \/ ( 0 < A /\ B = +oo ) ) ) )
35 orcom 
 |-  ( ( ( A < 0 /\ B = -oo ) \/ ( 0 < A /\ B = +oo ) ) <-> ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) )
36 34 35 bitrdi 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) <-> ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) )
37 25 36 orbi12d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) <-> ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) )
38 37 biimpar 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) -> ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) )
39 38 iftrued 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) -> if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) = -oo )
40 xmullem2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) )
41 40 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) )
42 23 anbi2d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( 0 < B /\ -e A = +oo ) <-> ( 0 < B /\ A = -oo ) ) )
43 16 anbi2d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( B < 0 /\ -e A = -oo ) <-> ( B < 0 /\ A = +oo ) ) )
44 42 43 orbi12d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) <-> ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) )
45 28 anbi1d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( 0 < -e A /\ B = +oo ) <-> ( A < 0 /\ B = +oo ) ) )
46 32 anbi1d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( -e A < 0 /\ B = -oo ) <-> ( 0 < A /\ B = -oo ) ) )
47 45 46 orbi12d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) <-> ( ( A < 0 /\ B = +oo ) \/ ( 0 < A /\ B = -oo ) ) ) )
48 orcom 
 |-  ( ( ( A < 0 /\ B = +oo ) \/ ( 0 < A /\ B = -oo ) ) <-> ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) )
49 47 48 bitrdi 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) <-> ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) )
50 44 49 orbi12d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) <-> ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) )
51 50 notbid 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( -. ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) <-> -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) )
52 41 51 sylibrd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> -. ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) ) )
53 52 imp 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) -> -. ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) )
54 53 iffalsed 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) -> if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) = if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) )
55 iftrue 
 |-  ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = +oo )
56 55 adantl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) -> if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = +oo )
57 xnegeq 
 |-  ( if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = +oo -> -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = -e +oo )
58 56 57 syl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) -> -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = -e +oo )
59 58 10 eqtrdi 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) -> -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = -oo )
60 39 54 59 3eqtr4d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) -> if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) = -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) )
61 50 biimpar 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) )
62 61 iftrued 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) = +oo )
63 41 con2d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) -> -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) )
64 63 imp 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) )
65 64 iffalsed 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) )
66 iftrue 
 |-  ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) -> if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) = -oo )
67 66 adantl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) = -oo )
68 65 67 eqtrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = -oo )
69 xnegeq 
 |-  ( if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = -oo -> -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = -e -oo )
70 68 69 syl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = -e -oo )
71 70 18 eqtrdi 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = +oo )
72 62 71 eqtr4d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) = -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) )
73 72 adantlr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) = -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) )
74 37 notbid 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( -. ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) <-> -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) )
75 74 biimpar 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) -> -. ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) )
76 75 adantr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> -. ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) )
77 76 iffalsed 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) = ( -e A x. B ) )
78 51 biimpar 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> -. ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) )
79 78 adantlr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> -. ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) )
80 79 iffalsed 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) = if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) )
81 iffalse 
 |-  ( -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) )
82 81 ad2antlr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) )
83 iffalse 
 |-  ( -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) -> if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) = ( A x. B ) )
84 83 adantl 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) = ( A x. B ) )
85 82 84 eqtrd 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = ( A x. B ) )
86 xnegeq 
 |-  ( if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = ( A x. B ) -> -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = -e ( A x. B ) )
87 85 86 syl 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = -e ( A x. B ) )
88 xmullem 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> A e. RR )
89 88 recnd 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> A e. CC )
90 ancom 
 |-  ( ( A e. RR* /\ B e. RR* ) <-> ( B e. RR* /\ A e. RR* ) )
91 orcom 
 |-  ( ( A = 0 \/ B = 0 ) <-> ( B = 0 \/ A = 0 ) )
92 91 notbii 
 |-  ( -. ( A = 0 \/ B = 0 ) <-> -. ( B = 0 \/ A = 0 ) )
93 90 92 anbi12i 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) <-> ( ( B e. RR* /\ A e. RR* ) /\ -. ( B = 0 \/ A = 0 ) ) )
94 orcom 
 |-  ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) <-> ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) )
95 94 notbii 
 |-  ( -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) <-> -. ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) )
96 93 95 anbi12i 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) <-> ( ( ( B e. RR* /\ A e. RR* ) /\ -. ( B = 0 \/ A = 0 ) ) /\ -. ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) ) )
97 orcom 
 |-  ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) <-> ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) )
98 97 notbii 
 |-  ( -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) <-> -. ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) )
99 xmullem 
 |-  ( ( ( ( ( B e. RR* /\ A e. RR* ) /\ -. ( B = 0 \/ A = 0 ) ) /\ -. ( ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) \/ ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) ) /\ -. ( ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) \/ ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) ) -> B e. RR )
100 96 98 99 syl2anb 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> B e. RR )
101 100 recnd 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> B e. CC )
102 89 101 mulneg1d 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> ( -u A x. B ) = -u ( A x. B ) )
103 rexneg 
 |-  ( A e. RR -> -e A = -u A )
104 88 103 syl 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> -e A = -u A )
105 104 oveq1d 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> ( -e A x. B ) = ( -u A x. B ) )
106 88 100 remulcld 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> ( A x. B ) e. RR )
107 rexneg 
 |-  ( ( A x. B ) e. RR -> -e ( A x. B ) = -u ( A x. B ) )
108 106 107 syl 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> -e ( A x. B ) = -u ( A x. B ) )
109 102 105 108 3eqtr4d 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> ( -e A x. B ) = -e ( A x. B ) )
110 87 109 eqtr4d 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) = ( -e A x. B ) )
111 77 80 110 3eqtr4d 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) = -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) )
112 73 111 pm2.61dan 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) -> if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) = -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) )
113 60 112 pm2.61dan 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) -> if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) = -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) )
114 113 ifeq2da 
 |-  ( ( A e. RR* /\ B e. RR* ) -> if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) ) = if ( ( A = 0 \/ B = 0 ) , 0 , -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) )
115 9 114 eqtrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> if ( ( -e A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) ) = if ( ( A = 0 \/ B = 0 ) , 0 , -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) )
116 xnegeq 
 |-  ( if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) = 0 -> -e if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) = -e 0 )
117 116 1 eqtrdi 
 |-  ( if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) = 0 -> -e if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) = 0 )
118 xnegeq 
 |-  ( if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) = if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) -> -e if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) = -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) )
119 117 118 ifsb 
 |-  -e if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) = if ( ( A = 0 \/ B = 0 ) , 0 , -e if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) )
120 115 119 eqtr4di 
 |-  ( ( A e. RR* /\ B e. RR* ) -> if ( ( -e A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) ) = -e if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) )
121 xnegcl 
 |-  ( A e. RR* -> -e A e. RR* )
122 xmulval 
 |-  ( ( -e A e. RR* /\ B e. RR* ) -> ( -e A *e B ) = if ( ( -e A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) ) )
123 121 122 sylan 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e A *e B ) = if ( ( -e A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ -e A = +oo ) \/ ( B < 0 /\ -e A = -oo ) ) \/ ( ( 0 < -e A /\ B = +oo ) \/ ( -e A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ -e A = -oo ) \/ ( B < 0 /\ -e A = +oo ) ) \/ ( ( 0 < -e A /\ B = -oo ) \/ ( -e A < 0 /\ B = +oo ) ) ) , -oo , ( -e A x. B ) ) ) ) )
124 xmulval 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A *e B ) = if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) )
125 xnegeq 
 |-  ( ( A *e B ) = if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) -> -e ( A *e B ) = -e if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) )
126 124 125 syl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> -e ( A *e B ) = -e if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) )
127 120 123 126 3eqtr4d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e A *e B ) = -e ( A *e B ) )