![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elpqn | Structured version Visualization version GIF version |
Description: Each positive fraction is an ordered pair of positive integers (the numerator and denominator, in "lowest terms". (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
Ref | Expression |
---|---|
elpqn | ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nq 10937 | . . 3 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))} | |
2 | 1 | ssrab3 4076 | . 2 ⊢ Q ⊆ (N × N) |
3 | 2 | sseli 3972 | 1 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2098 ∀wral 3050 class class class wbr 5149 × cxp 5676 ‘cfv 6549 2nd c2nd 7993 Ncnpi 10869 <N clti 10872 ~Q ceq 10876 Qcnq 10877 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-ss 3961 df-nq 10937 |
This theorem is referenced by: nqereu 10954 nqerid 10958 enqeq 10959 addpqnq 10963 mulpqnq 10966 ordpinq 10968 addclnq 10970 mulclnq 10972 addnqf 10973 mulnqf 10974 adderpq 10981 mulerpq 10982 addassnq 10983 mulassnq 10984 distrnq 10986 mulidnq 10988 recmulnq 10989 ltsonq 10994 lterpq 10995 ltanq 10996 ltmnq 10997 ltexnq 11000 archnq 11005 wuncn 11195 |
Copyright terms: Public domain | W3C validator |