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