Metamath Proof Explorer


Theorem xmulneg1

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

Ref Expression
Assertion xmulneg1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( -𝑒 𝐴 ·e 𝐵 ) = -𝑒 ( 𝐴 ·e 𝐵 ) )

Proof

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