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