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 ‘ 𝐵 ) ) ) )