This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐵 ) ) )