zndvds0

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

	Ref	Expression
Hypotheses	zncyg.y	$⊢ Y = ℤ / N ℤ$
	zndvds.2	$⊢ L = ℤRHom (Y)$
	zndvds0.3	$⊢ \underset{˙}{0} = 0_{Y}$
Assertion	zndvds0	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (L (A) = \underset{˙}{0} \leftrightarrow N ∥ A)$

Step	Hyp	Ref	Expression
1		zncyg.y	$⊢ Y = ℤ / N ℤ$
2		zndvds.2	$⊢ L = ℤRHom (Y)$
3		zndvds0.3	$⊢ \underset{˙}{0} = 0_{Y}$
4		0z	$⊢ 0 \in ℤ$
5	1 2	zndvds	$⊢ (N \in ℕ_{0} \land A \in ℤ \land 0 \in ℤ) \to (L (A) = L (0) \leftrightarrow N ∥ (A - 0))$
6	4 5	mp3an3	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (L (A) = L (0) \leftrightarrow N ∥ (A - 0))$
7	1	zncrng	$⊢ N \in ℕ_{0} \to Y \in CRing$
8	7	adantr	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to Y \in CRing$
9		crngring	$⊢ Y \in CRing \to Y \in Ring$
10	2	zrhrhm	$⊢ Y \in Ring \to L \in (ℤ_{ring} RingHom Y)$
11	8 9 10	3syl	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to L \in (ℤ_{ring} RingHom Y)$
12		rhmghm	$⊢ L \in (ℤ_{ring} RingHom Y) \to L \in (ℤ_{ring} GrpHom Y)$
13		zring0	$⊢ 0 = 0_{ℤ_{ring}}$
14	13 3	ghmid	$⊢ L \in (ℤ_{ring} GrpHom Y) \to L (0) = \underset{˙}{0}$
15	11 12 14	3syl	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to L (0) = \underset{˙}{0}$
16	15	eqeq2d	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (L (A) = L (0) \leftrightarrow L (A) = \underset{˙}{0})$
17		simpr	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to A \in ℤ$
18	17	zcnd	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to A \in ℂ$
19	18	subid1d	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to A - 0 = A$
20	19	breq2d	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (N ∥ (A - 0) \leftrightarrow N ∥ A)$
21	6 16 20	3bitr3d	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (L (A) = \underset{˙}{0} \leftrightarrow N ∥ A)$

Metamath Proof Explorer