remexz

	Ref	Expression
Hypotheses	remexz.1	$⊢ φ \to N \in ℤ$
	remexz.2	$⊢ φ \to A \in ℕ$
Assertion	remexz	$⊢ φ \to \exists x \in ℤ \exists y \in (0 \dots A - 1) N = x A + y$

Step	Hyp	Ref	Expression
1		remexz.1	$⊢ φ \to N \in ℤ$
2		remexz.2	$⊢ φ \to A \in ℕ$
3		zmodfzo	$⊢ (N \in ℤ \land A \in ℕ) \to N \mod A \in (0 ..^A)$
4	1 2 3	syl2anc	$⊢ φ \to N \mod A \in (0 ..^A)$
5	2	nnzd	$⊢ φ \to A \in ℤ$
6		fzoval	$⊢ A \in ℤ \to (0 ..^A) = (0 \dots A - 1)$
7	5 6	syl	$⊢ φ \to (0 ..^A) = (0 \dots A - 1)$
8	4 7	eleqtrd	$⊢ φ \to N \mod A \in (0 \dots A - 1)$
9		simpr	$⊢ (φ \land y = N \mod A) \to y = N \mod A$
10	9	oveq2d	$⊢ (φ \land y = N \mod A) \to x A + y = x A + (N \mod A)$
11	10	eqeq2d	$⊢ (φ \land y = N \mod A) \to (N = x A + y \leftrightarrow N = x A + (N \mod A))$
12	11	rexbidv	$⊢ (φ \land y = N \mod A) \to (\exists x \in ℤ N = x A + y \leftrightarrow \exists x \in ℤ N = x A + (N \mod A))$
13		eqidd	$⊢ φ \to N \mod A = N \mod A$
14	2	nnrpd	$⊢ φ \to A \in ℝ^{+}$
15		modmuladdim	$⊢ (N \in ℤ \land A \in ℝ^{+}) \to (N \mod A = N \mod A \to \exists x \in ℤ N = x A + (N \mod A))$
16	1 14 15	syl2anc	$⊢ φ \to (N \mod A = N \mod A \to \exists x \in ℤ N = x A + (N \mod A))$
17	13 16	mpd	$⊢ φ \to \exists x \in ℤ N = x A + (N \mod A)$
18	8 12 17	rspcedvd	$⊢ φ \to \exists y \in (0 \dots A - 1) \exists x \in ℤ N = x A + y$
19		rexcom	$⊢ \exists x \in ℤ \exists y \in (0 \dots A - 1) N = x A + y \leftrightarrow \exists y \in (0 \dots A - 1) \exists x \in ℤ N = x A + y$
20	18 19	sylibr	$⊢ φ \to \exists x \in ℤ \exists y \in (0 \dots A - 1) N = x A + y$

Metamath Proof Explorer