Metamath Proof Explorer


Theorem pinq

Description: The representatives of positive integers as positive fractions. (Contributed by NM, 29-Oct-1995) (Revised by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

Ref Expression
Assertion pinq A𝑵A1𝑜𝑸

Proof

Step Hyp Ref Expression
1 breq1 x=A1𝑜x~𝑸yA1𝑜~𝑸y
2 fveq2 x=A1𝑜2ndx=2ndA1𝑜
3 2 breq2d x=A1𝑜2ndy<𝑵2ndx2ndy<𝑵2ndA1𝑜
4 3 notbid x=A1𝑜¬2ndy<𝑵2ndx¬2ndy<𝑵2ndA1𝑜
5 1 4 imbi12d x=A1𝑜x~𝑸y¬2ndy<𝑵2ndxA1𝑜~𝑸y¬2ndy<𝑵2ndA1𝑜
6 5 ralbidv x=A1𝑜y𝑵×𝑵x~𝑸y¬2ndy<𝑵2ndxy𝑵×𝑵A1𝑜~𝑸y¬2ndy<𝑵2ndA1𝑜
7 1pi 1𝑜𝑵
8 opelxpi A𝑵1𝑜𝑵A1𝑜𝑵×𝑵
9 7 8 mpan2 A𝑵A1𝑜𝑵×𝑵
10 nlt1pi ¬2ndy<𝑵1𝑜
11 1oex 1𝑜V
12 op2ndg A𝑵1𝑜V2ndA1𝑜=1𝑜
13 11 12 mpan2 A𝑵2ndA1𝑜=1𝑜
14 13 breq2d A𝑵2ndy<𝑵2ndA1𝑜2ndy<𝑵1𝑜
15 10 14 mtbiri A𝑵¬2ndy<𝑵2ndA1𝑜
16 15 a1d A𝑵A1𝑜~𝑸y¬2ndy<𝑵2ndA1𝑜
17 16 ralrimivw A𝑵y𝑵×𝑵A1𝑜~𝑸y¬2ndy<𝑵2ndA1𝑜
18 6 9 17 elrabd A𝑵A1𝑜x𝑵×𝑵|y𝑵×𝑵x~𝑸y¬2ndy<𝑵2ndx
19 df-nq 𝑸=x𝑵×𝑵|y𝑵×𝑵x~𝑸y¬2ndy<𝑵2ndx
20 18 19 eleqtrrdi A𝑵A1𝑜𝑸