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 ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 mod 𝑀 ) = 0 ) )

Proof

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