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−NmodMM∈ℤ

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−NmodMM∈ℤ
7 1 5 6 syl2anc ⊢N∈ℝ∧M∈ℝ∧M≠0→N−NmodMM∈ℤ
8 absidm ⊢M∈ℂ→M=M
9 3 8 syl ⊢N∈ℝ∧M∈ℝ∧M≠0→M=M
10 9 oveq2d ⊢N∈ℝ∧M∈ℝ∧M≠0→N−NmodMM=N−NmodMM
11 1 5 modcld ⊢N∈ℝ∧M∈ℝ∧M≠0→NmodM∈ℝ
12 1 11 resubcld ⊢N∈ℝ∧M∈ℝ∧M≠0→N−NmodM∈ℝ
13 12 recnd ⊢N∈ℝ∧M∈ℝ∧M≠0→N−NmodM∈ℂ
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−NmodMM=N−NmodMM
18 13 3 4 absdivd ⊢N∈ℝ∧M∈ℝ∧M≠0→N−NmodMM=N−NmodMM
19 10 17 18 3eqtr4d ⊢N∈ℝ∧M∈ℝ∧M≠0→N−NmodMM=N−NmodMM
20 19 eleq1d ⊢N∈ℝ∧M∈ℝ∧M≠0→N−NmodMM∈ℤ↔N−NmodMM∈ℤ
21 12 14 16 redivcld ⊢N∈ℝ∧M∈ℝ∧M≠0→N−NmodMM∈ℝ
22 absz ⊢N−NmodMM∈ℝ→N−NmodMM∈ℤ↔N−NmodMM∈ℤ
23 21 22 syl ⊢N∈ℝ∧M∈ℝ∧M≠0→N−NmodMM∈ℤ↔N−NmodMM∈ℤ
24 12 2 4 redivcld ⊢N∈ℝ∧M∈ℝ∧M≠0→N−NmodMM∈ℝ
25 absz ⊢N−NmodMM∈ℝ→N−NmodMM∈ℤ↔N−NmodMM∈ℤ
26 24 25 syl ⊢N∈ℝ∧M∈ℝ∧M≠0→N−NmodMM∈ℤ↔N−NmodMM∈ℤ
27 20 23 26 3bitr4d ⊢N∈ℝ∧M∈ℝ∧M≠0→N−NmodMM∈ℤ↔N−NmodMM∈ℤ
28 7 27 mpbid ⊢N∈ℝ∧M∈ℝ∧M≠0→N−NmodMM∈ℤ