# Metamath Proof Explorer

## Theorem recdiv

Description: The reciprocal of a ratio. (Contributed by NM, 3-Aug-2004)

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

### Proof

Step Hyp Ref Expression
1 1div1e1 ${⊢}\frac{1}{1}=1$
2 1 oveq1i ${⊢}\frac{\frac{1}{1}}{\frac{{A}}{{B}}}=\frac{1}{\frac{{A}}{{B}}}$
3 ax-1cn ${⊢}1\in ℂ$
4 ax-1ne0 ${⊢}1\ne 0$
5 3 4 pm3.2i ${⊢}\left(1\in ℂ\wedge 1\ne 0\right)$
6 divdivdiv ${⊢}\left(\left(1\in ℂ\wedge \left(1\in ℂ\wedge 1\ne 0\right)\right)\wedge \left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\right)\to \frac{\frac{1}{1}}{\frac{{A}}{{B}}}=\frac{1{B}}{1{A}}$
7 3 5 6 mpanl12 ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \frac{\frac{1}{1}}{\frac{{A}}{{B}}}=\frac{1{B}}{1{A}}$
8 2 7 syl5eqr ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \frac{1}{\frac{{A}}{{B}}}=\frac{1{B}}{1{A}}$
9 mulid2 ${⊢}{B}\in ℂ\to 1{B}={B}$
10 mulid2 ${⊢}{A}\in ℂ\to 1{A}={A}$
11 9 10 oveqan12rd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \frac{1{B}}{1{A}}=\frac{{B}}{{A}}$
12 11 ad2ant2r ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \frac{1{B}}{1{A}}=\frac{{B}}{{A}}$
13 8 12 eqtrd ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \frac{1}{\frac{{A}}{{B}}}=\frac{{B}}{{A}}$