![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dvdsmul1 | Structured version Visualization version GIF version |
Description: An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
Ref | Expression |
---|---|
dvdsmul1 | ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑁)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zcn 11840 | . . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) | |
2 | zcn 11840 | . . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ) | |
3 | mulcom 10476 | . . 3 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝑁 · 𝑀) = (𝑀 · 𝑁)) | |
4 | 1, 2, 3 | syl2anr 596 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 · 𝑀) = (𝑀 · 𝑁)) |
5 | zmulcl 11885 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · 𝑁) ∈ ℤ) | |
6 | dvds0lem 15457 | . . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ (𝑁 · 𝑀) = (𝑀 · 𝑁)) → 𝑀 ∥ (𝑀 · 𝑁)) | |
7 | 6 | ex 413 | . . . 4 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → ((𝑁 · 𝑀) = (𝑀 · 𝑁) → 𝑀 ∥ (𝑀 · 𝑁))) |
8 | 7 | 3com12 1116 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → ((𝑁 · 𝑀) = (𝑀 · 𝑁) → 𝑀 ∥ (𝑀 · 𝑁))) |
9 | 5, 8 | mpd3an3 1454 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 · 𝑀) = (𝑀 · 𝑁) → 𝑀 ∥ (𝑀 · 𝑁))) |
10 | 4, 9 | mpd 15 | 1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑁)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1080 = wceq 1525 ∈ wcel 2083 class class class wbr 4968 (class class class)co 7023 ℂcc 10388 · cmul 10395 ℤcz 11835 ∥ cdvds 15444 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-resscn 10447 ax-1cn 10448 ax-icn 10449 ax-addcl 10450 ax-addrcl 10451 ax-mulcl 10452 ax-mulrcl 10453 ax-mulcom 10454 ax-addass 10455 ax-mulass 10456 ax-distr 10457 ax-i2m1 10458 ax-1ne0 10459 ax-1rid 10460 ax-rnegex 10461 ax-rrecex 10462 ax-cnre 10463 ax-pre-lttri 10464 ax-pre-lttrn 10465 ax-pre-ltadd 10466 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-nel 3093 df-ral 3112 df-rex 3113 df-reu 3114 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-pss 3882 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-tp 4483 df-op 4485 df-uni 4752 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-tr 5071 df-id 5355 df-eprel 5360 df-po 5369 df-so 5370 df-fr 5409 df-we 5411 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-pred 6030 df-ord 6076 df-on 6077 df-lim 6078 df-suc 6079 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-riota 6984 df-ov 7026 df-oprab 7027 df-mpo 7028 df-om 7444 df-wrecs 7805 df-recs 7867 df-rdg 7905 df-er 8146 df-en 8365 df-dom 8366 df-sdom 8367 df-pnf 10530 df-mnf 10531 df-ltxr 10533 df-sub 10725 df-neg 10726 df-nn 11493 df-n0 11752 df-z 11836 df-dvds 15445 |
This theorem is referenced by: dvdsmultr1 15484 3dvdsdec 15518 3dvds2dec 15519 2teven 15541 opoe 15549 omoe 15550 z4even 15560 ndvdsi 15600 bits0e 15615 bits0o 15616 mulgcd 15729 dvdsmulgcd 15738 lcmcllem 15773 lcmgcdlem 15783 qredeq 15834 cncongr2 15845 nprm 15865 exprmfct 15881 prmdiv 15955 iserodd 16005 difsqpwdvds 16056 expnprm 16071 pockthlem 16074 prmreclem3 16087 4sqlem14 16127 odmulg2 18416 odbezout 18419 gexdvds 18443 sylow2alem2 18477 odadd1 18695 odadd2 18696 gexexlem 18699 prmirredlem 20326 znunit 20396 wilthlem2 25332 dvdsflf1o 25450 dvdsmulf1o 25457 ppiublem1 25464 perfectlem1 25491 bposlem3 25548 lgsdir 25594 lgsquadlem1 25642 lgsquad2lem1 25646 lgsquad2lem2 25647 2lgsoddprmlem2 25671 2lgsoddprmlem3 25676 2sqlem4 25683 2sqblem 25693 2sqmod 25698 dchrisumlem1 25751 ex-ind-dvds 27928 jm2.23 39099 jm2.27c 39110 inductionexd 40011 fouriersw 42080 etransclem24 42107 etransclem28 42111 2pwp1prm 43255 m2even 43323 perfectALTVlem1 43390 |
Copyright terms: Public domain | W3C validator |