Metamath Proof Explorer

Theorem 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 ⊢ 0 ˙ = 0 Y
Assertion zndvds0 ⊢ N ∈ ℕ 0 ∧ A ∈ ℤ → L ⁡ A = 0 ˙ ↔ N ∥ A

Proof

Step Hyp Ref Expression
1 zncyg.y ⊢ Y = ℤ/Nℤ
2 zndvds.2 ⊢ L = ℤRHom ⁡ Y
3 zndvds0.3 ⊢ 0 ˙ = 0 Y
4 0z ⊢ 0 ∈ ℤ
5 1 2 zndvds ⊢ N ∈ ℕ 0 ∧ A ∈ ℤ ∧ 0 ∈ ℤ → L ⁡ A = L ⁡ 0 ↔ N ∥ A − 0
6 4 5 mp3an3 ⊢ N ∈ ℕ 0 ∧ A ∈ ℤ → L ⁡ A = L ⁡ 0 ↔ N ∥ A − 0
7 1 zncrng ⊢ N ∈ ℕ 0 → Y ∈ CRing
8 7 adantr ⊢ N ∈ ℕ 0 ∧ A ∈ ℤ → Y ∈ CRing
9 crngring ⊢ Y ∈ CRing → Y ∈ Ring
10 2 zrhrhm ⊢ Y ∈ Ring → L ∈ ℤ ring RingHom Y
11 8 9 10 3syl ⊢ N ∈ ℕ 0 ∧ A ∈ ℤ → L ∈ ℤ ring RingHom Y
12 rhmghm ⊢ L ∈ ℤ ring RingHom Y → L ∈ ℤ ring GrpHom Y
13 zring0 ⊢ 0 = 0 ℤ ring
14 13 3 ghmid ⊢ L ∈ ℤ ring GrpHom Y → L ⁡ 0 = 0 ˙
15 11 12 14 3syl ⊢ N ∈ ℕ 0 ∧ A ∈ ℤ → L ⁡ 0 = 0 ˙
16 15 eqeq2d ⊢ N ∈ ℕ 0 ∧ A ∈ ℤ → L ⁡ A = L ⁡ 0 ↔ L ⁡ A = 0 ˙
17 simpr ⊢ N ∈ ℕ 0 ∧ A ∈ ℤ → A ∈ ℤ
18 17 zcnd ⊢ N ∈ ℕ 0 ∧ A ∈ ℤ → A ∈ ℂ
19 18 subid1d ⊢ N ∈ ℕ 0 ∧ A ∈ ℤ → A − 0 = A
20 19 breq2d ⊢ N ∈ ℕ 0 ∧ A ∈ ℤ → N ∥ A − 0 ↔ N ∥ A
21 6 16 20 3bitr3d ⊢ N ∈ ℕ 0 ∧ A ∈ ℤ → L ⁡ A = 0 ˙ ↔ N ∥ A