MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordpipq Structured version   Visualization version   GIF version

Theorem ordpipq 10937
Description: Ordering of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
Assertion
Ref Expression
ordpipq (โŸจ๐ด, ๐ตโŸฉ <pQ โŸจ๐ถ, ๐ทโŸฉ โ†” (๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต))

Proof of Theorem ordpipq
Dummy variables ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opex 5465 . . 3 โŸจ๐ด, ๐ตโŸฉ โˆˆ V
2 opex 5465 . . 3 โŸจ๐ถ, ๐ทโŸฉ โˆˆ V
3 eleq1 2822 . . . . . 6 (๐‘ฅ = โŸจ๐ด, ๐ตโŸฉ โ†’ (๐‘ฅ โˆˆ (N ร— N) โ†” โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N)))
43anbi1d 631 . . . . 5 (๐‘ฅ = โŸจ๐ด, ๐ตโŸฉ โ†’ ((๐‘ฅ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N)) โ†” (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N))))
54anbi1d 631 . . . 4 (๐‘ฅ = โŸจ๐ด, ๐ตโŸฉ โ†’ (((๐‘ฅ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N)) โˆง ((1st โ€˜๐‘ฅ) ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN (2nd โ€˜๐‘ฅ))) โ†” ((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N)) โˆง ((1st โ€˜๐‘ฅ) ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN (2nd โ€˜๐‘ฅ)))))
6 fveq2 6892 . . . . . . . 8 (๐‘ฅ = โŸจ๐ด, ๐ตโŸฉ โ†’ (1st โ€˜๐‘ฅ) = (1st โ€˜โŸจ๐ด, ๐ตโŸฉ))
7 opelxp 5713 . . . . . . . . . 10 (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โ†” (๐ด โˆˆ N โˆง ๐ต โˆˆ N))
8 op1stg 7987 . . . . . . . . . 10 ((๐ด โˆˆ N โˆง ๐ต โˆˆ N) โ†’ (1st โ€˜โŸจ๐ด, ๐ตโŸฉ) = ๐ด)
97, 8sylbi 216 . . . . . . . . 9 (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โ†’ (1st โ€˜โŸจ๐ด, ๐ตโŸฉ) = ๐ด)
109adantr 482 . . . . . . . 8 ((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N)) โ†’ (1st โ€˜โŸจ๐ด, ๐ตโŸฉ) = ๐ด)
116, 10sylan9eq 2793 . . . . . . 7 ((๐‘ฅ = โŸจ๐ด, ๐ตโŸฉ โˆง (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N))) โ†’ (1st โ€˜๐‘ฅ) = ๐ด)
1211oveq1d 7424 . . . . . 6 ((๐‘ฅ = โŸจ๐ด, ๐ตโŸฉ โˆง (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N))) โ†’ ((1st โ€˜๐‘ฅ) ยทN (2nd โ€˜๐‘ฆ)) = (๐ด ยทN (2nd โ€˜๐‘ฆ)))
13 fveq2 6892 . . . . . . . 8 (๐‘ฅ = โŸจ๐ด, ๐ตโŸฉ โ†’ (2nd โ€˜๐‘ฅ) = (2nd โ€˜โŸจ๐ด, ๐ตโŸฉ))
14 op2ndg 7988 . . . . . . . . . 10 ((๐ด โˆˆ N โˆง ๐ต โˆˆ N) โ†’ (2nd โ€˜โŸจ๐ด, ๐ตโŸฉ) = ๐ต)
157, 14sylbi 216 . . . . . . . . 9 (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โ†’ (2nd โ€˜โŸจ๐ด, ๐ตโŸฉ) = ๐ต)
1615adantr 482 . . . . . . . 8 ((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N)) โ†’ (2nd โ€˜โŸจ๐ด, ๐ตโŸฉ) = ๐ต)
1713, 16sylan9eq 2793 . . . . . . 7 ((๐‘ฅ = โŸจ๐ด, ๐ตโŸฉ โˆง (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N))) โ†’ (2nd โ€˜๐‘ฅ) = ๐ต)
1817oveq2d 7425 . . . . . 6 ((๐‘ฅ = โŸจ๐ด, ๐ตโŸฉ โˆง (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N))) โ†’ ((1st โ€˜๐‘ฆ) ยทN (2nd โ€˜๐‘ฅ)) = ((1st โ€˜๐‘ฆ) ยทN ๐ต))
1912, 18breq12d 5162 . . . . 5 ((๐‘ฅ = โŸจ๐ด, ๐ตโŸฉ โˆง (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N))) โ†’ (((1st โ€˜๐‘ฅ) ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN (2nd โ€˜๐‘ฅ)) โ†” (๐ด ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN ๐ต)))
2019pm5.32da 580 . . . 4 (๐‘ฅ = โŸจ๐ด, ๐ตโŸฉ โ†’ (((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N)) โˆง ((1st โ€˜๐‘ฅ) ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN (2nd โ€˜๐‘ฅ))) โ†” ((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N)) โˆง (๐ด ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN ๐ต))))
215, 20bitrd 279 . . 3 (๐‘ฅ = โŸจ๐ด, ๐ตโŸฉ โ†’ (((๐‘ฅ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N)) โˆง ((1st โ€˜๐‘ฅ) ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN (2nd โ€˜๐‘ฅ))) โ†” ((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N)) โˆง (๐ด ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN ๐ต))))
22 eleq1 2822 . . . . . 6 (๐‘ฆ = โŸจ๐ถ, ๐ทโŸฉ โ†’ (๐‘ฆ โˆˆ (N ร— N) โ†” โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N)))
2322anbi2d 630 . . . . 5 (๐‘ฆ = โŸจ๐ถ, ๐ทโŸฉ โ†’ ((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N)) โ†” (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N))))
2423anbi1d 631 . . . 4 (๐‘ฆ = โŸจ๐ถ, ๐ทโŸฉ โ†’ (((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N)) โˆง (๐ด ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN ๐ต)) โ†” ((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N)) โˆง (๐ด ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN ๐ต))))
25 fveq2 6892 . . . . . . . 8 (๐‘ฆ = โŸจ๐ถ, ๐ทโŸฉ โ†’ (2nd โ€˜๐‘ฆ) = (2nd โ€˜โŸจ๐ถ, ๐ทโŸฉ))
26 opelxp 5713 . . . . . . . . . 10 (โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N) โ†” (๐ถ โˆˆ N โˆง ๐ท โˆˆ N))
27 op2ndg 7988 . . . . . . . . . 10 ((๐ถ โˆˆ N โˆง ๐ท โˆˆ N) โ†’ (2nd โ€˜โŸจ๐ถ, ๐ทโŸฉ) = ๐ท)
2826, 27sylbi 216 . . . . . . . . 9 (โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N) โ†’ (2nd โ€˜โŸจ๐ถ, ๐ทโŸฉ) = ๐ท)
2928adantl 483 . . . . . . . 8 ((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N)) โ†’ (2nd โ€˜โŸจ๐ถ, ๐ทโŸฉ) = ๐ท)
3025, 29sylan9eq 2793 . . . . . . 7 ((๐‘ฆ = โŸจ๐ถ, ๐ทโŸฉ โˆง (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N))) โ†’ (2nd โ€˜๐‘ฆ) = ๐ท)
3130oveq2d 7425 . . . . . 6 ((๐‘ฆ = โŸจ๐ถ, ๐ทโŸฉ โˆง (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N))) โ†’ (๐ด ยทN (2nd โ€˜๐‘ฆ)) = (๐ด ยทN ๐ท))
32 fveq2 6892 . . . . . . . 8 (๐‘ฆ = โŸจ๐ถ, ๐ทโŸฉ โ†’ (1st โ€˜๐‘ฆ) = (1st โ€˜โŸจ๐ถ, ๐ทโŸฉ))
33 op1stg 7987 . . . . . . . . . 10 ((๐ถ โˆˆ N โˆง ๐ท โˆˆ N) โ†’ (1st โ€˜โŸจ๐ถ, ๐ทโŸฉ) = ๐ถ)
3426, 33sylbi 216 . . . . . . . . 9 (โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N) โ†’ (1st โ€˜โŸจ๐ถ, ๐ทโŸฉ) = ๐ถ)
3534adantl 483 . . . . . . . 8 ((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N)) โ†’ (1st โ€˜โŸจ๐ถ, ๐ทโŸฉ) = ๐ถ)
3632, 35sylan9eq 2793 . . . . . . 7 ((๐‘ฆ = โŸจ๐ถ, ๐ทโŸฉ โˆง (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N))) โ†’ (1st โ€˜๐‘ฆ) = ๐ถ)
3736oveq1d 7424 . . . . . 6 ((๐‘ฆ = โŸจ๐ถ, ๐ทโŸฉ โˆง (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N))) โ†’ ((1st โ€˜๐‘ฆ) ยทN ๐ต) = (๐ถ ยทN ๐ต))
3831, 37breq12d 5162 . . . . 5 ((๐‘ฆ = โŸจ๐ถ, ๐ทโŸฉ โˆง (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N))) โ†’ ((๐ด ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN ๐ต) โ†” (๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต)))
3938pm5.32da 580 . . . 4 (๐‘ฆ = โŸจ๐ถ, ๐ทโŸฉ โ†’ (((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N)) โˆง (๐ด ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN ๐ต)) โ†” ((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N)) โˆง (๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต))))
4024, 39bitrd 279 . . 3 (๐‘ฆ = โŸจ๐ถ, ๐ทโŸฉ โ†’ (((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N)) โˆง (๐ด ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN ๐ต)) โ†” ((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N)) โˆง (๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต))))
41 df-ltpq 10905 . . 3 <pQ = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ (N ร— N) โˆง ๐‘ฆ โˆˆ (N ร— N)) โˆง ((1st โ€˜๐‘ฅ) ยทN (2nd โ€˜๐‘ฆ)) <N ((1st โ€˜๐‘ฆ) ยทN (2nd โ€˜๐‘ฅ)))}
421, 2, 21, 40, 41brab 5544 . 2 (โŸจ๐ด, ๐ตโŸฉ <pQ โŸจ๐ถ, ๐ทโŸฉ โ†” ((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N)) โˆง (๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต)))
43 simpr 486 . . 3 (((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N)) โˆง (๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต)) โ†’ (๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต))
44 ltrelpi 10884 . . . . . 6 <N โŠ† (N ร— N)
4544brel 5742 . . . . 5 ((๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต) โ†’ ((๐ด ยทN ๐ท) โˆˆ N โˆง (๐ถ ยทN ๐ต) โˆˆ N))
46 dmmulpi 10886 . . . . . . 7 dom ยทN = (N ร— N)
47 0npi 10877 . . . . . . 7 ยฌ โˆ… โˆˆ N
4846, 47ndmovrcl 7593 . . . . . 6 ((๐ด ยทN ๐ท) โˆˆ N โ†’ (๐ด โˆˆ N โˆง ๐ท โˆˆ N))
4946, 47ndmovrcl 7593 . . . . . 6 ((๐ถ ยทN ๐ต) โˆˆ N โ†’ (๐ถ โˆˆ N โˆง ๐ต โˆˆ N))
5048, 49anim12i 614 . . . . 5 (((๐ด ยทN ๐ท) โˆˆ N โˆง (๐ถ ยทN ๐ต) โˆˆ N) โ†’ ((๐ด โˆˆ N โˆง ๐ท โˆˆ N) โˆง (๐ถ โˆˆ N โˆง ๐ต โˆˆ N)))
51 opelxpi 5714 . . . . . . 7 ((๐ด โˆˆ N โˆง ๐ต โˆˆ N) โ†’ โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N))
5251ad2ant2rl 748 . . . . . 6 (((๐ด โˆˆ N โˆง ๐ท โˆˆ N) โˆง (๐ถ โˆˆ N โˆง ๐ต โˆˆ N)) โ†’ โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N))
53 simprl 770 . . . . . . 7 (((๐ด โˆˆ N โˆง ๐ท โˆˆ N) โˆง (๐ถ โˆˆ N โˆง ๐ต โˆˆ N)) โ†’ ๐ถ โˆˆ N)
54 simplr 768 . . . . . . 7 (((๐ด โˆˆ N โˆง ๐ท โˆˆ N) โˆง (๐ถ โˆˆ N โˆง ๐ต โˆˆ N)) โ†’ ๐ท โˆˆ N)
5553, 54opelxpd 5716 . . . . . 6 (((๐ด โˆˆ N โˆง ๐ท โˆˆ N) โˆง (๐ถ โˆˆ N โˆง ๐ต โˆˆ N)) โ†’ โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N))
5652, 55jca 513 . . . . 5 (((๐ด โˆˆ N โˆง ๐ท โˆˆ N) โˆง (๐ถ โˆˆ N โˆง ๐ต โˆˆ N)) โ†’ (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N)))
5745, 50, 563syl 18 . . . 4 ((๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต) โ†’ (โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N)))
5857ancri 551 . . 3 ((๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต) โ†’ ((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N)) โˆง (๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต)))
5943, 58impbii 208 . 2 (((โŸจ๐ด, ๐ตโŸฉ โˆˆ (N ร— N) โˆง โŸจ๐ถ, ๐ทโŸฉ โˆˆ (N ร— N)) โˆง (๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต)) โ†” (๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต))
6042, 59bitri 275 1 (โŸจ๐ด, ๐ตโŸฉ <pQ โŸจ๐ถ, ๐ทโŸฉ โ†” (๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต))
Colors of variables: wff setvar class
Syntax hints:   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107  โŸจcop 4635   class class class wbr 5149   ร— cxp 5675  โ€˜cfv 6544  (class class class)co 7409  1st c1st 7973  2nd c2nd 7974  Ncnpi 10839   ยทN cmi 10841   <N clti 10842   <pQ cltpq 10845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-omul 8471  df-ni 10867  df-mi 10869  df-lti 10870  df-ltpq 10905
This theorem is referenced by:  ordpinq  10938  lterpq  10965  ltanq  10966  ltmnq  10967  1lt2nq  10968
  Copyright terms: Public domain W3C validator