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→ABC=A⁢CB

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→A1BC=A⁢C1⁢B
5 3 4 mpanl2 ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→A1BC=A⁢C1⁢B
6 5 3impb ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→A1BC=A⁢C1⁢B
7 div1 ⊢A∈ℂ→A1=A
8 7 3ad2ant1 ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→A1=A
9 8 oveq1d ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→A1BC=ABC
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⁢C1⁢B=A⁢CB
14 6 9 13 3eqtr3d ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→ABC=A⁢CB