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 ⊢ ( 𝜑 → ( ( 𝐴 / 𝐵 ) = ( 𝐶 / 𝐷 ) ↔ ( 𝐵 / 𝐴 ) = ( 𝐷 / 𝐶 ) ) )