sgnmul - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sgnmul		Structured version Visualization version GIF version

Theorem sgnmul 31446

Description: Signum of a product. (Contributed by Thierry Arnoux, 2-Oct-2018.)

**Assertion**
Ref	Expression
sgnmul	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (sgn‘(𝐴 · 𝐵)) = ((sgn‘𝐴) · (sgn‘𝐵)))

**Proof of Theorem sgnmul**
Step	Hyp	Ref	Expression
1		remulcl 10422	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
2	1	rexrd 10492	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ^*)
3		eqeq1 2782	. 2 ⊢ ((sgn‘(𝐴 · 𝐵)) = 0 → ((sgn‘(𝐴 · 𝐵)) = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ 0 = ((sgn‘𝐴) · (sgn‘𝐵))))
4		eqeq1 2782	. 2 ⊢ ((sgn‘(𝐴 · 𝐵)) = 1 → ((sgn‘(𝐴 · 𝐵)) = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ 1 = ((sgn‘𝐴) · (sgn‘𝐵))))
5		eqeq1 2782	. 2 ⊢ ((sgn‘(𝐴 · 𝐵)) = -1 → ((sgn‘(𝐴 · 𝐵)) = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ -1 = ((sgn‘𝐴) · (sgn‘𝐵))))
6		fveq2 6501	. . . . . . 7 ⊢ (𝐴 = 0 → (sgn‘𝐴) = (sgn‘0))
7		sgn0 14312	. . . . . . 7 ⊢ (sgn‘0) = 0
8	6, 7	syl6eq 2830	. . . . . 6 ⊢ (𝐴 = 0 → (sgn‘𝐴) = 0)
9	8	oveq1d 6993	. . . . 5 ⊢ (𝐴 = 0 → ((sgn‘𝐴) · (sgn‘𝐵)) = (0 · (sgn‘𝐵)))
10	9	adantl 474	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) ∧ 𝐴 = 0) → ((sgn‘𝐴) · (sgn‘𝐵)) = (0 · (sgn‘𝐵)))
11		sgnclre 31443	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → (sgn‘𝐵) ∈ ℝ)
12	11	recnd 10470	. . . . . 6 ⊢ (𝐵 ∈ ℝ → (sgn‘𝐵) ∈ ℂ)
13	12	mul02d 10640	. . . . 5 ⊢ (𝐵 ∈ ℝ → (0 · (sgn‘𝐵)) = 0)
14	13	ad3antlr 718	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) ∧ 𝐴 = 0) → (0 · (sgn‘𝐵)) = 0)
15	10, 14	eqtr2d 2815	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) ∧ 𝐴 = 0) → 0 = ((sgn‘𝐴) · (sgn‘𝐵)))
16		fveq2 6501	. . . . . . 7 ⊢ (𝐵 = 0 → (sgn‘𝐵) = (sgn‘0))
17	16, 7	syl6eq 2830	. . . . . 6 ⊢ (𝐵 = 0 → (sgn‘𝐵) = 0)
18	17	oveq2d 6994	. . . . 5 ⊢ (𝐵 = 0 → ((sgn‘𝐴) · (sgn‘𝐵)) = ((sgn‘𝐴) · 0))
19	18	adantl 474	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) ∧ 𝐵 = 0) → ((sgn‘𝐴) · (sgn‘𝐵)) = ((sgn‘𝐴) · 0))
20		sgnclre 31443	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (sgn‘𝐴) ∈ ℝ)
21	20	recnd 10470	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (sgn‘𝐴) ∈ ℂ)
22	21	mul01d 10641	. . . . 5 ⊢ (𝐴 ∈ ℝ → ((sgn‘𝐴) · 0) = 0)
23	22	ad3antrrr 717	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) ∧ 𝐵 = 0) → ((sgn‘𝐴) · 0) = 0)
24	19, 23	eqtr2d 2815	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) ∧ 𝐵 = 0) → 0 = ((sgn‘𝐴) · (sgn‘𝐵)))
25		simpl 475	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈ ℝ)
26	25	recnd 10470	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈ ℂ)
27		simpr 477	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
28	27	recnd 10470	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℂ)
29	26, 28	mul0ord 11093	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0)))
30	29	biimpa 469	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) → (𝐴 = 0 ∨ 𝐵 = 0))
31	15, 24, 30	mpjaodan 941	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) → 0 = ((sgn‘𝐴) · (sgn‘𝐵)))
32		simpll 754	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 𝐴 ∈ ℝ)
33	32	rexrd 10492	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 𝐴 ∈ ℝ^*)
34		oveq1 6985	. . . 4 ⊢ ((sgn‘𝐴) = 0 → ((sgn‘𝐴) · (sgn‘𝐵)) = (0 · (sgn‘𝐵)))
35	34	eqeq2d 2788	. . 3 ⊢ ((sgn‘𝐴) = 0 → (1 = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ 1 = (0 · (sgn‘𝐵))))
36		oveq1 6985	. . . 4 ⊢ ((sgn‘𝐴) = 1 → ((sgn‘𝐴) · (sgn‘𝐵)) = (1 · (sgn‘𝐵)))
37	36	eqeq2d 2788	. . 3 ⊢ ((sgn‘𝐴) = 1 → (1 = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ 1 = (1 · (sgn‘𝐵))))
38		oveq1 6985	. . . 4 ⊢ ((sgn‘𝐴) = -1 → ((sgn‘𝐴) · (sgn‘𝐵)) = (-1 · (sgn‘𝐵)))
39	38	eqeq2d 2788	. . 3 ⊢ ((sgn‘𝐴) = -1 → (1 = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ 1 = (-1 · (sgn‘𝐵))))
40		simpr 477	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 = 0) → 𝐴 = 0)
41	26	adantr 473	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 𝐴 ∈ ℂ)
42	28	adantr 473	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 𝐵 ∈ ℂ)
43		simpr 477	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 0 < (𝐴 · 𝐵))
44	43	gt0ne0d 11007	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → (𝐴 · 𝐵) ≠ 0)
45	41, 42, 44	mulne0bad 11098	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 𝐴 ≠ 0)
46	45	neneqd 2972	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → ¬ 𝐴 = 0)
47	46	adantr 473	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 = 0) → ¬ 𝐴 = 0)
48	40, 47	pm2.21dd 187	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 = 0) → 1 = (0 · (sgn‘𝐵)))
49	27	ad2antrr 713	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 𝐵 ∈ ℝ)
50	49	rexrd 10492	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 𝐵 ∈ ℝ^*)
51		simpll 754	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
52		0red 10445	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 0 ∈ ℝ)
53		simplll 762	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 𝐴 ∈ ℝ)
54		simpr 477	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 0 < 𝐴)
55	52, 53, 54	ltled 10590	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 0 ≤ 𝐴)
56		simplr 756	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 0 < (𝐴 · 𝐵))
57		prodgt0 11290	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐵)
58	51, 55, 56, 57	syl12anc 824	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 0 < 𝐵)
59		sgnp 14313	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 0 < 𝐵) → (sgn‘𝐵) = 1)
60	50, 58, 59	syl2anc 576	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → (sgn‘𝐵) = 1)
61	60	oveq2d 6994	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → (1 · (sgn‘𝐵)) = (1 · 1))
62		1t1e1 11612	. . . 4 ⊢ (1 · 1) = 1
63	61, 62	syl6req 2831	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 1 = (1 · (sgn‘𝐵)))
64	27	ad2antrr 713	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐵 ∈ ℝ)
65	64	rexrd 10492	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐵 ∈ ℝ^*)
66		simplll 762	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐴 ∈ ℝ)
67	66	renegcld 10870	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → -𝐴 ∈ ℝ)
68	64	renegcld 10870	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → -𝐵 ∈ ℝ)
69		0red 10445	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 0 ∈ ℝ)
70		simpr 477	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐴 < 0)
71	25	lt0neg1d 11012	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ 0 < -𝐴))
72	71	ad2antrr 713	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → (𝐴 < 0 ↔ 0 < -𝐴))
73	70, 72	mpbid 224	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 0 < -𝐴)
74	69, 67, 73	ltled 10590	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 0 ≤ -𝐴)
75		simplr 756	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 0 < (𝐴 · 𝐵))
76	26	ad2antrr 713	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐴 ∈ ℂ)
77	28	ad2antrr 713	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐵 ∈ ℂ)
78	76, 77	mul2negd 10898	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → (-𝐴 · -𝐵) = (𝐴 · 𝐵))
79	75, 78	breqtrrd 4958	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 0 < (-𝐴 · -𝐵))
80		prodgt0 11290	. . . . . . . 8 ⊢ (((-𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) ∧ (0 ≤ -𝐴 ∧ 0 < (-𝐴 · -𝐵))) → 0 < -𝐵)
81	67, 68, 74, 79, 80	syl22anc 826	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 0 < -𝐵)
82	27	lt0neg1d 11012	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 < 0 ↔ 0 < -𝐵))
83	82	ad2antrr 713	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → (𝐵 < 0 ↔ 0 < -𝐵))
84	81, 83	mpbird 249	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐵 < 0)
85		sgnn 14317	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 < 0) → (sgn‘𝐵) = -1)
86	65, 84, 85	syl2anc 576	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → (sgn‘𝐵) = -1)
87	86	oveq2d 6994	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → (-1 · (sgn‘𝐵)) = (-1 · -1))
88		neg1mulneg1e1 11663	. . . 4 ⊢ (-1 · -1) = 1
89	87, 88	syl6req 2831	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 1 = (-1 · (sgn‘𝐵)))
90	33, 35, 37, 39, 48, 63, 89	sgn3da 31445	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 1 = ((sgn‘𝐴) · (sgn‘𝐵)))
91		simpll 754	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → 𝐴 ∈ ℝ)
92	91	rexrd 10492	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → 𝐴 ∈ ℝ^*)
93	34	eqeq2d 2788	. . 3 ⊢ ((sgn‘𝐴) = 0 → (-1 = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ -1 = (0 · (sgn‘𝐵))))
94	36	eqeq2d 2788	. . 3 ⊢ ((sgn‘𝐴) = 1 → (-1 = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ -1 = (1 · (sgn‘𝐵))))
95	38	eqeq2d 2788	. . 3 ⊢ ((sgn‘𝐴) = -1 → (-1 = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ -1 = (-1 · (sgn‘𝐵))))
96		simpr 477	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → 𝐴 = 0)
97	26	ad2antrr 713	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → 𝐴 ∈ ℂ)
98	28	ad2antrr 713	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → 𝐵 ∈ ℂ)
99		simplr 756	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → (𝐴 · 𝐵) < 0)
100	99	lt0ne0d 11008	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → (𝐴 · 𝐵) ≠ 0)
101	97, 98, 100	mulne0bad 11098	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → 𝐴 ≠ 0)
102	101	neneqd 2972	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → ¬ 𝐴 = 0)
103	96, 102	pm2.21dd 187	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → -1 = (0 · (sgn‘𝐵)))
104	27	ad2antrr 713	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 0 < 𝐴) → 𝐵 ∈ ℝ)
105	104	rexrd 10492	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 0 < 𝐴) → 𝐵 ∈ ℝ^*)
106		simplr 756	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → 𝐵 ∈ ℝ)
107	26, 28	mulcomd 10463	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
108	107	breq1d 4940	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐵) < 0 ↔ (𝐵 · 𝐴) < 0))
109	108	biimpa 469	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → (𝐵 · 𝐴) < 0)
110	106, 91, 109	mul2lt0rgt0 12312	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 0 < 𝐴) → 𝐵 < 0)
111	105, 110, 85	syl2anc 576	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 0 < 𝐴) → (sgn‘𝐵) = -1)
112	111	oveq2d 6994	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 0 < 𝐴) → (1 · (sgn‘𝐵)) = (1 · -1))
113		neg1cn 11564	. . . . 5 ⊢ -1 ∈ ℂ
114	113	mulid2i 10447	. . . 4 ⊢ (1 · -1) = -1
115	112, 114	syl6req 2831	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 0 < 𝐴) → -1 = (1 · (sgn‘𝐵)))
116	106	adantr 473	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → 𝐵 ∈ ℝ)
117	116	rexrd 10492	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → 𝐵 ∈ ℝ^*)
118	106, 91, 109	mul2lt0rlt0 12311	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → 0 < 𝐵)
119	117, 118, 59	syl2anc 576	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → (sgn‘𝐵) = 1)
120	119	oveq2d 6994	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → (-1 · (sgn‘𝐵)) = (-1 · 1))
121	113	mulid1i 10446	. . . 4 ⊢ (-1 · 1) = -1
122	120, 121	syl6req 2831	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → -1 = (-1 · (sgn‘𝐵)))
123	92, 93, 94, 95, 103, 115, 122	sgn3da 31445	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → -1 = ((sgn‘𝐴) · (sgn‘𝐵)))
124	2, 3, 4, 5, 31, 90, 123	sgn3da 31445	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (sgn‘(𝐴 · 𝐵)) = ((sgn‘𝐴) · (sgn‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 ∨ wo 833 = wceq 1507 ∈ wcel 2050 class class class wbr 4930 ‘cfv 6190 (class class class)co 6978 ℂcc 10335 ℝcr 10336 0cc0 10337 1c1 10338 · cmul 10342 ℝ^*cxr 10475 < clt 10476 ≤ cle 10477 -cneg 10673 sgncsgn 14309

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 ax-cnex 10393 ax-resscn 10394 ax-1cn 10395 ax-icn 10396 ax-addcl 10397 ax-addrcl 10398 ax-mulcl 10399 ax-mulrcl 10400 ax-mulcom 10401 ax-addass 10402 ax-mulass 10403 ax-distr 10404 ax-i2m1 10405 ax-1ne0 10406 ax-1rid 10407 ax-rnegex 10408 ax-rrecex 10409 ax-cnre 10410 ax-pre-lttri 10411 ax-pre-lttrn 10412 ax-pre-ltadd 10413 ax-pre-mulgt0 10414

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rmo 3096 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-tp 4447 df-op 4449 df-uni 4714 df-br 4931 df-opab 4993 df-mpt 5010 df-id 5313 df-po 5327 df-so 5328 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-iota 6154 df-fun 6192 df-fn 6193 df-f 6194 df-f1 6195 df-fo 6196 df-f1o 6197 df-fv 6198 df-riota 6939 df-ov 6981 df-oprab 6982 df-mpo 6983 df-er 8091 df-en 8309 df-dom 8310 df-sdom 8311 df-pnf 10478 df-mnf 10479 df-xr 10480 df-ltxr 10481 df-le 10482 df-sub 10674 df-neg 10675 df-div 11101 df-rp 12208 df-sgn 14310

This theorem is referenced by: sgnmulrp2 31447 sgnmulsgn 31453 sgnmulsgp 31454

W3C validator