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 16072 | . . 3 โข โฅ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ โค โง ๐ฆ โ โค) โง โ๐ง โ โค (๐ง ยท ๐ฅ) = ๐ฆ)} | |
2 | opabssxp 5721 | . . 3 โข {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ โค โง ๐ฆ โ โค) โง โ๐ง โ โค (๐ง ยท ๐ฅ) = ๐ฆ)} โ (โค ร โค) | |
3 | 1, 2 | eqsstri 3977 | . 2 โข โฅ โ (โค ร โค) |
4 | 3 | brel 5694 | 1 โข (๐ โฅ ๐ โ (๐ โ โค โง ๐ โ โค)) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 โง wa 397 = wceq 1542 โ wcel 2107 โwrex 3072 class class class wbr 5104 {copab 5166 ร cxp 5629 (class class class)co 7350 ยท cmul 10990 โคcz 12433 โฅ cdvds 16071 |
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 2709 ax-sep 5255 ax-nul 5262 ax-pr 5383 |
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 2716 df-cleq 2730 df-clel 2816 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-sn 4586 df-pr 4588 df-op 4592 df-br 5105 df-opab 5167 df-xp 5637 df-dvds 16072 |
This theorem is referenced by: dvdsmod0 16077 p1modz1 16078 dvdsmodexp 16079 dvdsaddre2b 16124 dvdsabseq 16130 divconjdvds 16132 evenelz 16153 4dvdseven 16190 dfgcd2 16362 dvdsmulgcd 16371 dvdsnprmd 16501 oddvdsi 19262 odmulg 19269 gexdvdsi 19294 dvdszzq 31493 dvdschrmulg 31847 nnproddivdvdsd 40344 lcmineqlem14 40385 nzss 42330 nzin 42331 |
Copyright terms: Public domain | W3C validator |