Metamath Proof Explorer


Theorem recbothd

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

Ref Expression
Hypotheses recbothd.1 ( 𝜑𝐴 ∈ ℂ )
recbothd.2 ( 𝜑𝐴 ≠ 0 )
recbothd.3 ( 𝜑𝐵 ∈ ℂ )
recbothd.4 ( 𝜑𝐵 ≠ 0 )
recbothd.5 ( 𝜑𝐶 ∈ ℂ )
recbothd.6 ( 𝜑𝐶 ≠ 0 )
recbothd.7 ( 𝜑𝐷 ∈ ℂ )
recbothd.8 ( 𝜑𝐷 ≠ 0 )
Assertion recbothd ( 𝜑 → ( ( 𝐴 / 𝐵 ) = ( 𝐶 / 𝐷 ) ↔ ( 𝐵 / 𝐴 ) = ( 𝐷 / 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 recbothd.1 ( 𝜑𝐴 ∈ ℂ )
2 recbothd.2 ( 𝜑𝐴 ≠ 0 )
3 recbothd.3 ( 𝜑𝐵 ∈ ℂ )
4 recbothd.4 ( 𝜑𝐵 ≠ 0 )
5 recbothd.5 ( 𝜑𝐶 ∈ ℂ )
6 recbothd.6 ( 𝜑𝐶 ≠ 0 )
7 recbothd.7 ( 𝜑𝐷 ∈ ℂ )
8 recbothd.8 ( 𝜑𝐷 ≠ 0 )
9 1 3 4 divcld ( 𝜑 → ( 𝐴 / 𝐵 ) ∈ ℂ )
10 1 3 2 4 divne0d ( 𝜑 → ( 𝐴 / 𝐵 ) ≠ 0 )
11 9 10 jca ( 𝜑 → ( ( 𝐴 / 𝐵 ) ∈ ℂ ∧ ( 𝐴 / 𝐵 ) ≠ 0 ) )
12 5 7 8 divcld ( 𝜑 → ( 𝐶 / 𝐷 ) ∈ ℂ )
13 5 7 6 8 divne0d ( 𝜑 → ( 𝐶 / 𝐷 ) ≠ 0 )
14 12 13 jca ( 𝜑 → ( ( 𝐶 / 𝐷 ) ∈ ℂ ∧ ( 𝐶 / 𝐷 ) ≠ 0 ) )
15 11 14 jca ( 𝜑 → ( ( ( 𝐴 / 𝐵 ) ∈ ℂ ∧ ( 𝐴 / 𝐵 ) ≠ 0 ) ∧ ( ( 𝐶 / 𝐷 ) ∈ ℂ ∧ ( 𝐶 / 𝐷 ) ≠ 0 ) ) )
16 rec11 ( ( ( ( 𝐴 / 𝐵 ) ∈ ℂ ∧ ( 𝐴 / 𝐵 ) ≠ 0 ) ∧ ( ( 𝐶 / 𝐷 ) ∈ ℂ ∧ ( 𝐶 / 𝐷 ) ≠ 0 ) ) → ( ( 1 / ( 𝐴 / 𝐵 ) ) = ( 1 / ( 𝐶 / 𝐷 ) ) ↔ ( 𝐴 / 𝐵 ) = ( 𝐶 / 𝐷 ) ) )
17 15 16 syl ( 𝜑 → ( ( 1 / ( 𝐴 / 𝐵 ) ) = ( 1 / ( 𝐶 / 𝐷 ) ) ↔ ( 𝐴 / 𝐵 ) = ( 𝐶 / 𝐷 ) ) )
18 17 bicomd ( 𝜑 → ( ( 𝐴 / 𝐵 ) = ( 𝐶 / 𝐷 ) ↔ ( 1 / ( 𝐴 / 𝐵 ) ) = ( 1 / ( 𝐶 / 𝐷 ) ) ) )
19 1 3 2 4 recdivd ( 𝜑 → ( 1 / ( 𝐴 / 𝐵 ) ) = ( 𝐵 / 𝐴 ) )
20 5 7 6 8 recdivd ( 𝜑 → ( 1 / ( 𝐶 / 𝐷 ) ) = ( 𝐷 / 𝐶 ) )
21 19 20 eqeq12d ( 𝜑 → ( ( 1 / ( 𝐴 / 𝐵 ) ) = ( 1 / ( 𝐶 / 𝐷 ) ) ↔ ( 𝐵 / 𝐴 ) = ( 𝐷 / 𝐶 ) ) )
22 18 21 bitrd ( 𝜑 → ( ( 𝐴 / 𝐵 ) = ( 𝐶 / 𝐷 ) ↔ ( 𝐵 / 𝐴 ) = ( 𝐷 / 𝐶 ) ) )