Metamath Proof Explorer


Theorem modmuladdim

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

Ref Expression
Assertion modmuladdim ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) = 𝐵 → ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 zre ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
2 modelico ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ( 0 [,) 𝑀 ) )
3 1 2 sylan ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ( 0 [,) 𝑀 ) )
4 3 adantr ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) → ( 𝐴 mod 𝑀 ) ∈ ( 0 [,) 𝑀 ) )
5 eleq1 ( ( 𝐴 mod 𝑀 ) = 𝐵 → ( ( 𝐴 mod 𝑀 ) ∈ ( 0 [,) 𝑀 ) ↔ 𝐵 ∈ ( 0 [,) 𝑀 ) ) )
6 5 adantl ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) → ( ( 𝐴 mod 𝑀 ) ∈ ( 0 [,) 𝑀 ) ↔ 𝐵 ∈ ( 0 [,) 𝑀 ) ) )
7 4 6 mpbid ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) → 𝐵 ∈ ( 0 [,) 𝑀 ) )
8 simpll ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ) → 𝐴 ∈ ℤ )
9 simpr ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ) → 𝐵 ∈ ( 0 [,) 𝑀 ) )
10 simpr ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → 𝑀 ∈ ℝ+ )
11 10 adantr ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ) → 𝑀 ∈ ℝ+ )
12 modmuladd ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) = 𝐵 ↔ ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) )
13 8 9 11 12 syl3anc ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ) → ( ( 𝐴 mod 𝑀 ) = 𝐵 ↔ ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) )
14 13 biimpd ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ 𝐵 ∈ ( 0 [,) 𝑀 ) ) → ( ( 𝐴 mod 𝑀 ) = 𝐵 → ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) )
15 14 impancom ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) → ( 𝐵 ∈ ( 0 [,) 𝑀 ) → ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) )
16 7 15 mpd ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑀 ) = 𝐵 ) → ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) )
17 16 ex ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) = 𝐵 → ∃ 𝑘 ∈ ℤ 𝐴 = ( ( 𝑘 · 𝑀 ) + 𝐵 ) ) )