Metamath Proof Explorer


Theorem modmuladd

Description: Decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021)

Ref Expression
Assertion modmuladd ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) = 𝐵 ↔ ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 zre ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
2 1 adantr ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
3 rpre ( 𝑀 ∈ ℝ+𝑀 ∈ ℝ )
4 3 adantl ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → 𝑀 ∈ ℝ )
5 rpne0 ( 𝑀 ∈ ℝ+𝑀 ≠ 0 )
6 5 adantl ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → 𝑀 ≠ 0 )
7 2 4 6 redivcld ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 / 𝑀 ) ∈ ℝ )
8 7 flcld ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) ∈ ℤ )
9 8 3adant2 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) ∈ ℤ )
10 oveq1 ( 𝑘 = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) → ( 𝑘 · 𝑀 ) = ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) · 𝑀 ) )
11 10 oveq1d ( 𝑘 = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) → ( ( 𝑘 · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) = ( ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) )
12 11 eqeq2d ( 𝑘 = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) → ( 𝐴 = ( ( 𝑘 · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) ↔ 𝐴 = ( ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) ) )
13 12 adantl ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) ∧ 𝑘 = ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) ) → ( 𝐴 = ( ( 𝑘 · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) ↔ 𝐴 = ( ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) ) )
14 1 anim1i ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) )
15 14 3adant2 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) )
16 flpmodeq ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) = 𝐴 )
17 15 16 syl ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) = 𝐴 )
18 17 eqcomd ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) → 𝐴 = ( ( ( ⌊ ‘ ( 𝐴 / 𝑀 ) ) · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) )
19 9 13 18 rspcedvd ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) → ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) )
20 oveq2 ( 𝐵 = ( 𝐴 mod 𝑀 ) → ( ( 𝑘 · 𝑀 ) + 𝐵 ) = ( ( 𝑘 · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) )
21 20 eqeq2d ( 𝐵 = ( 𝐴 mod 𝑀 ) → ( 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ↔ 𝐴 = ( ( 𝑘 · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) ) )
22 21 eqcoms ( ( 𝐴 mod 𝑀 ) = 𝐵 → ( 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ↔ 𝐴 = ( ( 𝑘 · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) ) )
23 22 rexbidv ( ( 𝐴 mod 𝑀 ) = 𝐵 → ( ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ↔ ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + ( 𝐴 mod 𝑀 ) ) ) )
24 19 23 syl5ibrcom ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) = 𝐵 → ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) )
25 oveq1 ( 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) → ( 𝐴 mod 𝑀 ) = ( ( ( 𝑘 · 𝑀 ) + 𝐵 ) mod 𝑀 ) )
26 simpr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℤ )
27 simpl3 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) ∧ 𝑘 ∈ ℤ ) → 𝑀 ∈ ℝ+ )
28 simpl2 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) ∧ 𝑘 ∈ ℤ ) → 𝐵 ∈ ( 0 [,) 𝑀 ) )
29 muladdmodid ( ( 𝑘 ∈ ℤ ∧ 𝑀 ∈ ℝ+𝐵 ∈ ( 0 [,) 𝑀 ) ) → ( ( ( 𝑘 · 𝑀 ) + 𝐵 ) mod 𝑀 ) = 𝐵 )
30 26 27 28 29 syl3anc ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) ∧ 𝑘 ∈ ℤ ) → ( ( ( 𝑘 · 𝑀 ) + 𝐵 ) mod 𝑀 ) = 𝐵 )
31 25 30 sylan9eqr ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) ∧ 𝑘 ∈ ℤ ) ∧ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) → ( 𝐴 mod 𝑀 ) = 𝐵 )
32 31 rexlimdva2 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) → ( ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) → ( 𝐴 mod 𝑀 ) = 𝐵 ) )
33 24 32 impbid ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) = 𝐵 ↔ ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) )