Metamath Proof Explorer

Theorem sgnmul

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

Ref Expression
Assertion sgnmul 
|- ( ( A e. RR /\ B e. RR ) -> ( sgn ` ( A x. B ) ) = ( ( sgn ` A ) x. ( sgn ` B ) ) )

Proof

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