# Metamath Proof Explorer

## Theorem divdiv1

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

Ref Expression
Assertion divdiv1 ${⊢}\left({A}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{\frac{{A}}{{B}}}{{C}}=\frac{{A}}{{B}{C}}$

### Proof

Step Hyp Ref Expression
1 ax-1cn ${⊢}1\in ℂ$
2 ax-1ne0 ${⊢}1\ne 0$
3 1 2 pm3.2i ${⊢}\left(1\in ℂ\wedge 1\ne 0\right)$
4 divdivdiv ${⊢}\left(\left({A}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\wedge \left(\left({C}\in ℂ\wedge {C}\ne 0\right)\wedge \left(1\in ℂ\wedge 1\ne 0\right)\right)\right)\to \frac{\frac{{A}}{{B}}}{\frac{{C}}{1}}=\frac{{A}\cdot 1}{{B}{C}}$
5 3 4 mpanr2 ${⊢}\left(\left({A}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{\frac{{A}}{{B}}}{\frac{{C}}{1}}=\frac{{A}\cdot 1}{{B}{C}}$
6 5 3impa ${⊢}\left({A}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{\frac{{A}}{{B}}}{\frac{{C}}{1}}=\frac{{A}\cdot 1}{{B}{C}}$
7 div1 ${⊢}{C}\in ℂ\to \frac{{C}}{1}={C}$
8 7 oveq2d ${⊢}{C}\in ℂ\to \frac{\frac{{A}}{{B}}}{\frac{{C}}{1}}=\frac{\frac{{A}}{{B}}}{{C}}$
9 8 ad2antrl ${⊢}\left(\left({B}\in ℂ\wedge {B}\ne 0\right)\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{\frac{{A}}{{B}}}{\frac{{C}}{1}}=\frac{\frac{{A}}{{B}}}{{C}}$
10 9 3adant1 ${⊢}\left({A}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{\frac{{A}}{{B}}}{\frac{{C}}{1}}=\frac{\frac{{A}}{{B}}}{{C}}$
11 mulid1 ${⊢}{A}\in ℂ\to {A}\cdot 1={A}$
12 11 oveq1d ${⊢}{A}\in ℂ\to \frac{{A}\cdot 1}{{B}{C}}=\frac{{A}}{{B}{C}}$
13 12 3ad2ant1 ${⊢}\left({A}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{A}\cdot 1}{{B}{C}}=\frac{{A}}{{B}{C}}$
14 6 10 13 3eqtr3d ${⊢}\left({A}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{\frac{{A}}{{B}}}{{C}}=\frac{{A}}{{B}{C}}$