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 ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≠ 0 ) → ( ( 𝑁 − ( 𝑁 mod ( abs ‘ 𝑀 ) ) ) / 𝑀 ) ∈ ℤ )

Proof

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