modfzo0difsn

Description: For a number within a half-open range of nonnegative integers with one excluded integer there is a positive integer so that the number is equal to the sum of the positive integer and the excluded integer modulo the upper bound of the range. (Contributed by AV, 19-Mar-2021)

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

Proof

Step	Hyp	Ref	Expression
1		eldifi	$⊢ K \in ((0 ..^N) ∖ \{J\}) \to K \in (0 ..^N)$
2		elfzoelz	$⊢ K \in (0 ..^N) \to K \in ℤ$
3	2	zred	$⊢ K \in (0 ..^N) \to K \in ℝ$
4	1 3	syl	$⊢ K \in ((0 ..^N) ∖ \{J\}) \to K \in ℝ$
5		elfzoelz	$⊢ J \in (0 ..^N) \to J \in ℤ$
6	5	zred	$⊢ J \in (0 ..^N) \to J \in ℝ$
7		leloe	$⊢ (K \in ℝ \land J \in ℝ) \to (K \leq J \leftrightarrow (K < J \lor K = J))$
8	4 6 7	syl2anr	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to (K \leq J \leftrightarrow (K < J \lor K = J))$
9		elfzo0	$⊢ K \in (0 ..^N) \leftrightarrow (K \in ℕ_{0} \land N \in ℕ \land K < N)$
10		elfzo0	$⊢ J \in (0 ..^N) \leftrightarrow (J \in ℕ_{0} \land N \in ℕ \land J < N)$
11		nn0cn	$⊢ K \in ℕ_{0} \to K \in ℂ$
12	11	adantr	$⊢ (K \in ℕ_{0} \land K < N) \to K \in ℂ$
13	12	adantl	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to K \in ℂ$
14		nn0cn	$⊢ J \in ℕ_{0} \to J \in ℂ$
15	14	3ad2ant1	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to J \in ℂ$
16	15	adantr	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to J \in ℂ$
17		nncn	$⊢ N \in ℕ \to N \in ℂ$
18	17	3ad2ant2	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to N \in ℂ$
19	18	adantr	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to N \in ℂ$
20	13 16 19	subadd23d	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to K - J + N = K + N - J$
21		simpl	$⊢ (K \in ℕ_{0} \land K < N) \to K \in ℕ_{0}$
22		nn0z	$⊢ J \in ℕ_{0} \to J \in ℤ$
23		nnz	$⊢ N \in ℕ \to N \in ℤ$
24		znnsub	$⊢ (J \in ℤ \land N \in ℤ) \to (J < N \leftrightarrow N - J \in ℕ)$
25	22 23 24	syl2an	$⊢ (J \in ℕ_{0} \land N \in ℕ) \to (J < N \leftrightarrow N - J \in ℕ)$
26	25	biimp3a	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to N - J \in ℕ$
27		nn0nnaddcl	$⊢ (K \in ℕ_{0} \land N - J \in ℕ) \to K + N - J \in ℕ$
28	21 26 27	syl2anr	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to K + N - J \in ℕ$
29	20 28	eqeltrd	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to K - J + N \in ℕ$
30	29	adantr	$⊢ (((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \land K < J) \to K - J + N \in ℕ$
31		simp2	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to N \in ℕ$
32	31	adantr	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to N \in ℕ$
33	32	adantr	$⊢ (((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \land K < J) \to N \in ℕ$
34		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
35	34	adantr	$⊢ (K \in ℕ_{0} \land K < N) \to K \in ℝ$
36	35	adantl	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to K \in ℝ$
37		nn0re	$⊢ J \in ℕ_{0} \to J \in ℝ$
38	37	3ad2ant1	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to J \in ℝ$
39	38	adantr	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to J \in ℝ$
40	36 39	sublt0d	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to (K - J < 0 \leftrightarrow K < J)$
41	40	bicomd	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to (K < J \leftrightarrow K - J < 0)$
42	41	biimpa	$⊢ (((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \land K < J) \to K - J < 0$
43		resubcl	$⊢ (K \in ℝ \land J \in ℝ) \to K - J \in ℝ$
44	35 38 43	syl2anr	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to K - J \in ℝ$
45		nnre	$⊢ N \in ℕ \to N \in ℝ$
46	45	3ad2ant2	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to N \in ℝ$
47	46	adantr	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to N \in ℝ$
48	44 47	jca	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \to (K - J \in ℝ \land N \in ℝ)$
49	48	adantr	$⊢ (((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \land K < J) \to (K - J \in ℝ \land N \in ℝ)$
50		ltaddnegr	$⊢ (K - J \in ℝ \land N \in ℝ) \to (K - J < 0 \leftrightarrow K - J + N < N)$
51	49 50	syl	$⊢ (((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \land K < J) \to (K - J < 0 \leftrightarrow K - J + N < N)$
52	42 51	mpbid	$⊢ (((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \land K < J) \to K - J + N < N$
53		elfzo1	$⊢ K - J + N \in (1 ..^N) \leftrightarrow (K - J + N \in ℕ \land N \in ℕ \land K - J + N < N)$
54	30 33 52 53	syl3anbrc	$⊢ (((J \in ℕ_{0} \land N \in ℕ \land J < N) \land (K \in ℕ_{0} \land K < N)) \land K < J) \to K - J + N \in (1 ..^N)$
55	54	exp31	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to ((K \in ℕ_{0} \land K < N) \to (K < J \to K - J + N \in (1 ..^N)))$
56	10 55	sylbi	$⊢ J \in (0 ..^N) \to ((K \in ℕ_{0} \land K < N) \to (K < J \to K - J + N \in (1 ..^N)))$
57	56	com12	$⊢ (K \in ℕ_{0} \land K < N) \to (J \in (0 ..^N) \to (K < J \to K - J + N \in (1 ..^N)))$
58	57	3adant2	$⊢ (K \in ℕ_{0} \land N \in ℕ \land K < N) \to (J \in (0 ..^N) \to (K < J \to K - J + N \in (1 ..^N)))$
59	9 58	sylbi	$⊢ K \in (0 ..^N) \to (J \in (0 ..^N) \to (K < J \to K - J + N \in (1 ..^N)))$
60	1 59	syl	$⊢ K \in ((0 ..^N) ∖ \{J\}) \to (J \in (0 ..^N) \to (K < J \to K - J + N \in (1 ..^N)))$
61	60	impcom	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to (K < J \to K - J + N \in (1 ..^N))$
62	61	impcom	$⊢ (K < J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \to K - J + N \in (1 ..^N)$
63		oveq1	$⊢ i = K - J + N \to i + J = (K - J) + N + J$
64	2	zcnd	$⊢ K \in (0 ..^N) \to K \in ℂ$
65	64	adantr	$⊢ (K \in (0 ..^N) \land (J \in ℕ_{0} \land N \in ℕ)) \to K \in ℂ$
66	14	adantr	$⊢ (J \in ℕ_{0} \land N \in ℕ) \to J \in ℂ$
67	66	adantl	$⊢ (K \in (0 ..^N) \land (J \in ℕ_{0} \land N \in ℕ)) \to J \in ℂ$
68	17	adantl	$⊢ (J \in ℕ_{0} \land N \in ℕ) \to N \in ℂ$
69	68	adantl	$⊢ (K \in (0 ..^N) \land (J \in ℕ_{0} \land N \in ℕ)) \to N \in ℂ$
70	65 67 69	3jca	$⊢ (K \in (0 ..^N) \land (J \in ℕ_{0} \land N \in ℕ)) \to (K \in ℂ \land J \in ℂ \land N \in ℂ)$
71	70	ex	$⊢ K \in (0 ..^N) \to ((J \in ℕ_{0} \land N \in ℕ) \to (K \in ℂ \land J \in ℂ \land N \in ℂ))$
72	1 71	syl	$⊢ K \in ((0 ..^N) ∖ \{J\}) \to ((J \in ℕ_{0} \land N \in ℕ) \to (K \in ℂ \land J \in ℂ \land N \in ℂ))$
73	72	com12	$⊢ (J \in ℕ_{0} \land N \in ℕ) \to (K \in ((0 ..^N) ∖ \{J\}) \to (K \in ℂ \land J \in ℂ \land N \in ℂ))$
74	73	3adant3	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (K \in ((0 ..^N) ∖ \{J\}) \to (K \in ℂ \land J \in ℂ \land N \in ℂ))$
75	10 74	sylbi	$⊢ J \in (0 ..^N) \to (K \in ((0 ..^N) ∖ \{J\}) \to (K \in ℂ \land J \in ℂ \land N \in ℂ))$
76	75	imp	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to (K \in ℂ \land J \in ℂ \land N \in ℂ)$
77	76	adantl	$⊢ (K < J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \to (K \in ℂ \land J \in ℂ \land N \in ℂ)$
78		nppcan	$⊢ (K \in ℂ \land J \in ℂ \land N \in ℂ) \to (K - J) + N + J = K + N$
79	77 78	syl	$⊢ (K < J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \to (K - J) + N + J = K + N$
80	63 79	sylan9eqr	$⊢ ((K < J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \land i = K - J + N) \to i + J = K + N$
81	80	oveq1d	$⊢ ((K < J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \land i = K - J + N) \to (i + J) \mod N = (K + N) \mod N$
82	81	eqeq2d	$⊢ ((K < J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \land i = K - J + N) \to (K = (i + J) \mod N \leftrightarrow K = (K + N) \mod N)$
83	9	biimpi	$⊢ K \in (0 ..^N) \to (K \in ℕ_{0} \land N \in ℕ \land K < N)$
84	83	a1d	$⊢ K \in (0 ..^N) \to (J \in (0 ..^N) \to (K \in ℕ_{0} \land N \in ℕ \land K < N))$
85	1 84	syl	$⊢ K \in ((0 ..^N) ∖ \{J\}) \to (J \in (0 ..^N) \to (K \in ℕ_{0} \land N \in ℕ \land K < N))$
86	85	impcom	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to (K \in ℕ_{0} \land N \in ℕ \land K < N)$
87	86	adantl	$⊢ (K < J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \to (K \in ℕ_{0} \land N \in ℕ \land K < N)$
88		addmodidr	$⊢ (K \in ℕ_{0} \land N \in ℕ \land K < N) \to (K + N) \mod N = K$
89	88	eqcomd	$⊢ (K \in ℕ_{0} \land N \in ℕ \land K < N) \to K = (K + N) \mod N$
90	87 89	syl	$⊢ (K < J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \to K = (K + N) \mod N$
91	62 82 90	rspcedvd	$⊢ (K < J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \to \exists i \in (1 ..^N) K = (i + J) \mod N$
92	91	ex	$⊢ K < J \to ((J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to \exists i \in (1 ..^N) K = (i + J) \mod N)$
93		eldifsn	$⊢ K \in ((0 ..^N) ∖ \{J\}) \leftrightarrow (K \in (0 ..^N) \land K \neq J)$
94		eqneqall	$⊢ K = J \to (K \neq J \to \exists i \in (1 ..^N) K = (i + J) \mod N)$
95	94	com12	$⊢ K \neq J \to (K = J \to \exists i \in (1 ..^N) K = (i + J) \mod N)$
96	95	adantl	$⊢ (K \in (0 ..^N) \land K \neq J) \to (K = J \to \exists i \in (1 ..^N) K = (i + J) \mod N)$
97	93 96	sylbi	$⊢ K \in ((0 ..^N) ∖ \{J\}) \to (K = J \to \exists i \in (1 ..^N) K = (i + J) \mod N)$
98	97	adantl	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to (K = J \to \exists i \in (1 ..^N) K = (i + J) \mod N)$
99	98	com12	$⊢ K = J \to ((J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to \exists i \in (1 ..^N) K = (i + J) \mod N)$
100	92 99	jaoi	$⊢ (K < J \lor K = J) \to ((J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to \exists i \in (1 ..^N) K = (i + J) \mod N)$
101	100	com12	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to ((K < J \lor K = J) \to \exists i \in (1 ..^N) K = (i + J) \mod N)$
102	8 101	sylbid	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to (K \leq J \to \exists i \in (1 ..^N) K = (i + J) \mod N)$
103	102	com12	$⊢ K \leq J \to ((J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to \exists i \in (1 ..^N) K = (i + J) \mod N)$
104		ltnle	$⊢ (J \in ℝ \land K \in ℝ) \to (J < K \leftrightarrow \neg K \leq J)$
105	6 4 104	syl2an	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to (J < K \leftrightarrow \neg K \leq J)$
106	105	bicomd	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to (\neg K \leq J \leftrightarrow J < K)$
107	22	3ad2ant1	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to J \in ℤ$
108		nn0z	$⊢ K \in ℕ_{0} \to K \in ℤ$
109	108	adantr	$⊢ (K \in ℕ_{0} \land K < N) \to K \in ℤ$
110		znnsub	$⊢ (J \in ℤ \land K \in ℤ) \to (J < K \leftrightarrow K - J \in ℕ)$
111	107 109 110	syl2anr	$⊢ ((K \in ℕ_{0} \land K < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (J < K \leftrightarrow K - J \in ℕ)$
112	111	biimpa	$⊢ (((K \in ℕ_{0} \land K < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \land J < K) \to K - J \in ℕ$
113	31	adantl	$⊢ ((K \in ℕ_{0} \land K < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to N \in ℕ$
114	113	adantr	$⊢ (((K \in ℕ_{0} \land K < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \land J < K) \to N \in ℕ$
115		nn0ge0	$⊢ J \in ℕ_{0} \to 0 \leq J$
116	115	3ad2ant1	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to 0 \leq J$
117	116	adantl	$⊢ (K \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to 0 \leq J$
118		subge02	$⊢ (K \in ℝ \land J \in ℝ) \to (0 \leq J \leftrightarrow K - J \leq K)$
119	34 38 118	syl2an	$⊢ (K \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (0 \leq J \leftrightarrow K - J \leq K)$
120	117 119	mpbid	$⊢ (K \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to K - J \leq K$
121	38	adantl	$⊢ (K \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to J \in ℝ$
122	34	adantr	$⊢ (K \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to K \in ℝ$
123	46	adantl	$⊢ (K \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to N \in ℝ$
124	121 122 123	3jca	$⊢ (K \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (J \in ℝ \land K \in ℝ \land N \in ℝ)$
125	43	ancoms	$⊢ (J \in ℝ \land K \in ℝ) \to K - J \in ℝ$
126	125	3adant3	$⊢ (J \in ℝ \land K \in ℝ \land N \in ℝ) \to K - J \in ℝ$
127		simp2	$⊢ (J \in ℝ \land K \in ℝ \land N \in ℝ) \to K \in ℝ$
128		simp3	$⊢ (J \in ℝ \land K \in ℝ \land N \in ℝ) \to N \in ℝ$
129	126 127 128	3jca	$⊢ (J \in ℝ \land K \in ℝ \land N \in ℝ) \to (K - J \in ℝ \land K \in ℝ \land N \in ℝ)$
130	124 129	syl	$⊢ (K \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (K - J \in ℝ \land K \in ℝ \land N \in ℝ)$
131		lelttr	$⊢ (K - J \in ℝ \land K \in ℝ \land N \in ℝ) \to ((K - J \leq K \land K < N) \to K - J < N)$
132	130 131	syl	$⊢ (K \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to ((K - J \leq K \land K < N) \to K - J < N)$
133	120 132	mpand	$⊢ (K \in ℕ_{0} \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to (K < N \to K - J < N)$
134	133	impancom	$⊢ (K \in ℕ_{0} \land K < N) \to ((J \in ℕ_{0} \land N \in ℕ \land J < N) \to K - J < N)$
135	134	imp	$⊢ ((K \in ℕ_{0} \land K < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \to K - J < N$
136	135	adantr	$⊢ (((K \in ℕ_{0} \land K < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \land J < K) \to K - J < N$
137	112 114 136	3jca	$⊢ (((K \in ℕ_{0} \land K < N) \land (J \in ℕ_{0} \land N \in ℕ \land J < N)) \land J < K) \to (K - J \in ℕ \land N \in ℕ \land K - J < N)$
138	137	exp31	$⊢ (K \in ℕ_{0} \land K < N) \to ((J \in ℕ_{0} \land N \in ℕ \land J < N) \to (J < K \to (K - J \in ℕ \land N \in ℕ \land K - J < N)))$
139	138	3adant2	$⊢ (K \in ℕ_{0} \land N \in ℕ \land K < N) \to ((J \in ℕ_{0} \land N \in ℕ \land J < N) \to (J < K \to (K - J \in ℕ \land N \in ℕ \land K - J < N)))$
140	9 139	sylbi	$⊢ K \in (0 ..^N) \to ((J \in ℕ_{0} \land N \in ℕ \land J < N) \to (J < K \to (K - J \in ℕ \land N \in ℕ \land K - J < N)))$
141	1 140	syl	$⊢ K \in ((0 ..^N) ∖ \{J\}) \to ((J \in ℕ_{0} \land N \in ℕ \land J < N) \to (J < K \to (K - J \in ℕ \land N \in ℕ \land K - J < N)))$
142	141	com12	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (K \in ((0 ..^N) ∖ \{J\}) \to (J < K \to (K - J \in ℕ \land N \in ℕ \land K - J < N)))$
143	10 142	sylbi	$⊢ J \in (0 ..^N) \to (K \in ((0 ..^N) ∖ \{J\}) \to (J < K \to (K - J \in ℕ \land N \in ℕ \land K - J < N)))$
144	143	imp	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to (J < K \to (K - J \in ℕ \land N \in ℕ \land K - J < N))$
145	106 144	sylbid	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to (\neg K \leq J \to (K - J \in ℕ \land N \in ℕ \land K - J < N))$
146	145	impcom	$⊢ (\neg K \leq J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \to (K - J \in ℕ \land N \in ℕ \land K - J < N)$
147		elfzo1	$⊢ K - J \in (1 ..^N) \leftrightarrow (K - J \in ℕ \land N \in ℕ \land K - J < N)$
148	146 147	sylibr	$⊢ (\neg K \leq J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \to K - J \in (1 ..^N)$
149		oveq1	$⊢ i = K - J \to i + J = K - J + J$
150	1 64	syl	$⊢ K \in ((0 ..^N) ∖ \{J\}) \to K \in ℂ$
151	5	zcnd	$⊢ J \in (0 ..^N) \to J \in ℂ$
152		npcan	$⊢ (K \in ℂ \land J \in ℂ) \to K - J + J = K$
153	150 151 152	syl2anr	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to K - J + J = K$
154	153	adantl	$⊢ (\neg K \leq J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \to K - J + J = K$
155	149 154	sylan9eqr	$⊢ ((\neg K \leq J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \land i = K - J) \to i + J = K$
156	155	oveq1d	$⊢ ((\neg K \leq J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \land i = K - J) \to (i + J) \mod N = K \mod N$
157	156	eqeq2d	$⊢ ((\neg K \leq J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \land i = K - J) \to (K = (i + J) \mod N \leftrightarrow K = K \mod N)$
158		zmodidfzoimp	$⊢ K \in (0 ..^N) \to K \mod N = K$
159	1 158	syl	$⊢ K \in ((0 ..^N) ∖ \{J\}) \to K \mod N = K$
160	159	adantl	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to K \mod N = K$
161	160	adantl	$⊢ (\neg K \leq J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \to K \mod N = K$
162	161	eqcomd	$⊢ (\neg K \leq J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \to K = K \mod N$
163	148 157 162	rspcedvd	$⊢ (\neg K \leq J \land (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\}))) \to \exists i \in (1 ..^N) K = (i + J) \mod N$
164	163	ex	$⊢ \neg K \leq J \to ((J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to \exists i \in (1 ..^N) K = (i + J) \mod N)$
165	103 164	pm2.61i	$⊢ (J \in (0 ..^N) \land K \in ((0 ..^N) ∖ \{J\})) \to \exists i \in (1 ..^N) K = (i + J) \mod N$

Metamath Proof Explorer

Theorem modfzo0difsn

Proof