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