Metamath Proof Explorer


Theorem xmulneg1

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

Ref Expression
Assertion xmulneg1 A * B * A 𝑒 B = A 𝑒 B

Proof

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