This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑀 ) = 𝐵 ↔ ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) )