xmulneg1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xmulneg1		Structured version Visualization version GIF version

Theorem xmulneg1 13295

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

**Assertion**
Ref	Expression
xmulneg1	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (-_𝑒𝐴 ·_e 𝐵) = -_𝑒(𝐴 ·_e 𝐵))

**Proof of Theorem xmulneg1**
Step	Hyp	Ref	Expression
1		xneg0 13238	. . . . . . . . 9 ⊢ -_𝑒0 = 0
2	1	eqeq2i 2782	. . . . . . . 8 ⊢ (-_𝑒𝐴 = -_𝑒0 ↔ -_𝑒𝐴 = 0)
3		0xr 11256	. . . . . . . . 9 ⊢ 0 ∈ ℝ^*
4		xneg11 13241	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 0 ∈ ℝ^*) → (-_𝑒𝐴 = -_𝑒0 ↔ 𝐴 = 0))
5	3, 4	mpan2 703	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ^* → (-_𝑒𝐴 = -_𝑒0 ↔ 𝐴 = 0))
6	2, 5	bitr3id 288	. . . . . . 7 ⊢ (𝐴 ∈ ℝ^* → (-_𝑒𝐴 = 0 ↔ 𝐴 = 0))
7	6	adantr 485	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (-_𝑒𝐴 = 0 ↔ 𝐴 = 0))
8	7	orbi1d 929	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((-_𝑒𝐴 = 0 ∨ 𝐵 = 0) ↔ (𝐴 = 0 ∨ 𝐵 = 0)))
9	8	ifbid 4516	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → 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 13235	. . . . . . . . . . . . . 14 ⊢ -_𝑒+∞ = -∞
11	10	eqeq2i 2782	. . . . . . . . . . . . 13 ⊢ (-_𝑒𝐴 = -_𝑒+∞ ↔ -_𝑒𝐴 = -∞)
12		simpll 778	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → 𝐴 ∈ ℝ^)
13		pnfxr 11263	. . . . . . . . . . . . . 14 ⊢ +∞ ∈ ℝ^*
14		xneg11 13241	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (-_𝑒𝐴 = -_𝑒+∞ ↔ 𝐴 = +∞))
15	12, 13, 14	sylancl 597	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (-_𝑒𝐴 = -_𝑒+∞ ↔ 𝐴 = +∞))
16	11, 15	bitr3id 288	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (-_𝑒𝐴 = -∞ ↔ 𝐴 = +∞))
17	16	anbi2d 641	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ↔ (0 < 𝐵 ∧ 𝐴 = +∞)))
18		xnegmnf 13236	. . . . . . . . . . . . . 14 ⊢ -_𝑒-∞ = +∞
19	18	eqeq2i 2782	. . . . . . . . . . . . 13 ⊢ (-_𝑒𝐴 = -_𝑒-∞ ↔ -_𝑒𝐴 = +∞)
20		mnfxr 11266	. . . . . . . . . . . . . 14 ⊢ -∞ ∈ ℝ^*
21		xneg11 13241	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ -∞ ∈ ℝ^*) → (-_𝑒𝐴 = -_𝑒-∞ ↔ 𝐴 = -∞))
22	12, 20, 21	sylancl 597	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (-_𝑒𝐴 = -_𝑒-∞ ↔ 𝐴 = -∞))
23	19, 22	bitr3id 288	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (-_𝑒𝐴 = +∞ ↔ 𝐴 = -∞))
24	23	anbi2d 641	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((𝐵 < 0 ∧ -_𝑒𝐴 = +∞) ↔ (𝐵 < 0 ∧ 𝐴 = -∞)))
25	17, 24	orbi12d 931	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ↔ ((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞))))
26		xlt0neg1 13245	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℝ^* → (𝐴 < 0 ↔ 0 < -_𝑒𝐴))
27	26	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (𝐴 < 0 ↔ 0 < -_𝑒𝐴))
28	27	bicomd 226	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (0 < -_𝑒𝐴 ↔ 𝐴 < 0))
29	28	anbi1d 642	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ↔ (𝐴 < 0 ∧ 𝐵 = -∞)))
30		xlt0neg2 13246	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℝ^* → (0 < 𝐴 ↔ -_𝑒𝐴 < 0))
31	30	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (0 < 𝐴 ↔ -_𝑒𝐴 < 0))
32	31	bicomd 226	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (-_𝑒𝐴 < 0 ↔ 0 < 𝐴))
33	32	anbi1d 642	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((-_𝑒𝐴 < 0 ∧ 𝐵 = +∞) ↔ (0 < 𝐴 ∧ 𝐵 = +∞)))
34	29, 33	orbi12d 931	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞)) ↔ ((𝐴 < 0 ∧ 𝐵 = -∞) ∨ (0 < 𝐴 ∧ 𝐵 = +∞))))
35		orcom 883	. . . . . . . . . . 11 ⊢ (((𝐴 < 0 ∧ 𝐵 = -∞) ∨ (0 < 𝐴 ∧ 𝐵 = +∞)) ↔ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))
36	34, 35	bitrdi 290	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞)) ↔ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))))
37	25, 36	orbi12d 931	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))) ↔ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))))
38	37	biimpar 482	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → (((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))))
39	38	iftrued 4500	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵)) = -∞)
40		xmullem2 13291	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))))
41	40	adantr 485	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))))
42	23	anbi2d 641	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ↔ (0 < 𝐵 ∧ 𝐴 = -∞)))
43	16	anbi2d 641	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((𝐵 < 0 ∧ -_𝑒𝐴 = -∞) ↔ (𝐵 < 0 ∧ 𝐴 = +∞)))
44	42, 43	orbi12d 931	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ↔ ((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞))))
45	28	anbi1d 642	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ↔ (𝐴 < 0 ∧ 𝐵 = +∞)))
46	32	anbi1d 642	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((-_𝑒𝐴 < 0 ∧ 𝐵 = -∞) ↔ (0 < 𝐴 ∧ 𝐵 = -∞)))
47	45, 46	orbi12d 931	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞)) ↔ ((𝐴 < 0 ∧ 𝐵 = +∞) ∨ (0 < 𝐴 ∧ 𝐵 = -∞))))
48		orcom 883	. . . . . . . . . . . . 13 ⊢ (((𝐴 < 0 ∧ 𝐵 = +∞) ∨ (0 < 𝐴 ∧ 𝐵 = -∞)) ↔ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))
49	47, 48	bitrdi 290	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞)) ↔ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))))
50	44, 49	orbi12d 931	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))) ↔ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))))
51	50	notbid 321	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))) ↔ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))))
52	41, 51	sylibrd 262	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞)))))
53	52	imp 411	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → ¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))))
54	53	iffalsed 4503	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → if((((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵))) = if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵)))
55		iftrue 4498	. . . . . . . . . 10 ⊢ ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = +∞)
56	55	adantl 486	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = +∞)
57		xnegeq 13233	. . . . . . . . 9 ⊢ (if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = +∞ → -_𝑒if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -_𝑒+∞)
58	56, 57	syl 18	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → -_𝑒if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -_𝑒+∞)
59	58, 10	eqtrdi 2820	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → -_𝑒if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -∞)
60	39, 54, 59	3eqtr4d 2814	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 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 482	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))))
62	61	iftrued 4500	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵))) = +∞)
63	41	con2d 135	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) → ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))))
64	63	imp 411	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))))
65	64	iffalsed 4503	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))
66		iftrue 4498	. . . . . . . . . . . . 13 ⊢ ((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) → if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)) = -∞)
67	66	adantl 486	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)) = -∞)
68	65, 67	eqtrd 2804	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -∞)
69		xnegeq 13233	. . . . . . . . . . 11 ⊢ (if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -∞ → -_𝑒if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -_𝑒-∞)
70	68, 69	syl 18	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → -_𝑒if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -_𝑒-∞)
71	70, 18	eqtrdi 2820	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → -_𝑒if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = +∞)
72	62, 71	eqtr4d 2807	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 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 727	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 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 321	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))) ↔ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))))
75	74	biimpar 482	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → ¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))))
76	75	adantr 485	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → ¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))))
77	76	iffalsed 4503	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵)) = (-_𝑒𝐴 · 𝐵))
78	51	biimpar 482	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → ¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))))
79	78	adantlr 727	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → ¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))))
80	79	iffalsed 4503	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 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 4501	. . . . . . . . . . . 12 ⊢ (¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))
82	81	ad2antlr 739	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 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 4501	. . . . . . . . . . . 12 ⊢ (¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) → if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)) = (𝐴 · 𝐵))
84	83	adantl 486	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)) = (𝐴 · 𝐵))
85	82, 84	eqtrd 2804	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = (𝐴 · 𝐵))
86		xnegeq 13233	. . . . . . . . . 10 ⊢ (if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = (𝐴 · 𝐵) → -_𝑒if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -_𝑒(𝐴 · 𝐵))
87	85, 86	syl 18	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → -_𝑒if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -_𝑒(𝐴 · 𝐵))
88		xmullem 13290	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐴 ∈ ℝ)
89	88	recnd 11237	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐴 ∈ ℂ)
90		ancom 465	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ↔ (𝐵 ∈ ℝ^ ∧ 𝐴 ∈ ℝ^*))
91		orcom 883	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 = 0 ∨ 𝐵 = 0) ↔ (𝐵 = 0 ∨ 𝐴 = 0))
92	91	notbii 323	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝐴 = 0 ∨ 𝐵 = 0) ↔ ¬ (𝐵 = 0 ∨ 𝐴 = 0))
93	90, 92	anbi12i 639	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ↔ ((𝐵 ∈ ℝ^ ∧ 𝐴 ∈ ℝ^*) ∧ ¬ (𝐵 = 0 ∨ 𝐴 = 0)))
94		orcom 883	. . . . . . . . . . . . . . 15 ⊢ ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) ↔ (((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞))))
95	94	notbii 323	. . . . . . . . . . . . . 14 ⊢ (¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) ↔ ¬ (((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞))))
96	93, 95	anbi12i 639	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ↔ (((𝐵 ∈ ℝ^ ∧ 𝐴 ∈ ℝ^*) ∧ ¬ (𝐵 = 0 ∨ 𝐴 = 0)) ∧ ¬ (((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)))))
97		orcom 883	. . . . . . . . . . . . . 14 ⊢ ((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) ↔ (((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞))))
98	97	notbii 323	. . . . . . . . . . . . 13 ⊢ (¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) ↔ ¬ (((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞))))
99		xmullem 13290	. . . . . . . . . . . . 13 ⊢ (((((𝐵 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^*) ∧ ¬ (𝐵 = 0 ∨ 𝐴 = 0)) ∧ ¬ (((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)))) ∧ ¬ (((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)))) → 𝐵 ∈ ℝ)
100	96, 98, 99	syl2anb 609	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐵 ∈ ℝ)
101	100	recnd 11237	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐵 ∈ ℂ)
102	89, 101	mulneg1d 11667	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → (-𝐴 · 𝐵) = -(𝐴 · 𝐵))
103		rexneg 13237	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 = -𝐴)
104	88, 103	syl 18	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → -_𝑒𝐴 = -𝐴)
105	104	oveq1d 7426	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → (-_𝑒𝐴 · 𝐵) = (-𝐴 · 𝐵))
106	88, 100	remulcld 11239	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → (𝐴 · 𝐵) ∈ ℝ)
107		rexneg 13237	. . . . . . . . . . 11 ⊢ ((𝐴 · 𝐵) ∈ ℝ → -_𝑒(𝐴 · 𝐵) = -(𝐴 · 𝐵))
108	106, 107	syl 18	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → -_𝑒(𝐴 · 𝐵) = -(𝐴 · 𝐵))
109	102, 105, 108	3eqtr4d 2814	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → (-_𝑒𝐴 · 𝐵) = -_𝑒(𝐴 · 𝐵))
110	87, 109	eqtr4d 2807	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 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 2814	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 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 824	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 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 824	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 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 4525	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → 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 2804	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → 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 13233	. . . . 5 ⊢ (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 2820	. . . 4 ⊢ (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 13233	. . . 4 ⊢ (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 4506	. . 3 ⊢ -_𝑒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 2822	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → 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 13239	. . 3 ⊢ (𝐴 ∈ ℝ^* → -_𝑒𝐴 ∈ ℝ^*)
122		xmulval 13251	. . 3 ⊢ ((-_𝑒𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (-_𝑒𝐴 ·_e 𝐵) = if((-_𝑒𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵)))))
123	121, 122	sylan 591	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (-_𝑒𝐴 ·_e 𝐵) = if((-_𝑒𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵)))))
124		xmulval 13251	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ·_e 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))))
125		xnegeq 13233	. . 3 ⊢ ((𝐴 ·_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 18	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → -_𝑒(𝐴 ·_e 𝐵) = -_𝑒if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))))
127	120, 123, 126	3eqtr4d 2814	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (-_𝑒𝐴 ·_e 𝐵) = -_𝑒(𝐴 ·_e 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1567 ∈ wcel 2149 ifcif 4492 class class class wbr 5113 (class class class)co 7411 ℝcr 11099 0cc0 11100 · cmul 11105 +∞cpnf 11240 -∞cmnf 11241 ℝ^*cxr 11242 < clt 11243 -cneg 11442 -_𝑒cxne 13134 ·_e cxmu 13136

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-br 5114 df-opab 5178 df-mpt 5197 df-id 5557 df-po 5570 df-so 5571 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-er 8694 df-en 8944 df-dom 8945 df-sdom 8946 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-xneg 13137 df-xmul 13139

This theorem is referenced by: xmulneg2 13296 xmulpnf1n 13304 xmulm1 13307 xmulass 13313 xadddi 13321 xadddi2 13323 xrsmulgzz 33270

W3C validator