This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdsval3

Description: One nonzero integer divides another integer if and only if the remainder upon division is zero, see remark in ApostolNT p. 106. (Contributed by Mario Carneiro, 22-Feb-2014) (Revised by Mario Carneiro, 15-Jul-2014)

Ref Expression
Assertion dvdsval3 ⊢ M ∈ ℕ ∧ N ∈ ℤ → M ∥ N ↔ N mod M = 0

Proof

Step Hyp Ref Expression
1 nnz ⊢ M ∈ ℕ → M ∈ ℤ
2 nnne0 ⊢ M ∈ ℕ → M ≠ 0
3 1 2 jca ⊢ M ∈ ℕ → M ∈ ℤ ∧ M ≠ 0
4 dvdsval2 ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ → M ∥ N ↔ N M ∈ ℤ
5 4 3expa ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ → M ∥ N ↔ N M ∈ ℤ
6 3 5 sylan ⊢ M ∈ ℕ ∧ N ∈ ℤ → M ∥ N ↔ N M ∈ ℤ
7 zre ⊢ N ∈ ℤ → N ∈ ℝ
8 nnrp ⊢ M ∈ ℕ → M ∈ ℝ +
9 mod0 ⊢ N ∈ ℝ ∧ M ∈ ℝ + → N mod M = 0 ↔ N M ∈ ℤ
10 7 8 9 syl2anr ⊢ M ∈ ℕ ∧ N ∈ ℤ → N mod M = 0 ↔ N M ∈ ℤ
11 6 10 bitr4d ⊢ M ∈ ℕ ∧ N ∈ ℤ → M ∥ N ↔ N mod M = 0