Theorem absdivzi

Description: Absolute value distributes over division. (Contributed by NM, 26-Mar-2005)

	Ref	Expression
Hypotheses	absvalsqi.1	⊢ 𝐴 ∈ ℂ
	abssub.2	⊢ 𝐵 ∈ ℂ
Assertion	absdivzi	⊢ ( 𝐵 ≠ 0 → ( abs ‘ ( 𝐴 / 𝐵 ) ) = ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		absvalsqi.1	⊢ 𝐴 ∈ ℂ
2		abssub.2	⊢ 𝐵 ∈ ℂ
3		absdiv	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( abs ‘ ( 𝐴 / 𝐵 ) ) = ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝐵 ) ) )
4	1 2 3	mp3an12	⊢ ( 𝐵 ≠ 0 → ( abs ‘ ( 𝐴 / 𝐵 ) ) = ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝐵 ) ) )