divalglem8

	Ref	Expression
Hypotheses	divalglem8.1	$⊢ N \in ℤ$
	divalglem8.2	$⊢ D \in ℤ$
	divalglem8.3	$⊢ D \neq 0$
	divalglem8.4	$⊢ S = \{r \in ℕ_{0} \| D ∥ (N - r)\}$
Assertion	divalglem8	$⊢ ((X \in S \land Y \in S) \land (X < \|D\| \land Y < \|D\|)) \to (K \in ℤ \to (K \|D\| = Y - X \to X = Y))$

Proof

Step	Hyp	Ref	Expression
1		divalglem8.1	$⊢ N \in ℤ$
2		divalglem8.2	$⊢ D \in ℤ$
3		divalglem8.3	$⊢ D \neq 0$
4		divalglem8.4	$⊢ S = \{r \in ℕ_{0} \| D ∥ (N - r)\}$
5	4	ssrab3	$⊢ S \subseteq ℕ_{0}$
6		nn0sscn	$⊢ ℕ_{0} \subseteq ℂ$
7	5 6	sstri	$⊢ S \subseteq ℂ$
8	7	sseli	$⊢ Y \in S \to Y \in ℂ$
9	7	sseli	$⊢ X \in S \to X \in ℂ$
10		nnabscl	$⊢ (D \in ℤ \land D \neq 0) \to \|D\| \in ℕ$
11	2 3 10	mp2an	$⊢ \|D\| \in ℕ$
12	11	nnzi	$⊢ \|D\| \in ℤ$
13		zmulcl	$⊢ (K \in ℤ \land \|D\| \in ℤ) \to K \|D\| \in ℤ$
14	12 13	mpan2	$⊢ K \in ℤ \to K \|D\| \in ℤ$
15	14	zcnd	$⊢ K \in ℤ \to K \|D\| \in ℂ$
16		subadd	$⊢ (Y \in ℂ \land X \in ℂ \land K \|D\| \in ℂ) \to (Y - X = K \|D\| \leftrightarrow X + K \|D\| = Y)$
17	8 9 15 16	syl3an	$⊢ (Y \in S \land X \in S \land K \in ℤ) \to (Y - X = K \|D\| \leftrightarrow X + K \|D\| = Y)$
18	17	3com12	$⊢ (X \in S \land Y \in S \land K \in ℤ) \to (Y - X = K \|D\| \leftrightarrow X + K \|D\| = Y)$
19		eqcom	$⊢ Y - X = K \|D\| \leftrightarrow K \|D\| = Y - X$
20		eqcom	$⊢ X + K \|D\| = Y \leftrightarrow Y = X + K \|D\|$
21	18 19 20	3bitr3g	$⊢ (X \in S \land Y \in S \land K \in ℤ) \to (K \|D\| = Y - X \leftrightarrow Y = X + K \|D\|)$
22	21	3adant1r	$⊢ ((X \in S \land X < \|D\|) \land Y \in S \land K \in ℤ) \to (K \|D\| = Y - X \leftrightarrow Y = X + K \|D\|)$
23	22	3adant2r	$⊢ ((X \in S \land X < \|D\|) \land (Y \in S \land Y < \|D\|) \land K \in ℤ) \to (K \|D\| = Y - X \leftrightarrow Y = X + K \|D\|)$
24		breq1	$⊢ z = Y \to (z < \|D\| \leftrightarrow Y < \|D\|)$
25		eleq1	$⊢ z = Y \to (z \in (0 \dots \|D\| - 1) \leftrightarrow Y \in (0 \dots \|D\| - 1))$
26	24 25	imbi12d	$⊢ z = Y \to ((z < \|D\| \to z \in (0 \dots \|D\| - 1)) \leftrightarrow (Y < \|D\| \to Y \in (0 \dots \|D\| - 1)))$
27	5	sseli	$⊢ z \in S \to z \in ℕ_{0}$
28		elnn0z	$⊢ z \in ℕ_{0} \leftrightarrow (z \in ℤ \land 0 \leq z)$
29	27 28	sylib	$⊢ z \in S \to (z \in ℤ \land 0 \leq z)$
30	29	anim1i	$⊢ (z \in S \land z < \|D\|) \to ((z \in ℤ \land 0 \leq z) \land z < \|D\|)$
31		df-3an	$⊢ (z \in ℤ \land 0 \leq z \land z < \|D\|) \leftrightarrow ((z \in ℤ \land 0 \leq z) \land z < \|D\|)$
32	30 31	sylibr	$⊢ (z \in S \land z < \|D\|) \to (z \in ℤ \land 0 \leq z \land z < \|D\|)$
33		0z	$⊢ 0 \in ℤ$
34		elfzm11	$⊢ (0 \in ℤ \land \|D\| \in ℤ) \to (z \in (0 \dots \|D\| - 1) \leftrightarrow (z \in ℤ \land 0 \leq z \land z < \|D\|))$
35	33 12 34	mp2an	$⊢ z \in (0 \dots \|D\| - 1) \leftrightarrow (z \in ℤ \land 0 \leq z \land z < \|D\|)$
36	32 35	sylibr	$⊢ (z \in S \land z < \|D\|) \to z \in (0 \dots \|D\| - 1)$
37	36	ex	$⊢ z \in S \to (z < \|D\| \to z \in (0 \dots \|D\| - 1))$
38	26 37	vtoclga	$⊢ Y \in S \to (Y < \|D\| \to Y \in (0 \dots \|D\| - 1))$
39		eleq1	$⊢ Y = X + K \|D\| \to (Y \in (0 \dots \|D\| - 1) \leftrightarrow X + K \|D\| \in (0 \dots \|D\| - 1))$
40	39	biimpd	$⊢ Y = X + K \|D\| \to (Y \in (0 \dots \|D\| - 1) \to X + K \|D\| \in (0 \dots \|D\| - 1))$
41	38 40	sylan9	$⊢ (Y \in S \land Y = X + K \|D\|) \to (Y < \|D\| \to X + K \|D\| \in (0 \dots \|D\| - 1))$
42	41	impancom	$⊢ (Y \in S \land Y < \|D\|) \to (Y = X + K \|D\| \to X + K \|D\| \in (0 \dots \|D\| - 1))$
43	42	3ad2ant2	$⊢ ((X \in S \land X < \|D\|) \land (Y \in S \land Y < \|D\|) \land K \in ℤ) \to (Y = X + K \|D\| \to X + K \|D\| \in (0 \dots \|D\| - 1))$
44		breq1	$⊢ z = X \to (z < \|D\| \leftrightarrow X < \|D\|)$
45		eleq1	$⊢ z = X \to (z \in (0 \dots \|D\| - 1) \leftrightarrow X \in (0 \dots \|D\| - 1))$
46	44 45	imbi12d	$⊢ z = X \to ((z < \|D\| \to z \in (0 \dots \|D\| - 1)) \leftrightarrow (X < \|D\| \to X \in (0 \dots \|D\| - 1)))$
47	46 37	vtoclga	$⊢ X \in S \to (X < \|D\| \to X \in (0 \dots \|D\| - 1))$
48	47	imp	$⊢ (X \in S \land X < \|D\|) \to X \in (0 \dots \|D\| - 1)$
49	2 3	divalglem7	$⊢ (X \in (0 \dots \|D\| - 1) \land K \in ℤ) \to (K \neq 0 \to \neg X + K \|D\| \in (0 \dots \|D\| - 1))$
50	48 49	sylan	$⊢ ((X \in S \land X < \|D\|) \land K \in ℤ) \to (K \neq 0 \to \neg X + K \|D\| \in (0 \dots \|D\| - 1))$
51	50	3adant2	$⊢ ((X \in S \land X < \|D\|) \land (Y \in S \land Y < \|D\|) \land K \in ℤ) \to (K \neq 0 \to \neg X + K \|D\| \in (0 \dots \|D\| - 1))$
52	51	con2d	$⊢ ((X \in S \land X < \|D\|) \land (Y \in S \land Y < \|D\|) \land K \in ℤ) \to (X + K \|D\| \in (0 \dots \|D\| - 1) \to \neg K \neq 0)$
53	43 52	syld	$⊢ ((X \in S \land X < \|D\|) \land (Y \in S \land Y < \|D\|) \land K \in ℤ) \to (Y = X + K \|D\| \to \neg K \neq 0)$
54		df-ne	$⊢ K \neq 0 \leftrightarrow \neg K = 0$
55	54	con2bii	$⊢ K = 0 \leftrightarrow \neg K \neq 0$
56	53 55	imbitrrdi	$⊢ ((X \in S \land X < \|D\|) \land (Y \in S \land Y < \|D\|) \land K \in ℤ) \to (Y = X + K \|D\| \to K = 0)$
57	23 56	sylbid	$⊢ ((X \in S \land X < \|D\|) \land (Y \in S \land Y < \|D\|) \land K \in ℤ) \to (K \|D\| = Y - X \to K = 0)$
58		oveq1	$⊢ K = 0 \to K \|D\| = 0 \cdot \|D\|$
59	11	nncni	$⊢ \|D\| \in ℂ$
60	59	mul02i	$⊢ 0 \cdot \|D\| = 0$
61	58 60	eqtrdi	$⊢ K = 0 \to K \|D\| = 0$
62	61	eqeq1d	$⊢ K = 0 \to (K \|D\| = Y - X \leftrightarrow 0 = Y - X)$
63	62	biimpac	$⊢ (K \|D\| = Y - X \land K = 0) \to 0 = Y - X$
64		subeq0	$⊢ (Y \in ℂ \land X \in ℂ) \to (Y - X = 0 \leftrightarrow Y = X)$
65	8 9 64	syl2anr	$⊢ (X \in S \land Y \in S) \to (Y - X = 0 \leftrightarrow Y = X)$
66		eqcom	$⊢ Y - X = 0 \leftrightarrow 0 = Y - X$
67		eqcom	$⊢ Y = X \leftrightarrow X = Y$
68	65 66 67	3bitr3g	$⊢ (X \in S \land Y \in S) \to (0 = Y - X \leftrightarrow X = Y)$
69	63 68	imbitrid	$⊢ (X \in S \land Y \in S) \to ((K \|D\| = Y - X \land K = 0) \to X = Y)$
70	69	ad2ant2r	$⊢ ((X \in S \land X < \|D\|) \land (Y \in S \land Y < \|D\|)) \to ((K \|D\| = Y - X \land K = 0) \to X = Y)$
71	70	3adant3	$⊢ ((X \in S \land X < \|D\|) \land (Y \in S \land Y < \|D\|) \land K \in ℤ) \to ((K \|D\| = Y - X \land K = 0) \to X = Y)$
72	71	expd	$⊢ ((X \in S \land X < \|D\|) \land (Y \in S \land Y < \|D\|) \land K \in ℤ) \to (K \|D\| = Y - X \to (K = 0 \to X = Y))$
73	57 72	mpdd	$⊢ ((X \in S \land X < \|D\|) \land (Y \in S \land Y < \|D\|) \land K \in ℤ) \to (K \|D\| = Y - X \to X = Y)$
74	73	3expia	$⊢ ((X \in S \land X < \|D\|) \land (Y \in S \land Y < \|D\|)) \to (K \in ℤ \to (K \|D\| = Y - X \to X = Y))$
75	74	an4s	$⊢ ((X \in S \land Y \in S) \land (X < \|D\| \land Y < \|D\|)) \to (K \in ℤ \to (K \|D\| = Y - X \to X = Y))$

Metamath Proof Explorer

Theorem divalglem8

Proof