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

Proof

Step Hyp Ref Expression
1 0lt1 ⊢0<1
2 breq2 ⊢sgn⁡A⁢B=1→0<sgn⁡A⁢B↔0<1
3 1 2 mpbiri ⊢sgn⁡A⁢B=1→0<sgn⁡A⁢B
4 3 adantl ⊢A∈ℝ∧B∈ℝ∧sgn⁡A⁢B=1→0<sgn⁡A⁢B
5 simplr ⊢A∈ℝ∧B∈ℝ∧0<sgn⁡A⁢B∧sgn⁡A⁢B=−1→0<sgn⁡A⁢B
6 simpr ⊢A∈ℝ∧B∈ℝ∧0<sgn⁡A⁢B∧sgn⁡A⁢B=−1→sgn⁡A⁢B=−1
7 5 6 breqtrd ⊢A∈ℝ∧B∈ℝ∧0<sgn⁡A⁢B∧sgn⁡A⁢B=−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 ⊢A∈ℝ∧B∈ℝ∧0<sgn⁡A⁢B∧sgn⁡A⁢B=−1→¬0<−1
16 7 15 pm2.21dd ⊢A∈ℝ∧B∈ℝ∧0<sgn⁡A⁢B∧sgn⁡A⁢B=−1→sgn⁡A⁢B=1
17 simpr ⊢A∈ℝ∧B∈ℝ∧0<sgn⁡A⁢B∧sgn⁡A⁢B=0→sgn⁡A⁢B=0
18 simplr ⊢A∈ℝ∧B∈ℝ∧0<sgn⁡A⁢B∧sgn⁡A⁢B=0→0<sgn⁡A⁢B
19 18 gt0ne0d ⊢A∈ℝ∧B∈ℝ∧0<sgn⁡A⁢B∧sgn⁡A⁢B=0→sgn⁡A⁢B≠0
20 17 19 pm2.21ddne ⊢A∈ℝ∧B∈ℝ∧0<sgn⁡A⁢B∧sgn⁡A⁢B=0→sgn⁡A⁢B=1
21 simpr ⊢A∈ℝ∧B∈ℝ∧0<sgn⁡A⁢B∧sgn⁡A⁢B=1→sgn⁡A⁢B=1
22 remulcl ⊢A∈ℝ∧B∈ℝ→A⁢B∈ℝ
23 22 rexrd ⊢A∈ℝ∧B∈ℝ→A⁢B∈ℝ*
24 23 adantr ⊢A∈ℝ∧B∈ℝ∧0<sgn⁡A⁢B→A⁢B∈ℝ*
25 sgncl ⊢A⁢B∈ℝ*→sgn⁡A⁢B∈−101
26 eltpi ⊢sgn⁡A⁢B∈−101→sgn⁡A⁢B=−1∨sgn⁡A⁢B=0∨sgn⁡A⁢B=1
27 24 25 26 3syl ⊢A∈ℝ∧B∈ℝ∧0<sgn⁡A⁢B→sgn⁡A⁢B=−1∨sgn⁡A⁢B=0∨sgn⁡A⁢B=1
28 16 20 21 27 mpjao3dan ⊢A∈ℝ∧B∈ℝ∧0<sgn⁡A⁢B→sgn⁡A⁢B=1
29 4 28 impbida ⊢A∈ℝ∧B∈ℝ→sgn⁡A⁢B=1↔0<sgn⁡A⁢B
30 sgnpbi ⊢A⁢B∈ℝ*→sgn⁡A⁢B=1↔0<A⁢B
31 23 30 syl ⊢A∈ℝ∧B∈ℝ→sgn⁡A⁢B=1↔0<A⁢B
32 sgnmul ⊢A∈ℝ∧B∈ℝ→sgn⁡A⁢B=sgn⁡A⁢sgn⁡B
33 32 breq2d ⊢A∈ℝ∧B∈ℝ→0<sgn⁡A⁢B↔0<sgn⁡A⁢sgn⁡B
34 29 31 33 3bitr3d ⊢A∈ℝ∧B∈ℝ→0<A⁢B↔0<sgn⁡A⁢sgn⁡B