Theorem mod0mul

Description: If an integer is 0 modulo a positive integer, this integer must be the product of another integer and the modulus. (Contributed by AV, 7-Jun-2020)

	Ref	Expression
Assertion	mod0mul	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) = 0 → ∃ 𝑥 ∈ ℤ 𝐴 = ( 𝑥 · 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
2		nnrp	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
3		mod0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑁 ) = 0 ↔ ( 𝐴 / 𝑁 ) ∈ ℤ ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) = 0 ↔ ( 𝐴 / 𝑁 ) ∈ ℤ ) )
5		simpr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 / 𝑁 ) ∈ ℤ ) → ( 𝐴 / 𝑁 ) ∈ ℤ )
6		oveq1	⊢ ( 𝑥 = ( 𝐴 / 𝑁 ) → ( 𝑥 · 𝑁 ) = ( ( 𝐴 / 𝑁 ) · 𝑁 ) )
7	6	eqeq2d	⊢ ( 𝑥 = ( 𝐴 / 𝑁 ) → ( 𝐴 = ( 𝑥 · 𝑁 ) ↔ 𝐴 = ( ( 𝐴 / 𝑁 ) · 𝑁 ) ) )
8	7	adantl	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 / 𝑁 ) ∈ ℤ ) ∧ 𝑥 = ( 𝐴 / 𝑁 ) ) → ( 𝐴 = ( 𝑥 · 𝑁 ) ↔ 𝐴 = ( ( 𝐴 / 𝑁 ) · 𝑁 ) ) )
9		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
10	9	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℂ )
11		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
12	11	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
13		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
14	13	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 )
15	10 12 14	divcan1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 / 𝑁 ) · 𝑁 ) = 𝐴 )
16	15	adantr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 / 𝑁 ) ∈ ℤ ) → ( ( 𝐴 / 𝑁 ) · 𝑁 ) = 𝐴 )
17	16	eqcomd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 / 𝑁 ) ∈ ℤ ) → 𝐴 = ( ( 𝐴 / 𝑁 ) · 𝑁 ) )
18	5 8 17	rspcedvd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 / 𝑁 ) ∈ ℤ ) → ∃ 𝑥 ∈ ℤ 𝐴 = ( 𝑥 · 𝑁 ) )
19	18	ex	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 / 𝑁 ) ∈ ℤ → ∃ 𝑥 ∈ ℤ 𝐴 = ( 𝑥 · 𝑁 ) ) )
20	4 19	sylbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) = 0 → ∃ 𝑥 ∈ ℤ 𝐴 = ( 𝑥 · 𝑁 ) ) )