sgnmul

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

		Ref	Expression
	Assertion	sgnmul	$⊢ (A \in ℝ \land B \in ℝ) \to sgn (A B) = sgn (A) sgn (B)$

Proof

Step	Hyp	Ref	Expression
1		remulcl	$⊢ (A \in ℝ \land B \in ℝ) \to A B \in ℝ$
2	1	rexrd	$⊢ (A \in ℝ \land B \in ℝ) \to A B \in ℝ^{*}$
3		eqeq1	$⊢ sgn (A B) = 0 \to (sgn (A B) = sgn (A) sgn (B) \leftrightarrow 0 = sgn (A) sgn (B))$
4		eqeq1	$⊢ sgn (A B) = 1 \to (sgn (A B) = sgn (A) sgn (B) \leftrightarrow 1 = sgn (A) sgn (B))$
5		eqeq1	$⊢ sgn (A B) = - 1 \to (sgn (A B) = sgn (A) sgn (B) \leftrightarrow - 1 = sgn (A) sgn (B))$
6		fveq2	$⊢ A = 0 \to sgn (A) = sgn (0)$
7		sgn0	$⊢ sgn (0) = 0$
8	6 7	eqtrdi	$⊢ A = 0 \to sgn (A) = 0$
9	8	oveq1d	$⊢ A = 0 \to sgn (A) sgn (B) = 0 \cdot sgn (B)$
10	9	adantl	$⊢ (((A \in ℝ \land B \in ℝ) \land A B = 0) \land A = 0) \to sgn (A) sgn (B) = 0 \cdot sgn (B)$
11		sgnclre	$⊢ B \in ℝ \to sgn (B) \in ℝ$
12	11	recnd	$⊢ B \in ℝ \to sgn (B) \in ℂ$
13	12	mul02d	$⊢ B \in ℝ \to 0 \cdot sgn (B) = 0$
14	13	ad3antlr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B = 0) \land A = 0) \to 0 \cdot sgn (B) = 0$
15	10 14	eqtr2d	$⊢ (((A \in ℝ \land B \in ℝ) \land A B = 0) \land A = 0) \to 0 = sgn (A) sgn (B)$
16		fveq2	$⊢ B = 0 \to sgn (B) = sgn (0)$
17	16 7	eqtrdi	$⊢ B = 0 \to sgn (B) = 0$
18	17	oveq2d	$⊢ B = 0 \to sgn (A) sgn (B) = sgn (A) \cdot 0$
19	18	adantl	$⊢ (((A \in ℝ \land B \in ℝ) \land A B = 0) \land B = 0) \to sgn (A) sgn (B) = sgn (A) \cdot 0$
20		sgnclre	$⊢ A \in ℝ \to sgn (A) \in ℝ$
21	20	recnd	$⊢ A \in ℝ \to sgn (A) \in ℂ$
22	21	mul01d	$⊢ A \in ℝ \to sgn (A) \cdot 0 = 0$
23	22	ad3antrrr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B = 0) \land B = 0) \to sgn (A) \cdot 0 = 0$
24	19 23	eqtr2d	$⊢ (((A \in ℝ \land B \in ℝ) \land A B = 0) \land B = 0) \to 0 = sgn (A) sgn (B)$
25		simpl	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℝ$
26	25	recnd	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℂ$
27		simpr	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℝ$
28	27	recnd	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℂ$
29	26 28	mul0ord	$⊢ (A \in ℝ \land B \in ℝ) \to (A B = 0 \leftrightarrow (A = 0 \lor B = 0))$
30	29	biimpa	$⊢ ((A \in ℝ \land B \in ℝ) \land A B = 0) \to (A = 0 \lor B = 0)$
31	15 24 30	mpjaodan	$⊢ ((A \in ℝ \land B \in ℝ) \land A B = 0) \to 0 = sgn (A) sgn (B)$
32		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land 0 < A B) \to A \in ℝ$
33	32	rexrd	$⊢ ((A \in ℝ \land B \in ℝ) \land 0 < A B) \to A \in ℝ^{*}$
34		oveq1	$⊢ sgn (A) = 0 \to sgn (A) sgn (B) = 0 \cdot sgn (B)$
35	34	eqeq2d	$⊢ sgn (A) = 0 \to (1 = sgn (A) sgn (B) \leftrightarrow 1 = 0 \cdot sgn (B))$
36		oveq1	$⊢ sgn (A) = 1 \to sgn (A) sgn (B) = 1 sgn (B)$
37	36	eqeq2d	$⊢ sgn (A) = 1 \to (1 = sgn (A) sgn (B) \leftrightarrow 1 = 1 sgn (B))$
38		oveq1	$⊢ sgn (A) = - 1 \to sgn (A) sgn (B) = -1 sgn (B)$
39	38	eqeq2d	$⊢ sgn (A) = - 1 \to (1 = sgn (A) sgn (B) \leftrightarrow 1 = -1 sgn (B))$
40		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A = 0) \to A = 0$
41	26	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land 0 < A B) \to A \in ℂ$
42	28	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land 0 < A B) \to B \in ℂ$
43		simpr	$⊢ ((A \in ℝ \land B \in ℝ) \land 0 < A B) \to 0 < A B$
44	43	gt0ne0d	$⊢ ((A \in ℝ \land B \in ℝ) \land 0 < A B) \to A B \neq 0$
45	41 42 44	mulne0bad	$⊢ ((A \in ℝ \land B \in ℝ) \land 0 < A B) \to A \neq 0$
46	45	neneqd	$⊢ ((A \in ℝ \land B \in ℝ) \land 0 < A B) \to \neg A = 0$
47	46	adantr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A = 0) \to \neg A = 0$
48	40 47	pm2.21dd	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A = 0) \to 1 = 0 \cdot sgn (B)$
49	27	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land 0 < A) \to B \in ℝ$
50	49	rexrd	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land 0 < A) \to B \in ℝ^{*}$
51		simpll	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land 0 < A) \to (A \in ℝ \land B \in ℝ)$
52		0red	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land 0 < A) \to 0 \in ℝ$
53		simplll	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land 0 < A) \to A \in ℝ$
54		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land 0 < A) \to 0 < A$
55	52 53 54	ltled	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land 0 < A) \to 0 \leq A$
56		simplr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land 0 < A) \to 0 < A B$
57		prodgt0	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land 0 < A B)) \to 0 < B$
58	51 55 56 57	syl12anc	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land 0 < A) \to 0 < B$
59		sgnp	$⊢ (B \in ℝ^{*} \land 0 < B) \to sgn (B) = 1$
60	50 58 59	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land 0 < A) \to sgn (B) = 1$
61	60	oveq2d	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land 0 < A) \to 1 sgn (B) = 1 \cdot 1$
62		1t1e1	$⊢ 1 \cdot 1 = 1$
63	61 62	eqtr2di	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land 0 < A) \to 1 = 1 sgn (B)$
64	27	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to B \in ℝ$
65	64	rexrd	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to B \in ℝ^{*}$
66		simplll	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to A \in ℝ$
67	66	renegcld	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to - A \in ℝ$
68	64	renegcld	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to - B \in ℝ$
69		0red	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to 0 \in ℝ$
70		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to A < 0$
71	25	lt0neg1d	$⊢ (A \in ℝ \land B \in ℝ) \to (A < 0 \leftrightarrow 0 < - A)$
72	71	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to (A < 0 \leftrightarrow 0 < - A)$
73	70 72	mpbid	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to 0 < - A$
74	69 67 73	ltled	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to 0 \leq - A$
75		simplr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to 0 < A B$
76	26	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to A \in ℂ$
77	28	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to B \in ℂ$
78	76 77	mul2negd	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to (- A) (- B) = A B$
79	75 78	breqtrrd	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to 0 < (- A) (- B)$
80		prodgt0	$⊢ ((- A \in ℝ \land - B \in ℝ) \land (0 \leq - A \land 0 < (- A) (- B))) \to 0 < - B$
81	67 68 74 79 80	syl22anc	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to 0 < - B$
82	27	lt0neg1d	$⊢ (A \in ℝ \land B \in ℝ) \to (B < 0 \leftrightarrow 0 < - B)$
83	82	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to (B < 0 \leftrightarrow 0 < - B)$
84	81 83	mpbird	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to B < 0$
85		sgnn	$⊢ (B \in ℝ^{*} \land B < 0) \to sgn (B) = - 1$
86	65 84 85	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to sgn (B) = - 1$
87	86	oveq2d	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to -1 sgn (B) = -1 -1$
88		neg1mulneg1e1	$⊢ -1 -1 = 1$
89	87 88	eqtr2di	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < A B) \land A < 0) \to 1 = -1 sgn (B)$
90	33 35 37 39 48 63 89	sgn3da	$⊢ ((A \in ℝ \land B \in ℝ) \land 0 < A B) \to 1 = sgn (A) sgn (B)$
91		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land A B < 0) \to A \in ℝ$
92	91	rexrd	$⊢ ((A \in ℝ \land B \in ℝ) \land A B < 0) \to A \in ℝ^{*}$
93	34	eqeq2d	$⊢ sgn (A) = 0 \to (- 1 = sgn (A) sgn (B) \leftrightarrow - 1 = 0 \cdot sgn (B))$
94	36	eqeq2d	$⊢ sgn (A) = 1 \to (- 1 = sgn (A) sgn (B) \leftrightarrow - 1 = 1 sgn (B))$
95	38	eqeq2d	$⊢ sgn (A) = - 1 \to (- 1 = sgn (A) sgn (B) \leftrightarrow - 1 = -1 sgn (B))$
96		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to A = 0$
97	26	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to A \in ℂ$
98	28	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to B \in ℂ$
99		simplr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to A B < 0$
100	99	lt0ne0d	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to A B \neq 0$
101	97 98 100	mulne0bad	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to A \neq 0$
102	101	neneqd	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to \neg A = 0$
103	96 102	pm2.21dd	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to - 1 = 0 \cdot sgn (B)$
104	27	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to B \in ℝ$
105	104	rexrd	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to B \in ℝ^{*}$
106		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land A B < 0) \to B \in ℝ$
107	26 28	mulcomd	$⊢ (A \in ℝ \land B \in ℝ) \to A B = B A$
108	107	breq1d	$⊢ (A \in ℝ \land B \in ℝ) \to (A B < 0 \leftrightarrow B A < 0)$
109	108	biimpa	$⊢ ((A \in ℝ \land B \in ℝ) \land A B < 0) \to B A < 0$
110	106 91 109	mul2lt0rgt0	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to B < 0$
111	105 110 85	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to sgn (B) = - 1$
112	111	oveq2d	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to 1 sgn (B) = 1 -1$
113		neg1cn	$⊢ - 1 \in ℂ$
114	113	mulid2i	$⊢ 1 -1 = - 1$
115	112 114	eqtr2di	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to - 1 = 1 sgn (B)$
116	106	adantr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to B \in ℝ$
117	116	rexrd	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to B \in ℝ^{*}$
118	106 91 109	mul2lt0rlt0	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to 0 < B$
119	117 118 59	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to sgn (B) = 1$
120	119	oveq2d	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to -1 sgn (B) = -1 \cdot 1$
121	113	mulid1i	$⊢ -1 \cdot 1 = - 1$
122	120 121	eqtr2di	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to - 1 = -1 sgn (B)$
123	92 93 94 95 103 115 122	sgn3da	$⊢ ((A \in ℝ \land B \in ℝ) \land A B < 0) \to - 1 = sgn (A) sgn (B)$
124	2 3 4 5 31 90 123	sgn3da	$⊢ (A \in ℝ \land B \in ℝ) \to sgn (A B) = sgn (A) sgn (B)$

Metamath Proof Explorer

Theorem sgnmul

Proof