Theorem absmulrposd

Description: Specialization of absmuld with absidd . (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	absmulrposd.1	⊢ ( 𝜑 → 0 ≤ 𝐴 )
	absmulrposd.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	absmulrposd.3	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion	absmulrposd	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( abs ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		absmulrposd.1	⊢ ( 𝜑 → 0 ≤ 𝐴 )
2		absmulrposd.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3		absmulrposd.3	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4	2	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
5	3	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
6	4 5	absmuld	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 · 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) )
7	2 1	absidd	⊢ ( 𝜑 → ( abs ‘ 𝐴 ) = 𝐴 )
8	7	oveq1d	⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) = ( 𝐴 · ( abs ‘ 𝐵 ) ) )
9	6 8	eqtrd	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 · 𝐵 ) ) = ( 𝐴 · ( abs ‘ 𝐵 ) ) )