m1modmmod

Description: An integer decreased by 1 modulo a positive integer minus the integer modulo the same modulus is either -1 or the modulus minus 1. (Contributed by AV, 7-Jun-2020)

		Ref	Expression
	Assertion	m1modmmod	$⊢ (A \in ℤ \land N \in ℕ) \to ((A - 1) \mod N) - (A \mod N) = if (A \mod N = 0, N - 1, - 1)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ A \mod N = 0 \to ((A - 1) \mod N) - (A \mod N) = ((A - 1) \mod N) - 0$
2	1	adantl	$⊢ ((A \in ℤ \land N \in ℕ) \land A \mod N = 0) \to ((A - 1) \mod N) - (A \mod N) = ((A - 1) \mod N) - 0$
3		peano2zm	$⊢ A \in ℤ \to A - 1 \in ℤ$
4	3	zred	$⊢ A \in ℤ \to A - 1 \in ℝ$
5	4	adantr	$⊢ (A \in ℤ \land N \in ℕ) \to A - 1 \in ℝ$
6		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
7	6	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to N \in ℝ^{+}$
8	5 7	modcld	$⊢ (A \in ℤ \land N \in ℕ) \to (A - 1) \mod N \in ℝ$
9	8	recnd	$⊢ (A \in ℤ \land N \in ℕ) \to (A - 1) \mod N \in ℂ$
10	9	subid1d	$⊢ (A \in ℤ \land N \in ℕ) \to ((A - 1) \mod N) - 0 = (A - 1) \mod N$
11	10	adantr	$⊢ ((A \in ℤ \land N \in ℕ) \land A \mod N = 0) \to ((A - 1) \mod N) - 0 = (A - 1) \mod N$
12		mod0mul	$⊢ (A \in ℤ \land N \in ℕ) \to (A \mod N = 0 \to \exists x \in ℤ A = x \cdot N)$
13	12	imp	$⊢ ((A \in ℤ \land N \in ℕ) \land A \mod N = 0) \to \exists x \in ℤ A = x \cdot N$
14		oveq1	$⊢ A = x \cdot N \to A - 1 = x \cdot N - 1$
15	14	oveq1d	$⊢ A = x \cdot N \to (A - 1) \mod N = (x \cdot N - 1) \mod N$
16		zcn	$⊢ x \in ℤ \to x \in ℂ$
17		nncn	$⊢ N \in ℕ \to N \in ℂ$
18	17	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to N \in ℂ$
19		mulcl	$⊢ (x \in ℂ \land N \in ℂ) \to x \cdot N \in ℂ$
20	16 18 19	syl2anr	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to x \cdot N \in ℂ$
21	18	adantr	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to N \in ℂ$
22	20 21	npcand	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to x \cdot N - N + N = x \cdot N$
23	22	eqcomd	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to x \cdot N = x \cdot N - N + N$
24	16	adantl	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to x \in ℂ$
25	24 21	mulsubfacd	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to x \cdot N - N = (x - 1) \cdot N$
26	25	oveq1d	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to x \cdot N - N + N = (x - 1) \cdot N + N$
27	23 26	eqtrd	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to x \cdot N = (x - 1) \cdot N + N$
28	27	oveq1d	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to x \cdot N - 1 = (x - 1) \cdot N + N - 1$
29		peano2zm	$⊢ x \in ℤ \to x - 1 \in ℤ$
30	29	zcnd	$⊢ x \in ℤ \to x - 1 \in ℂ$
31		mulcl	$⊢ (x - 1 \in ℂ \land N \in ℂ) \to (x - 1) \cdot N \in ℂ$
32	30 18 31	syl2anr	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to (x - 1) \cdot N \in ℂ$
33		1cnd	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to 1 \in ℂ$
34	32 21 33	addsubassd	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to (x - 1) \cdot N + N - 1 = (x - 1) \cdot N + N - 1$
35	28 34	eqtrd	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to x \cdot N - 1 = (x - 1) \cdot N + N - 1$
36	35	oveq1d	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to (x \cdot N - 1) \mod N = ((x - 1) \cdot N + N - 1) \mod N$
37		nnre	$⊢ N \in ℕ \to N \in ℝ$
38		peano2rem	$⊢ N \in ℝ \to N - 1 \in ℝ$
39	37 38	syl	$⊢ N \in ℕ \to N - 1 \in ℝ$
40	39	recnd	$⊢ N \in ℕ \to N - 1 \in ℂ$
41	40	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to N - 1 \in ℂ$
42	41	adantr	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to N - 1 \in ℂ$
43	32 42	addcomd	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to (x - 1) \cdot N + N - 1 = N - 1 + (x - 1) \cdot N$
44	43	oveq1d	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to ((x - 1) \cdot N + N - 1) \mod N = (N - 1 + (x - 1) \cdot N) \mod N$
45	39	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to N - 1 \in ℝ$
46	45	adantr	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to N - 1 \in ℝ$
47	7	adantr	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to N \in ℝ^{+}$
48	29	adantl	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to x - 1 \in ℤ$
49		modcyc	$⊢ (N - 1 \in ℝ \land N \in ℝ^{+} \land x - 1 \in ℤ) \to (N - 1 + (x - 1) \cdot N) \mod N = (N - 1) \mod N$
50	46 47 48 49	syl3anc	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to (N - 1 + (x - 1) \cdot N) \mod N = (N - 1) \mod N$
51	39 6	jca	$⊢ N \in ℕ \to (N - 1 \in ℝ \land N \in ℝ^{+})$
52	51	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to (N - 1 \in ℝ \land N \in ℝ^{+})$
53	52	adantr	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to (N - 1 \in ℝ \land N \in ℝ^{+})$
54		nnm1ge0	$⊢ N \in ℕ \to 0 \leq N - 1$
55	54	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to 0 \leq N - 1$
56	55	adantr	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to 0 \leq N - 1$
57	37	ltm1d	$⊢ N \in ℕ \to N - 1 < N$
58	57	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to N - 1 < N$
59	58	adantr	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to N - 1 < N$
60		modid	$⊢ ((N - 1 \in ℝ \land N \in ℝ^{+}) \land (0 \leq N - 1 \land N - 1 < N)) \to (N - 1) \mod N = N - 1$
61	53 56 59 60	syl12anc	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to (N - 1) \mod N = N - 1$
62	50 61	eqtrd	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to (N - 1 + (x - 1) \cdot N) \mod N = N - 1$
63	36 44 62	3eqtrd	$⊢ ((A \in ℤ \land N \in ℕ) \land x \in ℤ) \to (x \cdot N - 1) \mod N = N - 1$
64	15 63	sylan9eqr	$⊢ (((A \in ℤ \land N \in ℕ) \land x \in ℤ) \land A = x \cdot N) \to (A - 1) \mod N = N - 1$
65	64	rexlimdva2	$⊢ (A \in ℤ \land N \in ℕ) \to (\exists x \in ℤ A = x \cdot N \to (A - 1) \mod N = N - 1)$
66	65	adantr	$⊢ ((A \in ℤ \land N \in ℕ) \land A \mod N = 0) \to (\exists x \in ℤ A = x \cdot N \to (A - 1) \mod N = N - 1)$
67	13 66	mpd	$⊢ ((A \in ℤ \land N \in ℕ) \land A \mod N = 0) \to (A - 1) \mod N = N - 1$
68	2 11 67	3eqtrrd	$⊢ ((A \in ℤ \land N \in ℕ) \land A \mod N = 0) \to N - 1 = ((A - 1) \mod N) - (A \mod N)$
69		df-ne	$⊢ A \mod N \neq 0 \leftrightarrow \neg A \mod N = 0$
70		modn0mul	$⊢ (A \in ℤ \land N \in ℕ) \to (A \mod N \neq 0 \to \exists x \in ℤ \exists y \in (1 ..^N) A = x \cdot N + y)$
71		oveq1	$⊢ A = x \cdot N + y \to A - 1 = x \cdot N + y - 1$
72	71	oveq1d	$⊢ A = x \cdot N + y \to (A - 1) \mod N = (x \cdot N + y - 1) \mod N$
73		oveq1	$⊢ A = x \cdot N + y \to A \mod N = (x \cdot N + y) \mod N$
74	72 73	oveq12d	$⊢ A = x \cdot N + y \to ((A - 1) \mod N) - (A \mod N) = ((x \cdot N + y - 1) \mod N) - ((x \cdot N + y) \mod N)$
75	16	adantr	$⊢ (x \in ℤ \land y \in (1 ..^N)) \to x \in ℂ$
76	75 18 19	syl2anr	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to x \cdot N \in ℂ$
77		elfzoelz	$⊢ y \in (1 ..^N) \to y \in ℤ$
78	77	zcnd	$⊢ y \in (1 ..^N) \to y \in ℂ$
79	78	adantl	$⊢ (x \in ℤ \land y \in (1 ..^N)) \to y \in ℂ$
80	79	adantl	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to y \in ℂ$
81		1cnd	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to 1 \in ℂ$
82	76 80 81	addsubassd	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to x \cdot N + y - 1 = x \cdot N + y - 1$
83		peano2zm	$⊢ y \in ℤ \to y - 1 \in ℤ$
84	77 83	syl	$⊢ y \in (1 ..^N) \to y - 1 \in ℤ$
85	84	zcnd	$⊢ y \in (1 ..^N) \to y - 1 \in ℂ$
86	85	adantl	$⊢ (x \in ℤ \land y \in (1 ..^N)) \to y - 1 \in ℂ$
87	86	adantl	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to y - 1 \in ℂ$
88	76 87	addcomd	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to x \cdot N + y - 1 = y - 1 + x \cdot N$
89	82 88	eqtrd	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to x \cdot N + y - 1 = y - 1 + x \cdot N$
90	89	oveq1d	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to (x \cdot N + y - 1) \mod N = (y - 1 + x \cdot N) \mod N$
91	84	zred	$⊢ y \in (1 ..^N) \to y - 1 \in ℝ$
92	91	adantl	$⊢ (x \in ℤ \land y \in (1 ..^N)) \to y - 1 \in ℝ$
93	92	adantl	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to y - 1 \in ℝ$
94	7	adantr	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to N \in ℝ^{+}$
95		simprl	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to x \in ℤ$
96		modcyc	$⊢ (y - 1 \in ℝ \land N \in ℝ^{+} \land x \in ℤ) \to (y - 1 + x \cdot N) \mod N = (y - 1) \mod N$
97	93 94 95 96	syl3anc	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to (y - 1 + x \cdot N) \mod N = (y - 1) \mod N$
98	90 97	eqtrd	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to (x \cdot N + y - 1) \mod N = (y - 1) \mod N$
99	76 80	addcomd	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to x \cdot N + y = y + x \cdot N$
100	99	oveq1d	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to (x \cdot N + y) \mod N = (y + x \cdot N) \mod N$
101	77	zred	$⊢ y \in (1 ..^N) \to y \in ℝ$
102	101	adantl	$⊢ (x \in ℤ \land y \in (1 ..^N)) \to y \in ℝ$
103	102	adantl	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to y \in ℝ$
104		modcyc	$⊢ (y \in ℝ \land N \in ℝ^{+} \land x \in ℤ) \to (y + x \cdot N) \mod N = y \mod N$
105	103 94 95 104	syl3anc	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to (y + x \cdot N) \mod N = y \mod N$
106	7 102	anim12ci	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to (y \in ℝ \land N \in ℝ^{+})$
107		elfzole1	$⊢ y \in (1 ..^N) \to 1 \leq y$
108		0lt1	$⊢ 0 < 1$
109		0red	$⊢ y \in (1 ..^N) \to 0 \in ℝ$
110		1red	$⊢ y \in (1 ..^N) \to 1 \in ℝ$
111		ltleletr	$⊢ (0 \in ℝ \land 1 \in ℝ \land y \in ℝ) \to ((0 < 1 \land 1 \leq y) \to 0 \leq y)$
112	109 110 101 111	syl3anc	$⊢ y \in (1 ..^N) \to ((0 < 1 \land 1 \leq y) \to 0 \leq y)$
113	108 112	mpani	$⊢ y \in (1 ..^N) \to (1 \leq y \to 0 \leq y)$
114	107 113	mpd	$⊢ y \in (1 ..^N) \to 0 \leq y$
115		elfzolt2	$⊢ y \in (1 ..^N) \to y < N$
116	114 115	jca	$⊢ y \in (1 ..^N) \to (0 \leq y \land y < N)$
117	116	adantl	$⊢ (x \in ℤ \land y \in (1 ..^N)) \to (0 \leq y \land y < N)$
118	117	adantl	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to (0 \leq y \land y < N)$
119	106 118	jca	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to ((y \in ℝ \land N \in ℝ^{+}) \land (0 \leq y \land y < N))$
120		modid	$⊢ ((y \in ℝ \land N \in ℝ^{+}) \land (0 \leq y \land y < N)) \to y \mod N = y$
121	119 120	syl	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to y \mod N = y$
122	100 105 121	3eqtrd	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to (x \cdot N + y) \mod N = y$
123	98 122	oveq12d	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to ((x \cdot N + y - 1) \mod N) - ((x \cdot N + y) \mod N) = ((y - 1) \mod N) - y$
124	74 123	sylan9eqr	$⊢ (((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \land A = x \cdot N + y) \to ((A - 1) \mod N) - (A \mod N) = ((y - 1) \mod N) - y$
125	7 92	anim12ci	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to (y - 1 \in ℝ \land N \in ℝ^{+})$
126		elfzo2	$⊢ y \in (1 ..^N) \leftrightarrow (y \in ℤ_{\geq 1} \land N \in ℤ \land y < N)$
127		eluz2	$⊢ y \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land y \in ℤ \land 1 \leq y)$
128		zre	$⊢ y \in ℤ \to y \in ℝ$
129		zre	$⊢ 1 \in ℤ \to 1 \in ℝ$
130		subge0	$⊢ (y \in ℝ \land 1 \in ℝ) \to (0 \leq y - 1 \leftrightarrow 1 \leq y)$
131	128 129 130	syl2anr	$⊢ (1 \in ℤ \land y \in ℤ) \to (0 \leq y - 1 \leftrightarrow 1 \leq y)$
132	131	biimp3ar	$⊢ (1 \in ℤ \land y \in ℤ \land 1 \leq y) \to 0 \leq y - 1$
133	127 132	sylbi	$⊢ y \in ℤ_{\geq 1} \to 0 \leq y - 1$
134	133	3ad2ant1	$⊢ (y \in ℤ_{\geq 1} \land N \in ℤ \land y < N) \to 0 \leq y - 1$
135	126 134	sylbi	$⊢ y \in (1 ..^N) \to 0 \leq y - 1$
136	135	adantl	$⊢ (x \in ℤ \land y \in (1 ..^N)) \to 0 \leq y - 1$
137	136	adantl	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to 0 \leq y - 1$
138		eluzelz	$⊢ y \in ℤ_{\geq 1} \to y \in ℤ$
139	138	zred	$⊢ y \in ℤ_{\geq 1} \to y \in ℝ$
140		zre	$⊢ N \in ℤ \to N \in ℝ$
141		ltle	$⊢ (y \in ℝ \land N \in ℝ) \to (y < N \to y \leq N)$
142	139 140 141	syl2an	$⊢ (y \in ℤ_{\geq 1} \land N \in ℤ) \to (y < N \to y \leq N)$
143	142	3impia	$⊢ (y \in ℤ_{\geq 1} \land N \in ℤ \land y < N) \to y \leq N$
144	138	anim1i	$⊢ (y \in ℤ_{\geq 1} \land N \in ℤ) \to (y \in ℤ \land N \in ℤ)$
145	144	3adant3	$⊢ (y \in ℤ_{\geq 1} \land N \in ℤ \land y < N) \to (y \in ℤ \land N \in ℤ)$
146		zlem1lt	$⊢ (y \in ℤ \land N \in ℤ) \to (y \leq N \leftrightarrow y - 1 < N)$
147	145 146	syl	$⊢ (y \in ℤ_{\geq 1} \land N \in ℤ \land y < N) \to (y \leq N \leftrightarrow y - 1 < N)$
148	143 147	mpbid	$⊢ (y \in ℤ_{\geq 1} \land N \in ℤ \land y < N) \to y - 1 < N$
149	148	a1d	$⊢ (y \in ℤ_{\geq 1} \land N \in ℤ \land y < N) \to ((A \in ℤ \land N \in ℕ) \to y - 1 < N)$
150	126 149	sylbi	$⊢ y \in (1 ..^N) \to ((A \in ℤ \land N \in ℕ) \to y - 1 < N)$
151	150	adantl	$⊢ (x \in ℤ \land y \in (1 ..^N)) \to ((A \in ℤ \land N \in ℕ) \to y - 1 < N)$
152	151	impcom	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to y - 1 < N$
153		modid	$⊢ ((y - 1 \in ℝ \land N \in ℝ^{+}) \land (0 \leq y - 1 \land y - 1 < N)) \to (y - 1) \mod N = y - 1$
154	125 137 152 153	syl12anc	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to (y - 1) \mod N = y - 1$
155	154	oveq1d	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to ((y - 1) \mod N) - y = y - 1 - y$
156		1cnd	$⊢ y \in (1 ..^N) \to 1 \in ℂ$
157	78 156 78	sub32d	$⊢ y \in (1 ..^N) \to y - 1 - y = y - y - 1$
158	78	subidd	$⊢ y \in (1 ..^N) \to y - y = 0$
159	158	oveq1d	$⊢ y \in (1 ..^N) \to y - y - 1 = 0 - 1$
160	157 159	eqtrd	$⊢ y \in (1 ..^N) \to y - 1 - y = 0 - 1$
161	160	adantl	$⊢ (x \in ℤ \land y \in (1 ..^N)) \to y - 1 - y = 0 - 1$
162	161	adantl	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to y - 1 - y = 0 - 1$
163		df-neg	$⊢ - 1 = 0 - 1$
164	162 163	eqtr4di	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to y - 1 - y = - 1$
165	155 164	eqtrd	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to ((y - 1) \mod N) - y = - 1$
166	165	adantr	$⊢ (((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \land A = x \cdot N + y) \to ((y - 1) \mod N) - y = - 1$
167	124 166	eqtrd	$⊢ (((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \land A = x \cdot N + y) \to ((A - 1) \mod N) - (A \mod N) = - 1$
168	167	eqcomd	$⊢ (((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \land A = x \cdot N + y) \to - 1 = ((A - 1) \mod N) - (A \mod N)$
169	168	ex	$⊢ ((A \in ℤ \land N \in ℕ) \land (x \in ℤ \land y \in (1 ..^N))) \to (A = x \cdot N + y \to - 1 = ((A - 1) \mod N) - (A \mod N))$
170	169	rexlimdvva	$⊢ (A \in ℤ \land N \in ℕ) \to (\exists x \in ℤ \exists y \in (1 ..^N) A = x \cdot N + y \to - 1 = ((A - 1) \mod N) - (A \mod N))$
171	70 170	syld	$⊢ (A \in ℤ \land N \in ℕ) \to (A \mod N \neq 0 \to - 1 = ((A - 1) \mod N) - (A \mod N))$
172	69 171	biimtrrid	$⊢ (A \in ℤ \land N \in ℕ) \to (\neg A \mod N = 0 \to - 1 = ((A - 1) \mod N) - (A \mod N))$
173	172	imp	$⊢ ((A \in ℤ \land N \in ℕ) \land \neg A \mod N = 0) \to - 1 = ((A - 1) \mod N) - (A \mod N)$
174	68 173	ifeqda	$⊢ (A \in ℤ \land N \in ℕ) \to if (A \mod N = 0, N - 1, - 1) = ((A - 1) \mod N) - (A \mod N)$
175	174	eqcomd	$⊢ (A \in ℤ \land N \in ℕ) \to ((A - 1) \mod N) - (A \mod N) = if (A \mod N = 0, N - 1, - 1)$

Metamath Proof Explorer

Theorem m1modmmod

Proof