Theorem remexz

Description: Division with rest. (Contributed by metakunt, 15-May-2025)

	Ref	Expression
Hypotheses	remexz.1	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	remexz.2	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
Assertion	remexz	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( 0 ... ( 𝐴 − 1 ) ) 𝑁 = ( ( 𝑥 · 𝐴 ) + 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		remexz.1	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
2		remexz.2	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
3		zmodfzo	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ ) → ( 𝑁 mod 𝐴 ) ∈ ( 0 ..^ 𝐴 ) )
4	1 2 3	syl2anc	⊢ ( 𝜑 → ( 𝑁 mod 𝐴 ) ∈ ( 0 ..^ 𝐴 ) )
5	2	nnzd	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
6		fzoval	⊢ ( 𝐴 ∈ ℤ → ( 0 ..^ 𝐴 ) = ( 0 ... ( 𝐴 − 1 ) ) )
7	5 6	syl	⊢ ( 𝜑 → ( 0 ..^ 𝐴 ) = ( 0 ... ( 𝐴 − 1 ) ) )
8	4 7	eleqtrd	⊢ ( 𝜑 → ( 𝑁 mod 𝐴 ) ∈ ( 0 ... ( 𝐴 − 1 ) ) )
9		simpr	⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑁 mod 𝐴 ) ) → 𝑦 = ( 𝑁 mod 𝐴 ) )
10	9	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑁 mod 𝐴 ) ) → ( ( 𝑥 · 𝐴 ) + 𝑦 ) = ( ( 𝑥 · 𝐴 ) + ( 𝑁 mod 𝐴 ) ) )
11	10	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑁 mod 𝐴 ) ) → ( 𝑁 = ( ( 𝑥 · 𝐴 ) + 𝑦 ) ↔ 𝑁 = ( ( 𝑥 · 𝐴 ) + ( 𝑁 mod 𝐴 ) ) ) )
12	11	rexbidv	⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑁 mod 𝐴 ) ) → ( ∃ 𝑥 ∈ ℤ 𝑁 = ( ( 𝑥 · 𝐴 ) + 𝑦 ) ↔ ∃ 𝑥 ∈ ℤ 𝑁 = ( ( 𝑥 · 𝐴 ) + ( 𝑁 mod 𝐴 ) ) ) )
13		eqidd	⊢ ( 𝜑 → ( 𝑁 mod 𝐴 ) = ( 𝑁 mod 𝐴 ) )
14	2	nnrpd	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
15		modmuladdim	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ+ ) → ( ( 𝑁 mod 𝐴 ) = ( 𝑁 mod 𝐴 ) → ∃ 𝑥 ∈ ℤ 𝑁 = ( ( 𝑥 · 𝐴 ) + ( 𝑁 mod 𝐴 ) ) ) )
16	1 14 15	syl2anc	⊢ ( 𝜑 → ( ( 𝑁 mod 𝐴 ) = ( 𝑁 mod 𝐴 ) → ∃ 𝑥 ∈ ℤ 𝑁 = ( ( 𝑥 · 𝐴 ) + ( 𝑁 mod 𝐴 ) ) ) )
17	13 16	mpd	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℤ 𝑁 = ( ( 𝑥 · 𝐴 ) + ( 𝑁 mod 𝐴 ) ) )
18	8 12 17	rspcedvd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 0 ... ( 𝐴 − 1 ) ) ∃ 𝑥 ∈ ℤ 𝑁 = ( ( 𝑥 · 𝐴 ) + 𝑦 ) )
19		rexcom	⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( 0 ... ( 𝐴 − 1 ) ) 𝑁 = ( ( 𝑥 · 𝐴 ) + 𝑦 ) ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝐴 − 1 ) ) ∃ 𝑥 ∈ ℤ 𝑁 = ( ( 𝑥 · 𝐴 ) + 𝑦 ) )
20	18 19	sylibr	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( 0 ... ( 𝐴 − 1 ) ) 𝑁 = ( ( 𝑥 · 𝐴 ) + 𝑦 ) )