zndvds0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > zndvds0		Structured version Visualization version GIF version

Theorem zndvds0 21488

Description: Special case of zndvds 21487 when one argument is zero. (Contributed by Mario Carneiro, 15-Jun-2015.)

**Hypotheses**
Ref	Expression
zncyg.y	⊢ 𝑌 = (ℤ/nℤ‘𝑁)
zndvds.2	⊢ 𝐿 = (ℤRHom‘𝑌)
zndvds0.3	⊢ 0 = (0_g‘𝑌)

**Assertion**
Ref	Expression
zndvds0	⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) = 0 ↔ 𝑁 ∥ 𝐴))

**Proof of Theorem zndvds0**
Step	Hyp	Ref	Expression
1		0z 12479	. . 3 ⊢ 0 ∈ ℤ
2		zncyg.y	. . . 4 ⊢ 𝑌 = (ℤ/nℤ‘𝑁)
3		zndvds.2	. . . 4 ⊢ 𝐿 = (ℤRHom‘𝑌)
4	2, 3	zndvds 21487	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐴 ∈ ℤ ∧ 0 ∈ ℤ) → ((𝐿‘𝐴) = (𝐿‘0) ↔ 𝑁 ∥ (𝐴 − 0)))
5	1, 4	mp3an3 1452	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) = (𝐿‘0) ↔ 𝑁 ∥ (𝐴 − 0)))
6	2	zncrng 21482	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → 𝑌 ∈ CRing)
7	6	adantr 480	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐴 ∈ ℤ) → 𝑌 ∈ CRing)
8		crngring 20164	. . . . 5 ⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring)
9	3	zrhrhm 21449	. . . . 5 ⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
10	7, 8, 9	3syl 18	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐴 ∈ ℤ) → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
11		rhmghm 20402	. . . 4 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿 ∈ (ℤ_ring GrpHom 𝑌))
12		zring0 21396	. . . . 5 ⊢ 0 = (0_g‘ℤ_ring)
13		zndvds0.3	. . . . 5 ⊢ 0 = (0_g‘𝑌)
14	12, 13	ghmid 19135	. . . 4 ⊢ (𝐿 ∈ (ℤ_ring GrpHom 𝑌) → (𝐿‘0) = 0 )
15	10, 11, 14	3syl 18	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐴 ∈ ℤ) → (𝐿‘0) = 0 )
16	15	eqeq2d 2742	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) = (𝐿‘0) ↔ (𝐿‘𝐴) = 0 ))
17		simpr 484	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐴 ∈ ℤ) → 𝐴 ∈ ℤ)
18	17	zcnd 12578	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐴 ∈ ℤ) → 𝐴 ∈ ℂ)
19	18	subid1d 11461	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐴 ∈ ℤ) → (𝐴 − 0) = 𝐴)
20	19	breq2d 5103	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐴 ∈ ℤ) → (𝑁 ∥ (𝐴 − 0) ↔ 𝑁 ∥ 𝐴))
21	5, 16, 20	3bitr3d 309	1 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) = 0 ↔ 𝑁 ∥ 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2111 class class class wbr 5091 ‘cfv 6481 (class class class)co 7346 0cc0 11006 − cmin 11344 ℕ₀cn0 12381 ℤcz 12468 ∥ cdvds 16163 0_gc0g 17343 GrpHom cghm 19125 Ringcrg 20152 CRingccrg 20153 RingHom crh 20388 ℤ_ringczring 21384 ℤRHomczrh 21437 ℤ/nℤczn 21440

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-addf 11085 ax-mulf 11086

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-tp 4581 df-op 4583 df-uni 4860 df-int 4898 df-iun 4943 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-tpos 8156 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-er 8622 df-ec 8624 df-qs 8628 df-map 8752 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-sup 9326 df-inf 9327 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-nn 12126 df-2 12188 df-3 12189 df-4 12190 df-5 12191 df-6 12192 df-7 12193 df-8 12194 df-9 12195 df-n0 12382 df-z 12469 df-dec 12589 df-uz 12733 df-fz 13408 df-seq 13909 df-dvds 16164 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-0g 17345 df-imas 17412 df-qus 17413 df-mgm 18548 df-sgrp 18627 df-mnd 18643 df-mhm 18691 df-grp 18849 df-minusg 18850 df-sbg 18851 df-mulg 18981 df-subg 19036 df-nsg 19037 df-eqg 19038 df-ghm 19126 df-cmn 19695 df-abl 19696 df-mgp 20060 df-rng 20072 df-ur 20101 df-ring 20154 df-cring 20155 df-oppr 20256 df-dvdsr 20276 df-rhm 20391 df-subrng 20462 df-subrg 20486 df-lmod 20796 df-lss 20866 df-lsp 20906 df-sra 21108 df-rgmod 21109 df-lidl 21146 df-rsp 21147 df-2idl 21188 df-cnfld 21293 df-zring 21385 df-zrh 21441 df-zn 21444

This theorem is referenced by: znfld 21498 znidomb 21499 znchr 21500 znrrg 21503 lgseisenlem3 27316 znfermltl 33329

W3C validator