Metamath Proof Explorer

Theorem sgnmul

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

Ref Expression
Assertion sgnmul ⊢A∈ℝ∧B∈ℝ→sgn⁡A⁢B=sgn⁡A⁢sgn⁡B

Proof

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