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 ⊢A∈ℝ∧B∈ℝ→A⁢B<0↔sgn⁡A⁢sgn⁡B<0

Proof

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