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 ( ( ๐ด โˆˆ ( N ร— N ) โˆง ๐ต โˆˆ ( N ร— N ) ) โ†’ ( ๐ด ~Q ๐ต โ†” ( ( 1st โ€˜ ๐ด ) ยทN ( 2nd โ€˜ ๐ต ) ) = ( ( 1st โ€˜ ๐ต ) ยทN ( 2nd โ€˜ ๐ด ) ) ) )

Proof

Step Hyp Ref Expression
1 1st2nd2 โŠข ( ๐ด โˆˆ ( N ร— N ) โ†’ ๐ด = โŸจ ( 1st โ€˜ ๐ด ) , ( 2nd โ€˜ ๐ด ) โŸฉ )
2 1st2nd2 โŠข ( ๐ต โˆˆ ( N ร— N ) โ†’ ๐ต = โŸจ ( 1st โ€˜ ๐ต ) , ( 2nd โ€˜ ๐ต ) โŸฉ )
3 1 2 breqan12d โŠข ( ( ๐ด โˆˆ ( N ร— N ) โˆง ๐ต โˆˆ ( N ร— N ) ) โ†’ ( ๐ด ~Q ๐ต โ†” โŸจ ( 1st โ€˜ ๐ด ) , ( 2nd โ€˜ ๐ด ) โŸฉ ~Q โŸจ ( 1st โ€˜ ๐ต ) , ( 2nd โ€˜ ๐ต ) โŸฉ ) )
4 xp1st โŠข ( ๐ด โˆˆ ( N ร— N ) โ†’ ( 1st โ€˜ ๐ด ) โˆˆ N )
5 xp2nd โŠข ( ๐ด โˆˆ ( N ร— N ) โ†’ ( 2nd โ€˜ ๐ด ) โˆˆ N )
6 4 5 jca โŠข ( ๐ด โˆˆ ( N ร— N ) โ†’ ( ( 1st โ€˜ ๐ด ) โˆˆ N โˆง ( 2nd โ€˜ ๐ด ) โˆˆ N ) )
7 xp1st โŠข ( ๐ต โˆˆ ( N ร— N ) โ†’ ( 1st โ€˜ ๐ต ) โˆˆ N )
8 xp2nd โŠข ( ๐ต โˆˆ ( N ร— N ) โ†’ ( 2nd โ€˜ ๐ต ) โˆˆ N )
9 7 8 jca โŠข ( ๐ต โˆˆ ( N ร— N ) โ†’ ( ( 1st โ€˜ ๐ต ) โˆˆ N โˆง ( 2nd โ€˜ ๐ต ) โˆˆ N ) )
10 enqbreq โŠข ( ( ( ( 1st โ€˜ ๐ด ) โˆˆ N โˆง ( 2nd โ€˜ ๐ด ) โˆˆ N ) โˆง ( ( 1st โ€˜ ๐ต ) โˆˆ N โˆง ( 2nd โ€˜ ๐ต ) โˆˆ N ) ) โ†’ ( โŸจ ( 1st โ€˜ ๐ด ) , ( 2nd โ€˜ ๐ด ) โŸฉ ~Q โŸจ ( 1st โ€˜ ๐ต ) , ( 2nd โ€˜ ๐ต ) โŸฉ โ†” ( ( 1st โ€˜ ๐ด ) ยทN ( 2nd โ€˜ ๐ต ) ) = ( ( 2nd โ€˜ ๐ด ) ยทN ( 1st โ€˜ ๐ต ) ) ) )
11 6 9 10 syl2an โŠข ( ( ๐ด โˆˆ ( N ร— N ) โˆง ๐ต โˆˆ ( N ร— N ) ) โ†’ ( โŸจ ( 1st โ€˜ ๐ด ) , ( 2nd โ€˜ ๐ด ) โŸฉ ~Q โŸจ ( 1st โ€˜ ๐ต ) , ( 2nd โ€˜ ๐ต ) โŸฉ โ†” ( ( 1st โ€˜ ๐ด ) ยทN ( 2nd โ€˜ ๐ต ) ) = ( ( 2nd โ€˜ ๐ด ) ยทN ( 1st โ€˜ ๐ต ) ) ) )
12 mulcompi โŠข ( ( 2nd โ€˜ ๐ด ) ยทN ( 1st โ€˜ ๐ต ) ) = ( ( 1st โ€˜ ๐ต ) ยทN ( 2nd โ€˜ ๐ด ) )
13 12 eqeq2i โŠข ( ( ( 1st โ€˜ ๐ด ) ยทN ( 2nd โ€˜ ๐ต ) ) = ( ( 2nd โ€˜ ๐ด ) ยทN ( 1st โ€˜ ๐ต ) ) โ†” ( ( 1st โ€˜ ๐ด ) ยทN ( 2nd โ€˜ ๐ต ) ) = ( ( 1st โ€˜ ๐ต ) ยทN ( 2nd โ€˜ ๐ด ) ) )
14 13 a1i โŠข ( ( ๐ด โˆˆ ( N ร— N ) โˆง ๐ต โˆˆ ( N ร— N ) ) โ†’ ( ( ( 1st โ€˜ ๐ด ) ยทN ( 2nd โ€˜ ๐ต ) ) = ( ( 2nd โ€˜ ๐ด ) ยทN ( 1st โ€˜ ๐ต ) ) โ†” ( ( 1st โ€˜ ๐ด ) ยทN ( 2nd โ€˜ ๐ต ) ) = ( ( 1st โ€˜ ๐ต ) ยทN ( 2nd โ€˜ ๐ด ) ) ) )
15 3 11 14 3bitrd โŠข ( ( ๐ด โˆˆ ( N ร— N ) โˆง ๐ต โˆˆ ( N ร— N ) ) โ†’ ( ๐ด ~Q ๐ต โ†” ( ( 1st โ€˜ ๐ด ) ยทN ( 2nd โ€˜ ๐ต ) ) = ( ( 1st โ€˜ ๐ต ) ยทN ( 2nd โ€˜ ๐ด ) ) ) )