Theorem absdiv

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

	Ref	Expression
Assertion	absdiv	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( abs ‘ ( 𝐴 / 𝐵 ) ) = ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		divcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℂ )
2		abscl	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℂ → ( abs ‘ ( 𝐴 / 𝐵 ) ) ∈ ℝ )
3	1 2	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( abs ‘ ( 𝐴 / 𝐵 ) ) ∈ ℝ )
4	3	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( abs ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
5		absrpcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( abs ‘ 𝐵 ) ∈ ℝ+ )
6	5	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( abs ‘ 𝐵 ) ∈ ℝ+ )
7	6	rpcnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( abs ‘ 𝐵 ) ∈ ℂ )
8	6	rpne0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( abs ‘ 𝐵 ) ≠ 0 )
9	4 7 8	divcan4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( ( abs ‘ ( 𝐴 / 𝐵 ) ) · ( abs ‘ 𝐵 ) ) / ( abs ‘ 𝐵 ) ) = ( abs ‘ ( 𝐴 / 𝐵 ) ) )
10		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℂ )
11		absmul	⊢ ( ( ( 𝐴 / 𝐵 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( ( 𝐴 / 𝐵 ) · 𝐵 ) ) = ( ( abs ‘ ( 𝐴 / 𝐵 ) ) · ( abs ‘ 𝐵 ) ) )
12	1 10 11	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( abs ‘ ( ( 𝐴 / 𝐵 ) · 𝐵 ) ) = ( ( abs ‘ ( 𝐴 / 𝐵 ) ) · ( abs ‘ 𝐵 ) ) )
13		divcan1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) · 𝐵 ) = 𝐴 )
14	13	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( abs ‘ ( ( 𝐴 / 𝐵 ) · 𝐵 ) ) = ( abs ‘ 𝐴 ) )
15	12 14	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( abs ‘ ( 𝐴 / 𝐵 ) ) · ( abs ‘ 𝐵 ) ) = ( abs ‘ 𝐴 ) )
16	15	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( ( abs ‘ ( 𝐴 / 𝐵 ) ) · ( abs ‘ 𝐵 ) ) / ( abs ‘ 𝐵 ) ) = ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝐵 ) ) )
17	9 16	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( abs ‘ ( 𝐴 / 𝐵 ) ) = ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝐵 ) ) )