Theorem sgnmulrp2

Description: Multiplication by a positive number does not affect signum. (Contributed by Thierry Arnoux, 2-Oct-2018)

	Ref	Expression
Assertion	sgnmulrp2	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \mathrm{sgn}\left(AB\right)=\mathrm{sgn}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B\in {ℝ}^{+}$$
2	1	rpred	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B\in ℝ$$
3		sgnmul	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \mathrm{sgn}\left(AB\right)=\mathrm{sgn}\left(A\right)\mathrm{sgn}\left(B\right)$$
4	2 3	syldan	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \mathrm{sgn}\left(AB\right)=\mathrm{sgn}\left(A\right)\mathrm{sgn}\left(B\right)$$
5	1	rpxrd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to B\in {ℝ}^{*}$$
6	1	rpgt0d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to 0<B$$
7		sgnp	$$⊢\left(B\in {ℝ}^{*}\wedge 0<B\right)\to \mathrm{sgn}\left(B\right)=1$$
8	5 6 7	syl2anc	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \mathrm{sgn}\left(B\right)=1$$
9	8	oveq2d	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \mathrm{sgn}\left(A\right)\mathrm{sgn}\left(B\right)=\mathrm{sgn}\left(A\right)\cdot 1$$
10		simpl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to A\in ℝ$$
11		sgnclre	$$⊢A\in ℝ\to \mathrm{sgn}\left(A\right)\in ℝ$$
12		ax-1rid	$$⊢\mathrm{sgn}\left(A\right)\in ℝ\to \mathrm{sgn}\left(A\right)\cdot 1=\mathrm{sgn}\left(A\right)$$
13	10 11 12	3syl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \mathrm{sgn}\left(A\right)\cdot 1=\mathrm{sgn}\left(A\right)$$
14	4 9 13	3eqtrd	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \mathrm{sgn}\left(AB\right)=\mathrm{sgn}\left(A\right)$$