Metamath Proof Explorer


Theorem sgnmulsgn

Description: If two real numbers are of different signs, so are their signs. (Contributed by Thierry Arnoux, 12-Oct-2018)

Ref Expression
Assertion sgnmulsgn ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) < 0 ↔ ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) < 0 ) )

Proof

Step Hyp Ref Expression
1 neg1lt0 - 1 < 0
2 breq1 ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 → ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ↔ - 1 < 0 ) )
3 1 2 mpbiri ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 → ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 )
4 3 adantl ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 )
5 simpr ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 )
6 simpr ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 )
7 simplr ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 )
8 7 lt0ne0d ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) ≠ 0 )
9 6 8 pm2.21ddne ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 )
10 simpr ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 )
11 simplr ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 )
12 10 11 eqbrtrrd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ) → 1 < 0 )
13 1nn0 1 ∈ ℕ0
14 nn0nlt0 ( 1 ∈ ℕ0 → ¬ 1 < 0 )
15 13 14 mp1i ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ) → ¬ 1 < 0 )
16 12 15 pm2.21dd ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 )
17 remulcl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
18 17 rexrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ* )
19 18 adantr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) → ( 𝐴 · 𝐵 ) ∈ ℝ* )
20 sgncl ( ( 𝐴 · 𝐵 ) ∈ ℝ* → ( sgn ‘ ( 𝐴 · 𝐵 ) ) ∈ { - 1 , 0 , 1 } )
21 eltpi ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) ∈ { - 1 , 0 , 1 } → ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ∨ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 ∨ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ) )
22 19 20 21 3syl ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) → ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ∨ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 ∨ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ) )
23 5 9 16 22 mpjao3dan ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 )
24 4 23 impbida ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ↔ ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ) )
25 sgnnbi ( ( 𝐴 · 𝐵 ) ∈ ℝ* → ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ↔ ( 𝐴 · 𝐵 ) < 0 ) )
26 18 25 syl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ↔ ( 𝐴 · 𝐵 ) < 0 ) )
27 sgnmul ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) )
28 27 breq1d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) < 0 ↔ ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) < 0 ) )
29 24 26 28 3bitr3d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) < 0 ↔ ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) < 0 ) )