![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dvdszrcl | Structured version Visualization version GIF version |
Description: Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
Ref | Expression |
---|---|
dvdszrcl | ⊢ (𝑋 ∥ 𝑌 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dvds 16194 | . . 3 ⊢ ∥ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑧 ∈ ℤ (𝑧 · 𝑥) = 𝑦)} | |
2 | opabssxp 5766 | . . 3 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑧 ∈ ℤ (𝑧 · 𝑥) = 𝑦)} ⊆ (ℤ × ℤ) | |
3 | 1, 2 | eqsstri 4015 | . 2 ⊢ ∥ ⊆ (ℤ × ℤ) |
4 | 3 | brel 5739 | 1 ⊢ (𝑋 ∥ 𝑌 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∃wrex 3071 class class class wbr 5147 {copab 5209 × cxp 5673 (class class class)co 7404 · cmul 11111 ℤcz 12554 ∥ cdvds 16193 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5298 ax-nul 5305 ax-pr 5426 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-br 5148 df-opab 5210 df-xp 5681 df-dvds 16194 |
This theorem is referenced by: dvdsmod0 16199 p1modz1 16200 dvdsmodexp 16201 dvdsaddre2b 16246 dvdsabseq 16252 divconjdvds 16254 evenelz 16275 4dvdseven 16312 dfgcd2 16484 dvdsmulgcd 16493 dvdsnprmd 16623 oddvdsi 19409 odmulg 19417 gexdvdsi 19444 dvdszzq 31999 dvdschrmulg 32355 nnproddivdvdsd 40804 lcmineqlem14 40845 nzss 43009 nzin 43010 |
Copyright terms: Public domain | W3C validator |