Theorem remexz

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

	Ref	Expression
Hypotheses	remexz.1	|- ( ph -> N e. ZZ )
	remexz.2	|- ( ph -> A e. NN )
Assertion	remexz	|- ( ph -> E. x e. ZZ E. y e. ( 0 ... ( A - 1 ) ) N = ( ( x x. A ) + y ) )

Proof

Step	Hyp	Ref	Expression
1		remexz.1	|- ( ph -> N e. ZZ )
2		remexz.2	|- ( ph -> A e. NN )
3		zmodfzo	|- ( ( N e. ZZ /\ A e. NN ) -> ( N mod A ) e. ( 0 ..^ A ) )
4	1 2 3	syl2anc	|- ( ph -> ( N mod A ) e. ( 0 ..^ A ) )
5	2	nnzd	|- ( ph -> A e. ZZ )
6		fzoval	|- ( A e. ZZ -> ( 0 ..^ A ) = ( 0 ... ( A - 1 ) ) )
7	5 6	syl	|- ( ph -> ( 0 ..^ A ) = ( 0 ... ( A - 1 ) ) )
8	4 7	eleqtrd	|- ( ph -> ( N mod A ) e. ( 0 ... ( A - 1 ) ) )
9		simpr	|- ( ( ph /\ y = ( N mod A ) ) -> y = ( N mod A ) )
10	9	oveq2d	|- ( ( ph /\ y = ( N mod A ) ) -> ( ( x x. A ) + y ) = ( ( x x. A ) + ( N mod A ) ) )
11	10	eqeq2d	|- ( ( ph /\ y = ( N mod A ) ) -> ( N = ( ( x x. A ) + y ) <-> N = ( ( x x. A ) + ( N mod A ) ) ) )
12	11	rexbidv	|- ( ( ph /\ y = ( N mod A ) ) -> ( E. x e. ZZ N = ( ( x x. A ) + y ) <-> E. x e. ZZ N = ( ( x x. A ) + ( N mod A ) ) ) )
13		eqidd	|- ( ph -> ( N mod A ) = ( N mod A ) )
14	2	nnrpd	|- ( ph -> A e. RR+ )
15		modmuladdim	|- ( ( N e. ZZ /\ A e. RR+ ) -> ( ( N mod A ) = ( N mod A ) -> E. x e. ZZ N = ( ( x x. A ) + ( N mod A ) ) ) )
16	1 14 15	syl2anc	|- ( ph -> ( ( N mod A ) = ( N mod A ) -> E. x e. ZZ N = ( ( x x. A ) + ( N mod A ) ) ) )
17	13 16	mpd	|- ( ph -> E. x e. ZZ N = ( ( x x. A ) + ( N mod A ) ) )
18	8 12 17	rspcedvd	|- ( ph -> E. y e. ( 0 ... ( A - 1 ) ) E. x e. ZZ N = ( ( x x. A ) + y ) )
19		rexcom	|- ( E. x e. ZZ E. y e. ( 0 ... ( A - 1 ) ) N = ( ( x x. A ) + y ) <-> E. y e. ( 0 ... ( A - 1 ) ) E. x e. ZZ N = ( ( x x. A ) + y ) )
20	18 19	sylibr	|- ( ph -> E. x e. ZZ E. y e. ( 0 ... ( A - 1 ) ) N = ( ( x x. A ) + y ) )