Metamath Proof Explorer

Theorem absdiv

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

Ref Expression
Assertion absdiv ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = A B

Proof

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