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 ) ) |