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 13331

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

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

**Proof of Theorem xmulneg1**
Step	Hyp	Ref	Expression
1		xneg0 13274	. . . . . . . . 9 ⊢ -_𝑒0 = 0
2	1	eqeq2i 2753	. . . . . . . 8 ⊢ (-_𝑒𝐴 = -_𝑒0 ↔ -_𝑒𝐴 = 0)
3		0xr 11337	. . . . . . . . 9 ⊢ 0 ∈ ℝ^*
4		xneg11 13277	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 0 ∈ ℝ^*) → (-_𝑒𝐴 = -_𝑒0 ↔ 𝐴 = 0))
5	3, 4	mpan2 690	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ^* → (-_𝑒𝐴 = -_𝑒0 ↔ 𝐴 = 0))
6	2, 5	bitr3id 285	. . . . . . 7 ⊢ (𝐴 ∈ ℝ^* → (-_𝑒𝐴 = 0 ↔ 𝐴 = 0))
7	6	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (-_𝑒𝐴 = 0 ↔ 𝐴 = 0))
8	7	orbi1d 915	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((-_𝑒𝐴 = 0 ∨ 𝐵 = 0) ↔ (𝐴 = 0 ∨ 𝐵 = 0)))
9	8	ifbid 4571	. . . 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 13271	. . . . . . . . . . . . . 14 ⊢ -_𝑒+∞ = -∞
11	10	eqeq2i 2753	. . . . . . . . . . . . 13 ⊢ (-_𝑒𝐴 = -_𝑒+∞ ↔ -_𝑒𝐴 = -∞)
12		simpll 766	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → 𝐴 ∈ ℝ^)
13		pnfxr 11344	. . . . . . . . . . . . . 14 ⊢ +∞ ∈ ℝ^*
14		xneg11 13277	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (-_𝑒𝐴 = -_𝑒+∞ ↔ 𝐴 = +∞))
15	12, 13, 14	sylancl 585	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (-_𝑒𝐴 = -_𝑒+∞ ↔ 𝐴 = +∞))
16	11, 15	bitr3id 285	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (-_𝑒𝐴 = -∞ ↔ 𝐴 = +∞))
17	16	anbi2d 629	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ↔ (0 < 𝐵 ∧ 𝐴 = +∞)))
18		xnegmnf 13272	. . . . . . . . . . . . . 14 ⊢ -_𝑒-∞ = +∞
19	18	eqeq2i 2753	. . . . . . . . . . . . 13 ⊢ (-_𝑒𝐴 = -_𝑒-∞ ↔ -_𝑒𝐴 = +∞)
20		mnfxr 11347	. . . . . . . . . . . . . 14 ⊢ -∞ ∈ ℝ^*
21		xneg11 13277	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ -∞ ∈ ℝ^*) → (-_𝑒𝐴 = -_𝑒-∞ ↔ 𝐴 = -∞))
22	12, 20, 21	sylancl 585	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (-_𝑒𝐴 = -_𝑒-∞ ↔ 𝐴 = -∞))
23	19, 22	bitr3id 285	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (-_𝑒𝐴 = +∞ ↔ 𝐴 = -∞))
24	23	anbi2d 629	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((𝐵 < 0 ∧ -_𝑒𝐴 = +∞) ↔ (𝐵 < 0 ∧ 𝐴 = -∞)))
25	17, 24	orbi12d 917	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ↔ ((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞))))
26		xlt0neg1 13281	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℝ^* → (𝐴 < 0 ↔ 0 < -_𝑒𝐴))
27	26	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (𝐴 < 0 ↔ 0 < -_𝑒𝐴))
28	27	bicomd 223	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (0 < -_𝑒𝐴 ↔ 𝐴 < 0))
29	28	anbi1d 630	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ↔ (𝐴 < 0 ∧ 𝐵 = -∞)))
30		xlt0neg2 13282	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℝ^* → (0 < 𝐴 ↔ -_𝑒𝐴 < 0))
31	30	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (0 < 𝐴 ↔ -_𝑒𝐴 < 0))
32	31	bicomd 223	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (-_𝑒𝐴 < 0 ↔ 0 < 𝐴))
33	32	anbi1d 630	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((-_𝑒𝐴 < 0 ∧ 𝐵 = +∞) ↔ (0 < 𝐴 ∧ 𝐵 = +∞)))
34	29, 33	orbi12d 917	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞)) ↔ ((𝐴 < 0 ∧ 𝐵 = -∞) ∨ (0 < 𝐴 ∧ 𝐵 = +∞))))
35		orcom 869	. . . . . . . . . . 11 ⊢ (((𝐴 < 0 ∧ 𝐵 = -∞) ∨ (0 < 𝐴 ∧ 𝐵 = +∞)) ↔ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))
36	34, 35	bitrdi 287	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞)) ↔ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))))
37	25, 36	orbi12d 917	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))) ↔ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))))
38	37	biimpar 477	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → (((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))))
39	38	iftrued 4556	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵)) = -∞)
40		xmullem2 13327	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))))
41	40	adantr 480	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))))
42	23	anbi2d 629	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ↔ (0 < 𝐵 ∧ 𝐴 = -∞)))
43	16	anbi2d 629	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((𝐵 < 0 ∧ -_𝑒𝐴 = -∞) ↔ (𝐵 < 0 ∧ 𝐴 = +∞)))
44	42, 43	orbi12d 917	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ↔ ((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞))))
45	28	anbi1d 630	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ↔ (𝐴 < 0 ∧ 𝐵 = +∞)))
46	32	anbi1d 630	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((-_𝑒𝐴 < 0 ∧ 𝐵 = -∞) ↔ (0 < 𝐴 ∧ 𝐵 = -∞)))
47	45, 46	orbi12d 917	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞)) ↔ ((𝐴 < 0 ∧ 𝐵 = +∞) ∨ (0 < 𝐴 ∧ 𝐵 = -∞))))
48		orcom 869	. . . . . . . . . . . . 13 ⊢ (((𝐴 < 0 ∧ 𝐵 = +∞) ∨ (0 < 𝐴 ∧ 𝐵 = -∞)) ↔ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))
49	47, 48	bitrdi 287	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞)) ↔ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))))
50	44, 49	orbi12d 917	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))) ↔ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))))
51	50	notbid 318	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))) ↔ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))))
52	41, 51	sylibrd 259	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞)))))
53	52	imp 406	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → ¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))))
54	53	iffalsed 4559	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → if((((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵))) = if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵)))
55		iftrue 4554	. . . . . . . . . 10 ⊢ ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = +∞)
56	55	adantl 481	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = +∞)
57		xnegeq 13269	. . . . . . . . 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 17	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → -_𝑒if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -_𝑒+∞)
59	58, 10	eqtrdi 2796	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → -_𝑒if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -∞)
60	39, 54, 59	3eqtr4d 2790	. . . . . 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 477	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))))
62	61	iftrued 4556	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵))) = +∞)
63	41	con2d 134	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → ((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) → ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))))
64	63	imp 406	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))))
65	64	iffalsed 4559	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))
66		iftrue 4554	. . . . . . . . . . . . 13 ⊢ ((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) → if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)) = -∞)
67	66	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)) = -∞)
68	65, 67	eqtrd 2780	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -∞)
69		xnegeq 13269	. . . . . . . . . . 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 17	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → -_𝑒if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -_𝑒-∞)
71	70, 18	eqtrdi 2796	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → -_𝑒if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = +∞)
72	62, 71	eqtr4d 2783	. . . . . . . 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 714	. . . . . . 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 318	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) → (¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))) ↔ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))))
75	74	biimpar 477	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) → ¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))))
76	75	adantr 480	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → ¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))))
77	76	iffalsed 4559	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵)) = (-_𝑒𝐴 · 𝐵))
78	51	biimpar 477	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → ¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))))
79	78	adantlr 714	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → ¬ (((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))))
80	79	iffalsed 4559	. . . . . . . 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 4557	. . . . . . . . . . . 12 ⊢ (¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))
82	81	ad2antlr 726	. . . . . . . . . . 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 4557	. . . . . . . . . . . 12 ⊢ (¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) → if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)) = (𝐴 · 𝐵))
84	83	adantl 481	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)) = (𝐴 · 𝐵))
85	82, 84	eqtrd 2780	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = (𝐴 · 𝐵))
86		xnegeq 13269	. . . . . . . . . 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 17	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → -_𝑒if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵))) = -_𝑒(𝐴 · 𝐵))
88		xmullem 13326	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐴 ∈ ℝ)
89	88	recnd 11318	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐴 ∈ ℂ)
90		ancom 460	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ↔ (𝐵 ∈ ℝ^ ∧ 𝐴 ∈ ℝ^*))
91		orcom 869	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 = 0 ∨ 𝐵 = 0) ↔ (𝐵 = 0 ∨ 𝐴 = 0))
92	91	notbii 320	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝐴 = 0 ∨ 𝐵 = 0) ↔ ¬ (𝐵 = 0 ∨ 𝐴 = 0))
93	90, 92	anbi12i 627	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ↔ ((𝐵 ∈ ℝ^ ∧ 𝐴 ∈ ℝ^*) ∧ ¬ (𝐵 = 0 ∨ 𝐴 = 0)))
94		orcom 869	. . . . . . . . . . . . . . 15 ⊢ ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) ↔ (((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞))))
95	94	notbii 320	. . . . . . . . . . . . . 14 ⊢ (¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) ↔ ¬ (((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞))))
96	93, 95	anbi12i 627	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ↔ (((𝐵 ∈ ℝ^ ∧ 𝐴 ∈ ℝ^*) ∧ ¬ (𝐵 = 0 ∨ 𝐴 = 0)) ∧ ¬ (((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)))))
97		orcom 869	. . . . . . . . . . . . . 14 ⊢ ((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) ↔ (((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞))))
98	97	notbii 320	. . . . . . . . . . . . 13 ⊢ (¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))) ↔ ¬ (((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞))))
99		xmullem 13326	. . . . . . . . . . . . 13 ⊢ (((((𝐵 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^*) ∧ ¬ (𝐵 = 0 ∨ 𝐴 = 0)) ∧ ¬ (((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)))) ∧ ¬ (((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)) ∨ ((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)))) → 𝐵 ∈ ℝ)
100	96, 98, 99	syl2anb 597	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐵 ∈ ℝ)
101	100	recnd 11318	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐵 ∈ ℂ)
102	89, 101	mulneg1d 11743	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → (-𝐴 · 𝐵) = -(𝐴 · 𝐵))
103		rexneg 13273	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 = -𝐴)
104	88, 103	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → -_𝑒𝐴 = -𝐴)
105	104	oveq1d 7463	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → (-_𝑒𝐴 · 𝐵) = (-𝐴 · 𝐵))
106	88, 100	remulcld 11320	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → (𝐴 · 𝐵) ∈ ℝ)
107		rexneg 13273	. . . . . . . . . . 11 ⊢ ((𝐴 · 𝐵) ∈ ℝ → -_𝑒(𝐴 · 𝐵) = -(𝐴 · 𝐵))
108	106, 107	syl 17	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → -_𝑒(𝐴 · 𝐵) = -(𝐴 · 𝐵))
109	102, 105, 108	3eqtr4d 2790	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → (-_𝑒𝐴 · 𝐵) = -_𝑒(𝐴 · 𝐵))
110	87, 109	eqtr4d 2783	. . . . . . . 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 2790	. . . . . . 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 812	. . . . . 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 812	. . . . 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 4580	. . . 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 2780	. . 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 13269	. . . . 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 2796	. . . 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 13269	. . . 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 4561	. . 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 2798	. 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 13275	. . 3 ⊢ (𝐴 ∈ ℝ^* → -_𝑒𝐴 ∈ ℝ^*)
122		xmulval 13287	. . 3 ⊢ ((-_𝑒𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (-_𝑒𝐴 ·_e 𝐵) = if((-_𝑒𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵)))))
123	121, 122	sylan 579	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (-_𝑒𝐴 ·_e 𝐵) = if((-_𝑒𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ -_𝑒𝐴 = +∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = -∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = +∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ -_𝑒𝐴 = -∞) ∨ (𝐵 < 0 ∧ -_𝑒𝐴 = +∞)) ∨ ((0 < -_𝑒𝐴 ∧ 𝐵 = -∞) ∨ (-_𝑒𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (-_𝑒𝐴 · 𝐵)))))
124		xmulval 13287	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ·_e 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))))
125		xnegeq 13269	. . 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 17	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → -_𝑒(𝐴 ·_e 𝐵) = -_𝑒if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))))
127	120, 123, 126	3eqtr4d 2790	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (-_𝑒𝐴 ·_e 𝐵) = -_𝑒(𝐴 ·_e 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 846 = wceq 1537 ∈ wcel 2108 ifcif 4548 class class class wbr 5166 (class class class)co 7448 ℝcr 11183 0cc0 11184 · cmul 11189 +∞cpnf 11321 -∞cmnf 11322 ℝ^*cxr 11323 < clt 11324 -cneg 11521 -_𝑒cxne 13172 ·_e cxmu 13174

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-po 5607 df-so 5608 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-er 8763 df-en 9004 df-dom 9005 df-sdom 9006 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-xneg 13175 df-xmul 13177

This theorem is referenced by: xmulneg2 13332 xmulpnf1n 13340 xmulm1 13343 xmulass 13349 xadddi 13357 xadddi2 13359 xrsmulgzz 32992

W3C validator