| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > dvds0 | Structured version Visualization version GIF version | ||
| Description: Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
| Ref | Expression |
|---|---|
| dvds0 | ⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 0) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zcn 12595 | . . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) | |
| 2 | 1 | mul02d 11407 | . 2 ⊢ (𝑁 ∈ ℤ → (0 · 𝑁) = 0) |
| 3 | 0z 12601 | . . 3 ⊢ 0 ∈ ℤ | |
| 4 | dvds0lem 16323 | . . . 4 ⊢ (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 0 ∈ ℤ) ∧ (0 · 𝑁) = 0) → 𝑁 ∥ 0) | |
| 5 | 4 | ex 417 | . . 3 ⊢ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → ((0 · 𝑁) = 0 → 𝑁 ∥ 0)) |
| 6 | 3, 3, 5 | mp3an13 1479 | . 2 ⊢ (𝑁 ∈ ℤ → ((0 · 𝑁) = 0 → 𝑁 ∥ 0)) |
| 7 | 2, 6 | mpd 16 | 1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 0) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1101 = wceq 1568 ∈ wcel 2141 class class class wbr 5108 (class class class)co 7410 0cc0 11099 · cmul 11104 ℤcz 12590 ∥ cdvds 16309 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-br 5109 df-opab 5173 df-mpt 5192 df-id 5556 df-po 5569 df-so 5570 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-ov 7413 df-er 8693 df-en 8943 df-dom 8944 df-sdom 8945 df-pnf 11244 df-mnf 11245 df-ltxr 11247 df-neg 11443 df-z 12591 df-dvds 16310 |
| This theorem is referenced by: 0dvds 16333 fsumdvds 16365 alzdvds 16377 fzo0dvdseq 16380 z0even 16424 sadadd3 16518 gcddvds 16560 gcd0id 16576 bezoutlem4 16599 dfgcd2 16603 dvdssq 16624 dvdslcm 16655 lcmdvds 16665 dvdslcmf 16688 mulgcddvds 16712 odzdvds 16854 pcdvdsb 16928 pcz 16940 sylow2blem3 19691 odadd1 19917 odadd2 19918 cyggex2 19966 lgsne0 27475 lgsqr 27491 nn0prpw 36800 poimirlem25 38262 poimirlem26 38263 poimirlem27 38264 poimirlem28 38265 aks6d1c5lem1 42871 0dvds0 43056 dvdsexpnn0 43063 congid 43668 jm2.18 43685 jm2.19 43690 jm2.22 43692 jm2.23 43693 etransclem24 46942 etransclem25 46943 etransclem28 46946 |
| Copyright terms: Public domain | W3C validator |