![]() |
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 10069 | . . 3 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))} | |
2 | 1 | ssrab3 3909 | . 2 ⊢ Q ⊆ (N × N) |
3 | 2 | sseli 3817 | 1 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2107 ∀wral 3090 class class class wbr 4886 × cxp 5353 ‘cfv 6135 2nd c2nd 7444 Ncnpi 10001 <N clti 10004 ~Q ceq 10008 Qcnq 10009 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rab 3099 df-in 3799 df-ss 3806 df-nq 10069 |
This theorem is referenced by: nqereu 10086 nqerid 10090 enqeq 10091 addpqnq 10095 mulpqnq 10098 ordpinq 10100 addclnq 10102 mulclnq 10104 addnqf 10105 mulnqf 10106 adderpq 10113 mulerpq 10114 addassnq 10115 mulassnq 10116 distrnq 10118 mulidnq 10120 recmulnq 10121 ltsonq 10126 lterpq 10127 ltanq 10128 ltmnq 10129 ltexnq 10132 archnq 10137 wuncn 10327 |
Copyright terms: Public domain | W3C validator |