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{1B}{1A}$$
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{1B}{1A}$$
8	2 7	eqtr3id	$$⊢\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{1B}{1A}$$
9		mulid2	$$⊢B\in ℂ\to 1B=B$$
10		mulid2	$$⊢A\in ℂ\to 1A=A$$
11	9 10	oveqan12rd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \frac{1B}{1A}=\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{1B}{1A}=\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}$$