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

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