Metamath Proof Explorer

Theorem sgnmul

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

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

Proof

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