This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )