Metamath Proof Explorer

Theorem modabsdifz

Description: Divisibility in terms of modular reduction by the absolute value of the base. (Contributed by Stefan O'Rear, 26-Sep-2014)

Ref Expression
Assertion modabsdifz ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M M ∈ ℤ

Proof

Step Hyp Ref Expression
1 simp1 ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N ∈ ℝ
2 simp2 ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → M ∈ ℝ
3 2 recnd ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → M ∈ ℂ
4 simp3 ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → M ≠ 0
5 3 4 absrpcld ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → M ∈ ℝ +
6 moddifz ⊢ N ∈ ℝ ∧ M ∈ ℝ + → N − N mod M M ∈ ℤ
7 1 5 6 syl2anc ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M M ∈ ℤ
8 absidm ⊢ M ∈ ℂ → M = M
9 3 8 syl ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → M = M
10 9 oveq2d ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M M = N − N mod M M
11 1 5 modcld ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N mod M ∈ ℝ
12 1 11 resubcld ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M ∈ ℝ
13 12 recnd ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M ∈ ℂ
14 3 abscld ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → M ∈ ℝ
15 14 recnd ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → M ∈ ℂ
16 5 rpne0d ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → M ≠ 0
17 13 15 16 absdivd ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M M = N − N mod M M
18 13 3 4 absdivd ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M M = N − N mod M M
19 10 17 18 3eqtr4d ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M M = N − N mod M M
20 19 eleq1d ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M M ∈ ℤ ↔ N − N mod M M ∈ ℤ
21 12 14 16 redivcld ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M M ∈ ℝ
22 absz ⊢ N − N mod M M ∈ ℝ → N − N mod M M ∈ ℤ ↔ N − N mod M M ∈ ℤ
23 21 22 syl ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M M ∈ ℤ ↔ N − N mod M M ∈ ℤ
24 12 2 4 redivcld ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M M ∈ ℝ
25 absz ⊢ N − N mod M M ∈ ℝ → N − N mod M M ∈ ℤ ↔ N − N mod M M ∈ ℤ
26 24 25 syl ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M M ∈ ℤ ↔ N − N mod M M ∈ ℤ
27 20 23 26 3bitr4d ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M M ∈ ℤ ↔ N − N mod M M ∈ ℤ
28 7 27 mpbid ⊢ N ∈ ℝ ∧ M ∈ ℝ ∧ M ≠ 0 → N − N mod M M ∈ ℤ