Metamath Proof Explorer

Theorem mod0mul

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

Ref Expression
Assertion mod0mul ⊢ A ∈ ℤ ∧ N ∈ ℕ → A mod N = 0 → ∃ x ∈ ℤ A = x ⋅ N

Proof

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