Theorem recbothd

Description: Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypotheses	recbothd.1	$$⊢\phi \to A\in ℂ$$
	recbothd.2	$$⊢\phi \to A\ne 0$$
	recbothd.3	$$⊢\phi \to B\in ℂ$$
	recbothd.4	$$⊢\phi \to B\ne 0$$
	recbothd.5	$$⊢\phi \to C\in ℂ$$
	recbothd.6	$$⊢\phi \to C\ne 0$$
	recbothd.7	$$⊢\phi \to D\in ℂ$$
	recbothd.8	$$⊢\phi \to D\ne 0$$
Assertion	recbothd	$$⊢\phi \to \left(\frac{A}{B}=\frac{C}{D}\leftrightarrow \frac{B}{A}=\frac{D}{C}\right)$$

Proof

Step	Hyp	Ref	Expression
1		recbothd.1	$$⊢\phi \to A\in ℂ$$
2		recbothd.2	$$⊢\phi \to A\ne 0$$
3		recbothd.3	$$⊢\phi \to B\in ℂ$$
4		recbothd.4	$$⊢\phi \to B\ne 0$$
5		recbothd.5	$$⊢\phi \to C\in ℂ$$
6		recbothd.6	$$⊢\phi \to C\ne 0$$
7		recbothd.7	$$⊢\phi \to D\in ℂ$$
8		recbothd.8	$$⊢\phi \to D\ne 0$$
9	1 3 4	divcld	$$⊢\phi \to \frac{A}{B}\in ℂ$$
10	1 3 2 4	divne0d	$$⊢\phi \to \frac{A}{B}\ne 0$$
11	9 10	jca	$$⊢\phi \to \left(\frac{A}{B}\in ℂ\wedge \frac{A}{B}\ne 0\right)$$
12	5 7 8	divcld	$$⊢\phi \to \frac{C}{D}\in ℂ$$
13	5 7 6 8	divne0d	$$⊢\phi \to \frac{C}{D}\ne 0$$
14	12 13	jca	$$⊢\phi \to \left(\frac{C}{D}\in ℂ\wedge \frac{C}{D}\ne 0\right)$$
15	11 14	jca	$$⊢\phi \to \left(\left(\frac{A}{B}\in ℂ\wedge \frac{A}{B}\ne 0\right)\wedge \left(\frac{C}{D}\in ℂ\wedge \frac{C}{D}\ne 0\right)\right)$$
16		rec11	$$⊢\left(\left(\frac{A}{B}\in ℂ\wedge \frac{A}{B}\ne 0\right)\wedge \left(\frac{C}{D}\in ℂ\wedge \frac{C}{D}\ne 0\right)\right)\to \left(\frac{1}{\frac{A}{B}}=\frac{1}{\frac{C}{D}}\leftrightarrow \frac{A}{B}=\frac{C}{D}\right)$$
17	15 16	syl	$$⊢\phi \to \left(\frac{1}{\frac{A}{B}}=\frac{1}{\frac{C}{D}}\leftrightarrow \frac{A}{B}=\frac{C}{D}\right)$$
18	17	bicomd	$$⊢\phi \to \left(\frac{A}{B}=\frac{C}{D}\leftrightarrow \frac{1}{\frac{A}{B}}=\frac{1}{\frac{C}{D}}\right)$$
19	1 3 2 4	recdivd	$$⊢\phi \to \frac{1}{\frac{A}{B}}=\frac{B}{A}$$
20	5 7 6 8	recdivd	$$⊢\phi \to \frac{1}{\frac{C}{D}}=\frac{D}{C}$$
21	19 20	eqeq12d	$$⊢\phi \to \left(\frac{1}{\frac{A}{B}}=\frac{1}{\frac{C}{D}}\leftrightarrow \frac{B}{A}=\frac{D}{C}\right)$$
22	18 21	bitrd	$$⊢\phi \to \left(\frac{A}{B}=\frac{C}{D}\leftrightarrow \frac{B}{A}=\frac{D}{C}\right)$$