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

Metamath Proof Explorer

Theorem divdiv2

Description: Division by a fraction. (Contributed by NM, 27-Dec-2008)

Ref Expression
Assertion divdiv2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A B C = A ⁢ C B

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 ax-1ne0 ⊢ 1 ≠ 0
3 1 2 pm3.2i ⊢ 1 ∈ ℂ ∧ 1 ≠ 0
4 divdivdiv ⊢ A ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A 1 B C = A ⁢ C 1 ⁢ B
5 3 4 mpanl2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A 1 B C = A ⁢ C 1 ⁢ B
6 5 3impb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A 1 B C = A ⁢ C 1 ⁢ B
7 div1 ⊢ A ∈ ℂ → A 1 = A
8 7 3ad2ant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A 1 = A
9 8 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A 1 B C = A B C
10 mullid ⊢ B ∈ ℂ → 1 ⁢ B = B
11 10 ad2antrl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → 1 ⁢ B = B
12 11 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → 1 ⁢ B = B
13 12 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ C 1 ⁢ B = A ⁢ C B
14 6 9 13 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A B C = A ⁢ C B