Metamath Proof Explorer

Theorem divdiv1

Description: Division into a fraction. (Contributed by NM, 31-Dec-2007)

Ref Expression
Assertion divdiv1 ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→ABC=AB⁢C

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∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0∧1∈ℂ∧1≠0→ABC1=A⋅1B⁢C
5 3 4 mpanr2 ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→ABC1=A⋅1B⁢C
6 5 3impa ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→ABC1=A⋅1B⁢C
7 div1 ⊢C∈ℂ→C1=C
8 7 oveq2d ⊢C∈ℂ→ABC1=ABC
9 8 ad2antrl ⊢B∈ℂ∧B≠0∧C∈ℂ∧C≠0→ABC1=ABC
10 9 3adant1 ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→ABC1=ABC
11 mulrid ⊢A∈ℂ→A⋅1=A
12 11 oveq1d ⊢A∈ℂ→A⋅1B⁢C=AB⁢C
13 12 3ad2ant1 ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→A⋅1B⁢C=AB⁢C
14 6 10 13 3eqtr3d ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→ABC=AB⁢C