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

Metamath Proof Explorer

Theorem divalgmodcl

Description: The result of the mod operator satisfies the requirements for the remainder R in the division algorithm for a positive divisor. Variant of divalgmod . (Contributed by Stefan O'Rear, 17-Oct-2014) (Proof shortened by AV, 21-Aug-2021)

Ref Expression
Assertion divalgmodcl ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0 ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) )

Proof

Step Hyp Ref Expression
1 divalgmod ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ( 𝑅 ∈ ℕ0 ∧ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) ) )
2 1 baibd ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) ∧ 𝑅 ∈ ℕ0 ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) )
3 2 3impa ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0 ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) )