Metamath Proof Explorer

Theorem enqbreq2

Description: Equivalence relation for positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	enqbreq2	\|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ~Q B <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		1st2nd2	\|- ( A e. ( N. X. N. ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
2		1st2nd2	\|- ( B e. ( N. X. N. ) -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. )
3	1 2	breqan12d	\|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ~Q B <-> <. ( 1st ` A ) , ( 2nd ` A ) >. ~Q <. ( 1st ` B ) , ( 2nd ` B ) >. ) )
4		xp1st	\|- ( A e. ( N. X. N. ) -> ( 1st ` A ) e. N. )
5		xp2nd	\|- ( A e. ( N. X. N. ) -> ( 2nd ` A ) e. N. )
6	4 5	jca	\|- ( A e. ( N. X. N. ) -> ( ( 1st ` A ) e. N. /\ ( 2nd ` A ) e. N. ) )
7		xp1st	\|- ( B e. ( N. X. N. ) -> ( 1st ` B ) e. N. )
8		xp2nd	\|- ( B e. ( N. X. N. ) -> ( 2nd ` B ) e. N. )
9	7 8	jca	\|- ( B e. ( N. X. N. ) -> ( ( 1st ` B ) e. N. /\ ( 2nd ` B ) e. N. ) )
10		enqbreq	\|- ( ( ( ( 1st ` A ) e. N. /\ ( 2nd ` A ) e. N. ) /\ ( ( 1st ` B ) e. N. /\ ( 2nd ` B ) e. N. ) ) -> ( <. ( 1st ` A ) , ( 2nd ` A ) >. ~Q <. ( 1st ` B ) , ( 2nd ` B ) >. <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 2nd ` A ) .N ( 1st ` B ) ) ) )
11	6 9 10	syl2an	\|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( <. ( 1st ` A ) , ( 2nd ` A ) >. ~Q <. ( 1st ` B ) , ( 2nd ` B ) >. <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 2nd ` A ) .N ( 1st ` B ) ) ) )
12		mulcompi	\|- ( ( 2nd ` A ) .N ( 1st ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) )
13	12	eqeq2i	\|- ( ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 2nd ` A ) .N ( 1st ` B ) ) <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) )
14	13	a1i	\|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 2nd ` A ) .N ( 1st ` B ) ) <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
15	3 11 14	3bitrd	\|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ~Q B <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )