Metamath Proof Explorer


Theorem enreceq

Description: Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995) (New usage is discouraged.)

Ref Expression
Assertion enreceq
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R = [ <. C , D >. ] ~R <-> ( A +P. D ) = ( B +P. C ) ) )

Proof

Step Hyp Ref Expression
1 enrer
 |-  ~R Er ( P. X. P. )
2 1 a1i
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ~R Er ( P. X. P. ) )
3 opelxpi
 |-  ( ( A e. P. /\ B e. P. ) -> <. A , B >. e. ( P. X. P. ) )
4 3 adantr
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> <. A , B >. e. ( P. X. P. ) )
5 2 4 erth
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( <. A , B >. ~R <. C , D >. <-> [ <. A , B >. ] ~R = [ <. C , D >. ] ~R ) )
6 enrbreq
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( <. A , B >. ~R <. C , D >. <-> ( A +P. D ) = ( B +P. C ) ) )
7 5 6 bitr3d
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R = [ <. C , D >. ] ~R <-> ( A +P. D ) = ( B +P. C ) ) )