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 16071 | . . 3 โข โฅ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ โค โง ๐ฆ โ โค) โง โ๐ง โ โค (๐ง ยท ๐ฅ) = ๐ฆ)} | |
2 | opabssxp 5720 | . . 3 โข {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ โค โง ๐ฆ โ โค) โง โ๐ง โ โค (๐ง ยท ๐ฅ) = ๐ฆ)} โ (โค ร โค) | |
3 | 1, 2 | eqsstri 3976 | . 2 โข โฅ โ (โค ร โค) |
4 | 3 | brel 5693 | 1 โข (๐ โฅ ๐ โ (๐ โ โค โง ๐ โ โค)) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 โง wa 396 = wceq 1541 โ wcel 2106 โwrex 3071 class class class wbr 5103 {copab 5165 ร cxp 5628 (class class class)co 7349 ยท cmul 10989 โคcz 12432 โฅ cdvds 16070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-opab 5166 df-xp 5636 df-dvds 16071 |
This theorem is referenced by: dvdsmod0 16076 p1modz1 16077 dvdsmodexp 16078 dvdsaddre2b 16123 dvdsabseq 16129 divconjdvds 16131 evenelz 16152 4dvdseven 16189 dfgcd2 16361 dvdsmulgcd 16370 dvdsnprmd 16500 oddvdsi 19262 odmulg 19269 gexdvdsi 19294 dvdszzq 31505 dvdschrmulg 31859 nnproddivdvdsd 40353 lcmineqlem14 40394 nzss 42361 nzin 42362 |
Copyright terms: Public domain | W3C validator |