Metamath Proof Explorer

Theorem sgnmulsgn

Description: If two real numbers are of different signs, so are their signums. (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 ) )