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 10322 | . . 3 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))} | |
2 | 1 | ssrab3 4054 | . 2 ⊢ Q ⊆ (N × N) |
3 | 2 | sseli 3960 | 1 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2105 ∀wral 3135 class class class wbr 5057 × cxp 5546 ‘cfv 6348 2nd c2nd 7677 Ncnpi 10254 <N clti 10257 ~Q ceq 10261 Qcnq 10262 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-in 3940 df-ss 3949 df-nq 10322 |
This theorem is referenced by: nqereu 10339 nqerid 10343 enqeq 10344 addpqnq 10348 mulpqnq 10351 ordpinq 10353 addclnq 10355 mulclnq 10357 addnqf 10358 mulnqf 10359 adderpq 10366 mulerpq 10367 addassnq 10368 mulassnq 10369 distrnq 10371 mulidnq 10373 recmulnq 10374 ltsonq 10379 lterpq 10380 ltanq 10381 ltmnq 10382 ltexnq 10385 archnq 10390 wuncn 10580 |
Copyright terms: Public domain | W3C validator |