modsumfzodifsn

Description: The sum of a number within a half-open range of positive integers is an element of the corresponding open range of nonnegative integers with one excluded integer modulo the excluded integer. (Contributed by AV, 19-Mar-2021)

		Ref	Expression
	Assertion	modsumfzodifsn	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to (K + J) \mod N \in ((0 ..^N) ∖ \{J\})$

Proof

Step	Hyp	Ref	Expression
1		elfzo0	$⊢ J \in (0 ..^N) \leftrightarrow (J \in ℕ_{0} \land N \in ℕ \land J < N)$
2		elfzoelz	$⊢ K \in (1 ..^N) \to K \in ℤ$
3	2	zred	$⊢ K \in (1 ..^N) \to K \in ℝ$
4		nn0re	$⊢ J \in ℕ_{0} \to J \in ℝ$
5	4	3ad2ant1	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to J \in ℝ$
6		readdcl	$⊢ (K \in ℝ \land J \in ℝ) \to K + J \in ℝ$
7	3 5 6	syl2anr	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land K \in (1 ..^N)) \to K + J \in ℝ$
8		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
9	8	3ad2ant2	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to N \in ℝ^{+}$
10	9	adantr	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land K \in (1 ..^N)) \to N \in ℝ^{+}$
11	7 10	jca	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land K \in (1 ..^N)) \to (K + J \in ℝ \land N \in ℝ^{+})$
12	1 11	sylanb	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to (K + J \in ℝ \land N \in ℝ^{+})$
13	12	adantl	$⊢ (K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to (K + J \in ℝ \land N \in ℝ^{+})$
14		elfzo1	$⊢ K \in (1 ..^N) \leftrightarrow (K \in ℕ \land N \in ℕ \land K < N)$
15		nnnn0	$⊢ K \in ℕ \to K \in ℕ_{0}$
16	15	3ad2ant1	$⊢ (K \in ℕ \land N \in ℕ \land K < N) \to K \in ℕ_{0}$
17	14 16	sylbi	$⊢ K \in (1 ..^N) \to K \in ℕ_{0}$
18		elfzonn0	$⊢ J \in (0 ..^N) \to J \in ℕ_{0}$
19		nn0addcl	$⊢ (K \in ℕ_{0} \land J \in ℕ_{0}) \to K + J \in ℕ_{0}$
20	17 18 19	syl2anr	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K + J \in ℕ_{0}$
21	20	adantl	$⊢ (K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J \in ℕ_{0}$
22	21	nn0ge0d	$⊢ (K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to 0 \leq K + J$
23		simpl	$⊢ (K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J < N$
24		modid	$⊢ ((K + J \in ℝ \land N \in ℝ^{+}) \land (0 \leq K + J \land K + J < N)) \to (K + J) \mod N = K + J$
25	13 22 23 24	syl12anc	$⊢ (K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to (K + J) \mod N = K + J$
26		simp2	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to N \in ℕ$
27	1 26	sylbi	$⊢ J \in (0 ..^N) \to N \in ℕ$
28	27	adantr	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to N \in ℕ$
29	28	adantl	$⊢ (K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to N \in ℕ$
30		elfzo0	$⊢ K + J \in (0 ..^N) \leftrightarrow (K + J \in ℕ_{0} \land N \in ℕ \land K + J < N)$
31	21 29 23 30	syl3anbrc	$⊢ (K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J \in (0 ..^N)$
32	2	zcnd	$⊢ K \in (1 ..^N) \to K \in ℂ$
33	32	adantl	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K \in ℂ$
34		0cnd	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to 0 \in ℂ$
35		elfzoelz	$⊢ J \in (0 ..^N) \to J \in ℤ$
36	35	zcnd	$⊢ J \in (0 ..^N) \to J \in ℂ$
37	36	adantr	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to J \in ℂ$
38		nnne0	$⊢ K \in ℕ \to K \neq 0$
39	38	3ad2ant1	$⊢ (K \in ℕ \land N \in ℕ \land K < N) \to K \neq 0$
40	14 39	sylbi	$⊢ K \in (1 ..^N) \to K \neq 0$
41	40	adantl	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K \neq 0$
42	33 34 37 41	addneintr2d	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K + J \neq 0 + J$
43	42	adantl	$⊢ (K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J \neq 0 + J$
44	37	adantl	$⊢ (K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to J \in ℂ$
45		addid2	$⊢ J \in ℂ \to 0 + J = J$
46	45	eqcomd	$⊢ J \in ℂ \to J = 0 + J$
47	44 46	syl	$⊢ (K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to J = 0 + J$
48	43 47	neeqtrrd	$⊢ (K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J \neq J$
49		eldifsn	$⊢ K + J \in ((0 ..^N) ∖ \{J\}) \leftrightarrow (K + J \in (0 ..^N) \land K + J \neq J)$
50	31 48 49	sylanbrc	$⊢ (K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J \in ((0 ..^N) ∖ \{J\})$
51	25 50	eqeltrd	$⊢ (K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to (K + J) \mod N \in ((0 ..^N) ∖ \{J\})$
52		elfzoel2	$⊢ J \in (0 ..^N) \to N \in ℤ$
53	52	zcnd	$⊢ J \in (0 ..^N) \to N \in ℂ$
54	53	adantr	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to N \in ℂ$
55	54	adantl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to N \in ℂ$
56	55	mulm1d	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to -1 \cdot N = - N$
57	56	oveq2d	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J + -1 \cdot N = K + J + -N$
58		zaddcl	$⊢ (K \in ℤ \land J \in ℤ) \to K + J \in ℤ$
59	2 35 58	syl2anr	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K + J \in ℤ$
60	59	zcnd	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K + J \in ℂ$
61	60 54	jca	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to (K + J \in ℂ \land N \in ℂ)$
62	61	adantl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to (K + J \in ℂ \land N \in ℂ)$
63		negsub	$⊢ (K + J \in ℂ \land N \in ℂ) \to K + J + -N = K + J - N$
64	62 63	syl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J + -N = K + J - N$
65	57 64	eqtrd	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J + -1 \cdot N = K + J - N$
66	65	oveq1d	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to (K + J + -1 \cdot N) \mod N = (K + J - N) \mod N$
67	2 35 58	syl2an	$⊢ (K \in (1 ..^N) \land J \in (0 ..^N)) \to K + J \in ℤ$
68	67	zred	$⊢ (K \in (1 ..^N) \land J \in (0 ..^N)) \to K + J \in ℝ$
69	68	ancoms	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K + J \in ℝ$
70	52	zred	$⊢ J \in (0 ..^N) \to N \in ℝ$
71	70	adantr	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to N \in ℝ$
72	69 71	resubcld	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K + J - N \in ℝ$
73	72	adantl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J - N \in ℝ$
74	26	nnrpd	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to N \in ℝ^{+}$
75	1 74	sylbi	$⊢ J \in (0 ..^N) \to N \in ℝ^{+}$
76	75	adantr	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to N \in ℝ^{+}$
77	76	adantl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to N \in ℝ^{+}$
78		nnre	$⊢ K \in ℕ \to K \in ℝ$
79	78	3ad2ant1	$⊢ (K \in ℕ \land N \in ℕ \land K < N) \to K \in ℝ$
80	79	adantl	$⊢ ((J \in ℕ_{0} \land J < N) \land (K \in ℕ \land N \in ℕ \land K < N)) \to K \in ℝ$
81	4	adantr	$⊢ (J \in ℕ_{0} \land J < N) \to J \in ℝ$
82	81	adantr	$⊢ ((J \in ℕ_{0} \land J < N) \land (K \in ℕ \land N \in ℕ \land K < N)) \to J \in ℝ$
83		nnre	$⊢ N \in ℕ \to N \in ℝ$
84	83	3ad2ant2	$⊢ (K \in ℕ \land N \in ℕ \land K < N) \to N \in ℝ$
85	84	adantl	$⊢ ((J \in ℕ_{0} \land J < N) \land (K \in ℕ \land N \in ℕ \land K < N)) \to N \in ℝ$
86		simp3	$⊢ (K \in ℝ \land J \in ℝ \land N \in ℝ) \to N \in ℝ$
87	6	3adant3	$⊢ (K \in ℝ \land J \in ℝ \land N \in ℝ) \to K + J \in ℝ$
88	86 87	lenltd	$⊢ (K \in ℝ \land J \in ℝ \land N \in ℝ) \to (N \leq K + J \leftrightarrow \neg K + J < N)$
89	88	biimprd	$⊢ (K \in ℝ \land J \in ℝ \land N \in ℝ) \to (\neg K + J < N \to N \leq K + J)$
90	87 86	subge0d	$⊢ (K \in ℝ \land J \in ℝ \land N \in ℝ) \to (0 \leq K + J - N \leftrightarrow N \leq K + J)$
91	89 90	sylibrd	$⊢ (K \in ℝ \land J \in ℝ \land N \in ℝ) \to (\neg K + J < N \to 0 \leq K + J - N)$
92	80 82 85 91	syl3anc	$⊢ ((J \in ℕ_{0} \land J < N) \land (K \in ℕ \land N \in ℕ \land K < N)) \to (\neg K + J < N \to 0 \leq K + J - N)$
93	81 79	anim12ci	$⊢ ((J \in ℕ_{0} \land J < N) \land (K \in ℕ \land N \in ℕ \land K < N)) \to (K \in ℝ \land J \in ℝ)$
94	83 83	jca	$⊢ N \in ℕ \to (N \in ℝ \land N \in ℝ)$
95	94	3ad2ant2	$⊢ (K \in ℕ \land N \in ℕ \land K < N) \to (N \in ℝ \land N \in ℝ)$
96	95	adantl	$⊢ ((J \in ℕ_{0} \land J < N) \land (K \in ℕ \land N \in ℕ \land K < N)) \to (N \in ℝ \land N \in ℝ)$
97		simpr	$⊢ (J \in ℕ_{0} \land J < N) \to J < N$
98		simp3	$⊢ (K \in ℕ \land N \in ℕ \land K < N) \to K < N$
99	97 98	anim12ci	$⊢ ((J \in ℕ_{0} \land J < N) \land (K \in ℕ \land N \in ℕ \land K < N)) \to (K < N \land J < N)$
100	93 96 99	jca31	$⊢ ((J \in ℕ_{0} \land J < N) \land (K \in ℕ \land N \in ℕ \land K < N)) \to (((K \in ℝ \land J \in ℝ) \land (N \in ℝ \land N \in ℝ)) \land (K < N \land J < N))$
101		lt2add	$⊢ ((K \in ℝ \land J \in ℝ) \land (N \in ℝ \land N \in ℝ)) \to ((K < N \land J < N) \to K + J < N + N)$
102	101	imp	$⊢ (((K \in ℝ \land J \in ℝ) \land (N \in ℝ \land N \in ℝ)) \land (K < N \land J < N)) \to K + J < N + N$
103	100 102	syl	$⊢ ((J \in ℕ_{0} \land J < N) \land (K \in ℕ \land N \in ℕ \land K < N)) \to K + J < N + N$
104	79 81 6	syl2anr	$⊢ ((J \in ℕ_{0} \land J < N) \land (K \in ℕ \land N \in ℕ \land K < N)) \to K + J \in ℝ$
105		ltsubadd	$⊢ (K + J \in ℝ \land N \in ℝ \land N \in ℝ) \to (K + J - N < N \leftrightarrow K + J < N + N)$
106	104 85 85 105	syl3anc	$⊢ ((J \in ℕ_{0} \land J < N) \land (K \in ℕ \land N \in ℕ \land K < N)) \to (K + J - N < N \leftrightarrow K + J < N + N)$
107	103 106	mpbird	$⊢ ((J \in ℕ_{0} \land J < N) \land (K \in ℕ \land N \in ℕ \land K < N)) \to K + J - N < N$
108	92 107	jctird	$⊢ ((J \in ℕ_{0} \land J < N) \land (K \in ℕ \land N \in ℕ \land K < N)) \to (\neg K + J < N \to (0 \leq K + J - N \land K + J - N < N))$
109	108	ex	$⊢ (J \in ℕ_{0} \land J < N) \to ((K \in ℕ \land N \in ℕ \land K < N) \to (\neg K + J < N \to (0 \leq K + J - N \land K + J - N < N)))$
110	14 109	syl5bi	$⊢ (J \in ℕ_{0} \land J < N) \to (K \in (1 ..^N) \to (\neg K + J < N \to (0 \leq K + J - N \land K + J - N < N)))$
111	110	3adant2	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (K \in (1 ..^N) \to (\neg K + J < N \to (0 \leq K + J - N \land K + J - N < N)))$
112	1 111	sylbi	$⊢ J \in (0 ..^N) \to (K \in (1 ..^N) \to (\neg K + J < N \to (0 \leq K + J - N \land K + J - N < N)))$
113	112	imp	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to (\neg K + J < N \to (0 \leq K + J - N \land K + J - N < N))$
114	113	impcom	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to (0 \leq K + J - N \land K + J - N < N)$
115	73 77 114	jca31	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to ((K + J - N \in ℝ \land N \in ℝ^{+}) \land (0 \leq K + J - N \land K + J - N < N))$
116		modid	$⊢ ((K + J - N \in ℝ \land N \in ℝ^{+}) \land (0 \leq K + J - N \land K + J - N < N)) \to (K + J - N) \mod N = K + J - N$
117	115 116	syl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to (K + J - N) \mod N = K + J - N$
118	66 117	eqtrd	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to (K + J + -1 \cdot N) \mod N = K + J - N$
119	118	eqcomd	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J - N = (K + J + -1 \cdot N) \mod N$
120	1 9	sylbi	$⊢ J \in (0 ..^N) \to N \in ℝ^{+}$
121	120	adantr	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to N \in ℝ^{+}$
122		neg1z	$⊢ - 1 \in ℤ$
123	122	a1i	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to - 1 \in ℤ$
124		modcyc	$⊢ (K + J \in ℝ \land N \in ℝ^{+} \land - 1 \in ℤ) \to (K + J + -1 \cdot N) \mod N = (K + J) \mod N$
125	69 121 123 124	syl2an23an	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to (K + J + -1 \cdot N) \mod N = (K + J) \mod N$
126	119 125	eqtrd	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J - N = (K + J) \mod N$
127	126	eqcomd	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to (K + J) \mod N = K + J - N$
128	52	adantr	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to N \in ℤ$
129	59 128	zsubcld	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K + J - N \in ℤ$
130	129	adantl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J - N \in ℤ$
131	3	adantl	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K \in ℝ$
132	35	zred	$⊢ J \in (0 ..^N) \to J \in ℝ$
133	132	adantr	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to J \in ℝ$
134	90	biimprd	$⊢ (K \in ℝ \land J \in ℝ \land N \in ℝ) \to (N \leq K + J \to 0 \leq K + J - N)$
135	88 134	sylbird	$⊢ (K \in ℝ \land J \in ℝ \land N \in ℝ) \to (\neg K + J < N \to 0 \leq K + J - N)$
136	131 133 71 135	syl3anc	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to (\neg K + J < N \to 0 \leq K + J - N)$
137	136	impcom	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to 0 \leq K + J - N$
138		elnn0z	$⊢ K + J - N \in ℕ_{0} \leftrightarrow (K + J - N \in ℤ \land 0 \leq K + J - N)$
139	130 137 138	sylanbrc	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J - N \in ℕ_{0}$
140	28	adantl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to N \in ℕ$
141	100	expcom	$⊢ (K \in ℕ \land N \in ℕ \land K < N) \to ((J \in ℕ_{0} \land J < N) \to (((K \in ℝ \land J \in ℝ) \land (N \in ℝ \land N \in ℝ)) \land (K < N \land J < N)))$
142	14 141	sylbi	$⊢ K \in (1 ..^N) \to ((J \in ℕ_{0} \land J < N) \to (((K \in ℝ \land J \in ℝ) \land (N \in ℝ \land N \in ℝ)) \land (K < N \land J < N)))$
143	142	com12	$⊢ (J \in ℕ_{0} \land J < N) \to (K \in (1 ..^N) \to (((K \in ℝ \land J \in ℝ) \land (N \in ℝ \land N \in ℝ)) \land (K < N \land J < N)))$
144	143	3adant2	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (K \in (1 ..^N) \to (((K \in ℝ \land J \in ℝ) \land (N \in ℝ \land N \in ℝ)) \land (K < N \land J < N)))$
145	1 144	sylbi	$⊢ J \in (0 ..^N) \to (K \in (1 ..^N) \to (((K \in ℝ \land J \in ℝ) \land (N \in ℝ \land N \in ℝ)) \land (K < N \land J < N)))$
146	145	imp	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to (((K \in ℝ \land J \in ℝ) \land (N \in ℝ \land N \in ℝ)) \land (K < N \land J < N))$
147	146 102	syl	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K + J < N + N$
148	4	adantr	$⊢ (J \in ℕ_{0} \land N \in ℕ) \to J \in ℝ$
149	3 148 6	syl2anr	$⊢ ((J \in ℕ_{0} \land N \in ℕ) \land K \in (1 ..^N)) \to K + J \in ℝ$
150	83	adantl	$⊢ (J \in ℕ_{0} \land N \in ℕ) \to N \in ℝ$
151	150	adantr	$⊢ ((J \in ℕ_{0} \land N \in ℕ) \land K \in (1 ..^N)) \to N \in ℝ$
152	149 151 151	3jca	$⊢ ((J \in ℕ_{0} \land N \in ℕ) \land K \in (1 ..^N)) \to (K + J \in ℝ \land N \in ℝ \land N \in ℝ)$
153	152	ex	$⊢ (J \in ℕ_{0} \land N \in ℕ) \to (K \in (1 ..^N) \to (K + J \in ℝ \land N \in ℝ \land N \in ℝ))$
154	153	3adant3	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (K \in (1 ..^N) \to (K + J \in ℝ \land N \in ℝ \land N \in ℝ))$
155	1 154	sylbi	$⊢ J \in (0 ..^N) \to (K \in (1 ..^N) \to (K + J \in ℝ \land N \in ℝ \land N \in ℝ))$
156	155	imp	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to (K + J \in ℝ \land N \in ℝ \land N \in ℝ)$
157	156 105	syl	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to (K + J - N < N \leftrightarrow K + J < N + N)$
158	147 157	mpbird	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K + J - N < N$
159	158	adantl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J - N < N$
160		elfzo0	$⊢ K + J - N \in (0 ..^N) \leftrightarrow (K + J - N \in ℕ_{0} \land N \in ℕ \land K + J - N < N)$
161	139 140 159 160	syl3anbrc	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J - N \in (0 ..^N)$
162		nncn	$⊢ K \in ℕ \to K \in ℂ$
163		nncn	$⊢ N \in ℕ \to N \in ℂ$
164		subcl	$⊢ (K \in ℂ \land N \in ℂ) \to K - N \in ℂ$
165	162 163 164	syl2an	$⊢ (K \in ℕ \land N \in ℕ) \to K - N \in ℂ$
166	165	3adant3	$⊢ (K \in ℕ \land N \in ℕ \land K < N) \to K - N \in ℂ$
167	14 166	sylbi	$⊢ K \in (1 ..^N) \to K - N \in ℂ$
168	167	adantl	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K - N \in ℂ$
169	168	adantl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K - N \in ℂ$
170		0cnd	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to 0 \in ℂ$
171	37	adantl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to J \in ℂ$
172		elfzoel2	$⊢ K \in (1 ..^N) \to N \in ℤ$
173	172	zcnd	$⊢ K \in (1 ..^N) \to N \in ℂ$
174	79 98	ltned	$⊢ (K \in ℕ \land N \in ℕ \land K < N) \to K \neq N$
175	14 174	sylbi	$⊢ K \in (1 ..^N) \to K \neq N$
176	32 173 175	subne0d	$⊢ K \in (1 ..^N) \to K - N \neq 0$
177	176	adantl	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to K - N \neq 0$
178	177	adantl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K - N \neq 0$
179	169 170 171 178	addneintr2d	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K - N + J \neq 0 + J$
180	33 37 54	3jca	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to (K \in ℂ \land J \in ℂ \land N \in ℂ)$
181	180	adantl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to (K \in ℂ \land J \in ℂ \land N \in ℂ)$
182		addsub	$⊢ (K \in ℂ \land J \in ℂ \land N \in ℂ) \to K + J - N = K - N + J$
183	181 182	syl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J - N = K - N + J$
184	171 45	syl	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to 0 + J = J$
185	184	eqcomd	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to J = 0 + J$
186	179 183 185	3netr4d	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J - N \neq J$
187		eldifsn	$⊢ K + J - N \in ((0 ..^N) ∖ \{J\}) \leftrightarrow (K + J - N \in (0 ..^N) \land K + J - N \neq J)$
188	161 186 187	sylanbrc	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to K + J - N \in ((0 ..^N) ∖ \{J\})$
189	127 188	eqeltrd	$⊢ (\neg K + J < N \land (J \in (0 ..^N) \land K \in (1 ..^N))) \to (K + J) \mod N \in ((0 ..^N) ∖ \{J\})$
190	51 189	pm2.61ian	$⊢ (J \in (0 ..^N) \land K \in (1 ..^N)) \to (K + J) \mod N \in ((0 ..^N) ∖ \{J\})$

Metamath Proof Explorer

Theorem modsumfzodifsn

Proof