Metamath Proof Explorer

Theorem sgnmulsgp

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

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

Proof

Step Hyp Ref Expression
1 0lt1 ⊢ 0 < 1
2 breq2 ⊢ ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 → ( 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ↔ 0 < 1 ) )
3 1 2 mpbiri ⊢ ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 → 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) )
4 3 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ) → 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) )
5 simplr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ) → 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) )
6 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 )
7 5 6 breqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ) → 0 < - 1 )
8 1nn0 ⊢ 1 ∈ ℕ0
9 nn0nlt0 ⊢ ( 1 ∈ ℕ0 → ¬ 1 < 0 )
10 8 9 ax-mp ⊢ ¬ 1 < 0
11 1re ⊢ 1 ∈ ℝ
12 lt0neg1 ⊢ ( 1 ∈ ℝ → ( 1 < 0 ↔ 0 < - 1 ) )
13 11 12 ax-mp ⊢ ( 1 < 0 ↔ 0 < - 1 )
14 10 13 mtbi ⊢ ¬ 0 < - 1
15 14 a1i ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ) → ¬ 0 < - 1 )
16 7 15 pm2.21dd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 )
17 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 )
18 simplr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 ) → 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) )
19 18 gt0ne0d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) ≠ 0 )
20 17 19 pm2.21ddne ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 )
21 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) ∧ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 )
22 remulcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
23 22 rexrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ* )
24 23 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) → ( 𝐴 · 𝐵 ) ∈ ℝ* )
25 sgncl ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℝ* → ( sgn ‘ ( 𝐴 · 𝐵 ) ) ∈ { - 1 , 0 , 1 } )
26 eltpi ⊢ ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) ∈ { - 1 , 0 , 1 } → ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ∨ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 ∨ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ) )
27 24 25 26 3syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) → ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = - 1 ∨ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 0 ∨ ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ) )
28 16 20 21 27 mpjao3dan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 )
29 4 28 impbida ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ↔ 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ) )
30 sgnpbi ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℝ* → ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ↔ 0 < ( 𝐴 · 𝐵 ) ) )
31 23 30 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( sgn ‘ ( 𝐴 · 𝐵 ) ) = 1 ↔ 0 < ( 𝐴 · 𝐵 ) ) )
32 sgnmul ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) )
33 32 breq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < ( sgn ‘ ( 𝐴 · 𝐵 ) ) ↔ 0 < ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) ) )
34 29 31 33 3bitr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < ( 𝐴 · 𝐵 ) ↔ 0 < ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) ) )