Metamath Proof Explorer

Theorem modremain

Description: The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021)

Ref Expression
Assertion modremain ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → ( ( 𝑁 mod 𝐷 ) = 𝑅 ↔ ∃ 𝑧 ∈ ℤ ( ( 𝑧 · 𝐷 ) + 𝑅 ) = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 eqcom ⊢ ( ( 𝑁 mod 𝐷 ) = 𝑅 ↔ 𝑅 = ( 𝑁 mod 𝐷 ) )
2 divalgmodcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0 ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) )
3 2 3adant3r ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) )
4 ibar ⊢ ( 𝑅 < 𝐷 → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) ↔ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) )
5 4 adantl ⊢ ( ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) ↔ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) )
6 5 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) ↔ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) )
7 nnz ⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℤ )
8 7 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → 𝐷 ∈ ℤ )
9 simp1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → 𝑁 ∈ ℤ )
10 nn0z ⊢ ( 𝑅 ∈ ℕ0 → 𝑅 ∈ ℤ )
11 10 adantr ⊢ ( ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) → 𝑅 ∈ ℤ )
12 11 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → 𝑅 ∈ ℤ )
13 9 12 zsubcld ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → ( 𝑁 − 𝑅 ) ∈ ℤ )
14 divides ⊢ ( ( 𝐷 ∈ ℤ ∧ ( 𝑁 − 𝑅 ) ∈ ℤ ) → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) ↔ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝐷 ) = ( 𝑁 − 𝑅 ) ) )
15 8 13 14 syl2anc ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) ↔ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝐷 ) = ( 𝑁 − 𝑅 ) ) )
16 eqcom ⊢ ( ( 𝑧 · 𝐷 ) = ( 𝑁 − 𝑅 ) ↔ ( 𝑁 − 𝑅 ) = ( 𝑧 · 𝐷 ) )
17 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
18 17 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → 𝑁 ∈ ℂ )
19 18 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) ∧ 𝑧 ∈ ℤ ) → 𝑁 ∈ ℂ )
20 nn0cn ⊢ ( 𝑅 ∈ ℕ0 → 𝑅 ∈ ℂ )
21 20 adantr ⊢ ( ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) → 𝑅 ∈ ℂ )
22 21 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → 𝑅 ∈ ℂ )
23 22 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) ∧ 𝑧 ∈ ℤ ) → 𝑅 ∈ ℂ )
24 simpr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) ∧ 𝑧 ∈ ℤ ) → 𝑧 ∈ ℤ )
25 8 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) ∧ 𝑧 ∈ ℤ ) → 𝐷 ∈ ℤ )
26 24 25 zmulcld ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) ∧ 𝑧 ∈ ℤ ) → ( 𝑧 · 𝐷 ) ∈ ℤ )
27 26 zcnd ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) ∧ 𝑧 ∈ ℤ ) → ( 𝑧 · 𝐷 ) ∈ ℂ )
28 19 23 27 subadd2d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) ∧ 𝑧 ∈ ℤ ) → ( ( 𝑁 − 𝑅 ) = ( 𝑧 · 𝐷 ) ↔ ( ( 𝑧 · 𝐷 ) + 𝑅 ) = 𝑁 ) )
29 16 28 syl5bb ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) ∧ 𝑧 ∈ ℤ ) → ( ( 𝑧 · 𝐷 ) = ( 𝑁 − 𝑅 ) ↔ ( ( 𝑧 · 𝐷 ) + 𝑅 ) = 𝑁 ) )
30 29 rexbidva ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → ( ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝐷 ) = ( 𝑁 − 𝑅 ) ↔ ∃ 𝑧 ∈ ℤ ( ( 𝑧 · 𝐷 ) + 𝑅 ) = 𝑁 ) )
31 15 30 bitrd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) ↔ ∃ 𝑧 ∈ ℤ ( ( 𝑧 · 𝐷 ) + 𝑅 ) = 𝑁 ) )
32 3 6 31 3bitr2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ∃ 𝑧 ∈ ℤ ( ( 𝑧 · 𝐷 ) + 𝑅 ) = 𝑁 ) )
33 1 32 syl5bb ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ ( 𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷 ) ) → ( ( 𝑁 mod 𝐷 ) = 𝑅 ↔ ∃ 𝑧 ∈ ℤ ( ( 𝑧 · 𝐷 ) + 𝑅 ) = 𝑁 ) )