![]() |
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 10950 | . . 3 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))} | |
2 | 1 | ssrab3 4092 | . 2 ⊢ Q ⊆ (N × N) |
3 | 2 | sseli 3991 | 1 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2106 ∀wral 3059 class class class wbr 5148 × cxp 5687 ‘cfv 6563 2nd c2nd 8012 Ncnpi 10882 <N clti 10885 ~Q ceq 10889 Qcnq 10890 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-rab 3434 df-ss 3980 df-nq 10950 |
This theorem is referenced by: nqereu 10967 nqerid 10971 enqeq 10972 addpqnq 10976 mulpqnq 10979 ordpinq 10981 addclnq 10983 mulclnq 10985 addnqf 10986 mulnqf 10987 adderpq 10994 mulerpq 10995 addassnq 10996 mulassnq 10997 distrnq 10999 mulidnq 11001 recmulnq 11002 ltsonq 11007 lterpq 11008 ltanq 11009 ltmnq 11010 ltexnq 11013 archnq 11018 wuncn 11208 |
Copyright terms: Public domain | W3C validator |