![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dvdstrd | Structured version Visualization version GIF version |
Description: The divides relation is transitive, a deduction version of dvdstr 15680. (Contributed by metakunt, 12-May-2024.) |
Ref | Expression |
---|---|
dvdstrd.1 | ⊢ (𝜑 → 𝐾 ∈ ℤ) |
dvdstrd.2 | ⊢ (𝜑 → 𝑀 ∈ ℤ) |
dvdstrd.3 | ⊢ (𝜑 → 𝑁 ∈ ℤ) |
dvdstrd.4 | ⊢ (𝜑 → 𝐾 ∥ 𝑀) |
dvdstrd.5 | ⊢ (𝜑 → 𝑀 ∥ 𝑁) |
Ref | Expression |
---|---|
dvdstrd | ⊢ (𝜑 → 𝐾 ∥ 𝑁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvdstrd.4 | . 2 ⊢ (𝜑 → 𝐾 ∥ 𝑀) | |
2 | dvdstrd.5 | . 2 ⊢ (𝜑 → 𝑀 ∥ 𝑁) | |
3 | dvdstrd.1 | . . 3 ⊢ (𝜑 → 𝐾 ∈ ℤ) | |
4 | dvdstrd.2 | . . 3 ⊢ (𝜑 → 𝑀 ∈ ℤ) | |
5 | dvdstrd.3 | . . 3 ⊢ (𝜑 → 𝑁 ∈ ℤ) | |
6 | dvdstr 15680 | . . 3 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝑀 ∥ 𝑁) → 𝐾 ∥ 𝑁)) | |
7 | 3, 4, 5, 6 | syl3anc 1369 | . 2 ⊢ (𝜑 → ((𝐾 ∥ 𝑀 ∧ 𝑀 ∥ 𝑁) → 𝐾 ∥ 𝑁)) |
8 | 1, 2, 7 | mp2and 699 | 1 ⊢ (𝜑 → 𝐾 ∥ 𝑁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 400 ∈ wcel 2112 class class class wbr 5025 ℤcz 12005 ∥ cdvds 15640 |
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 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-sep 5162 ax-nul 5169 ax-pow 5227 ax-pr 5291 ax-un 7452 ax-resscn 10617 ax-1cn 10618 ax-icn 10619 ax-addcl 10620 ax-addrcl 10621 ax-mulcl 10622 ax-mulrcl 10623 ax-mulcom 10624 ax-addass 10625 ax-mulass 10626 ax-distr 10627 ax-i2m1 10628 ax-1ne0 10629 ax-1rid 10630 ax-rnegex 10631 ax-rrecex 10632 ax-cnre 10633 ax-pre-lttri 10634 ax-pre-lttrn 10635 ax-pre-ltadd 10636 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ne 2950 df-nel 3054 df-ral 3073 df-rex 3074 df-reu 3075 df-rab 3077 df-v 3409 df-sbc 3694 df-csb 3802 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-pss 3873 df-nul 4222 df-if 4414 df-pw 4489 df-sn 4516 df-pr 4518 df-tp 4520 df-op 4522 df-uni 4792 df-iun 4878 df-br 5026 df-opab 5088 df-mpt 5106 df-tr 5132 df-id 5423 df-eprel 5428 df-po 5436 df-so 5437 df-fr 5476 df-we 5478 df-xp 5523 df-rel 5524 df-cnv 5525 df-co 5526 df-dm 5527 df-rn 5528 df-res 5529 df-ima 5530 df-pred 6119 df-ord 6165 df-on 6166 df-lim 6167 df-suc 6168 df-iota 6287 df-fun 6330 df-fn 6331 df-f 6332 df-f1 6333 df-fo 6334 df-f1o 6335 df-fv 6336 df-riota 7101 df-ov 7146 df-oprab 7147 df-mpo 7148 df-om 7573 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-er 8292 df-en 8521 df-dom 8522 df-sdom 8523 df-pnf 10700 df-mnf 10701 df-ltxr 10703 df-sub 10895 df-neg 10896 df-nn 11660 df-n0 11920 df-z 12006 df-dvds 15641 |
This theorem is referenced by: dvdsexp2im 15713 bitsmod 15820 dvdsmulgcd 15941 gcddvdslcm 15983 lcmfunsnlem2lem2 16020 mulgcddvds 16036 rpmulgcd2 16037 rpdvds 16041 isprm5 16088 rpexp 16103 prmdvdsncoprmbd 16107 phimullem 16156 pcpremul 16220 pcdvdstr 16252 pockthlem 16281 4sqlem8 16321 ablfac1eu 19248 znunit 20316 fsumdvdsdiaglem 25852 lgsmod 25991 2sqlem3 26088 2sqlem8 26094 lcmineqlem14 39594 flt4lem2 39961 dvdsacongtr 40283 jm2.20nn 40296 jm2.27a 40304 jm2.27c 40306 |
Copyright terms: Public domain | W3C validator |