Theorem sgnmulrp2

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

	Ref	Expression
Assertion	sgnmulrp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = ( sgn ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℝ+ )
2	1	rpred	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
3		sgnmul	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) )
4	2 3	syldan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) )
5	1	rpxrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℝ* )
6	1	rpgt0d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 0 < 𝐵 )
7		sgnp	⊢ ( ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) → ( sgn ‘ 𝐵 ) = 1 )
8	5 6 7	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( sgn ‘ 𝐵 ) = 1 )
9	8	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) = ( ( sgn ‘ 𝐴 ) · 1 ) )
10		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
11		sgnclre	⊢ ( 𝐴 ∈ ℝ → ( sgn ‘ 𝐴 ) ∈ ℝ )
12		ax-1rid	⊢ ( ( sgn ‘ 𝐴 ) ∈ ℝ → ( ( sgn ‘ 𝐴 ) · 1 ) = ( sgn ‘ 𝐴 ) )
13	10 11 12	3syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( sgn ‘ 𝐴 ) · 1 ) = ( sgn ‘ 𝐴 ) )
14	4 9 13	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( sgn ‘ ( 𝐴 · 𝐵 ) ) = ( sgn ‘ 𝐴 ) )