Metamath Proof Explorer

Theorem recbothd

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

Ref Expression
Hypotheses recbothd.1 
|- ( ph -> A e. CC )
recbothd.2 
|- ( ph -> A =/= 0 )
recbothd.3 
|- ( ph -> B e. CC )
recbothd.4 
|- ( ph -> B =/= 0 )
recbothd.5 
|- ( ph -> C e. CC )
recbothd.6 
|- ( ph -> C =/= 0 )
recbothd.7 
|- ( ph -> D e. CC )
recbothd.8 
|- ( ph -> D =/= 0 )
Assertion recbothd 
|- ( ph -> ( ( A / B ) = ( C / D ) <-> ( B / A ) = ( D / C ) ) )

Proof

Step Hyp Ref Expression
1 recbothd.1 
 |-  ( ph -> A e. CC )
2 recbothd.2 
 |-  ( ph -> A =/= 0 )
3 recbothd.3 
 |-  ( ph -> B e. CC )
4 recbothd.4 
 |-  ( ph -> B =/= 0 )
5 recbothd.5 
 |-  ( ph -> C e. CC )
6 recbothd.6 
 |-  ( ph -> C =/= 0 )
7 recbothd.7 
 |-  ( ph -> D e. CC )
8 recbothd.8 
 |-  ( ph -> D =/= 0 )
9 1 3 4 divcld 
 |-  ( ph -> ( A / B ) e. CC )
10 1 3 2 4 divne0d 
 |-  ( ph -> ( A / B ) =/= 0 )
11 9 10 jca 
 |-  ( ph -> ( ( A / B ) e. CC /\ ( A / B ) =/= 0 ) )
12 5 7 8 divcld 
 |-  ( ph -> ( C / D ) e. CC )
13 5 7 6 8 divne0d 
 |-  ( ph -> ( C / D ) =/= 0 )
14 12 13 jca 
 |-  ( ph -> ( ( C / D ) e. CC /\ ( C / D ) =/= 0 ) )
15 11 14 jca 
 |-  ( ph -> ( ( ( A / B ) e. CC /\ ( A / B ) =/= 0 ) /\ ( ( C / D ) e. CC /\ ( C / D ) =/= 0 ) ) )
16 rec11 
 |-  ( ( ( ( A / B ) e. CC /\ ( A / B ) =/= 0 ) /\ ( ( C / D ) e. CC /\ ( C / D ) =/= 0 ) ) -> ( ( 1 / ( A / B ) ) = ( 1 / ( C / D ) ) <-> ( A / B ) = ( C / D ) ) )
17 15 16 syl 
 |-  ( ph -> ( ( 1 / ( A / B ) ) = ( 1 / ( C / D ) ) <-> ( A / B ) = ( C / D ) ) )
18 17 bicomd 
 |-  ( ph -> ( ( A / B ) = ( C / D ) <-> ( 1 / ( A / B ) ) = ( 1 / ( C / D ) ) ) )
19 1 3 2 4 recdivd 
 |-  ( ph -> ( 1 / ( A / B ) ) = ( B / A ) )
20 5 7 6 8 recdivd 
 |-  ( ph -> ( 1 / ( C / D ) ) = ( D / C ) )
21 19 20 eqeq12d 
 |-  ( ph -> ( ( 1 / ( A / B ) ) = ( 1 / ( C / D ) ) <-> ( B / A ) = ( D / C ) ) )
22 18 21 bitrd 
 |-  ( ph -> ( ( A / B ) = ( C / D ) <-> ( B / A ) = ( D / C ) ) )