| 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 1478 | . 2 ⊢ (𝑁 ∈ ℤ → ((0 · 𝑁) = 0 → 𝑁 ∥ 0)) |
| 7 | 2, 6 | mpd 16 | 1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 0) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 class class class wbr 5113 (class class class)co 7411 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 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 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 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-br 5114 df-opab 5178 df-mpt 5197 df-id 5557 df-po 5570 df-so 5571 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-ov 7414 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 27464 lgsqr 27480 nn0prpw 36722 poimirlem25 38183 poimirlem26 38184 poimirlem27 38185 poimirlem28 38186 aks6d1c5lem1 42792 0dvds0 42977 dvdsexpnn0 42984 congid 43589 jm2.18 43606 jm2.19 43611 jm2.22 43613 jm2.23 43614 etransclem24 46863 etransclem25 46864 etransclem28 46867 |
| Copyright terms: Public domain | W3C validator |