Theorem divalglem8

Description: Lemma for divalg . (Contributed by Paul Chapman, 21-Mar-2011)

	Ref	Expression
Hypotheses	divalglem8.1	⊢ 𝑁 ∈ ℤ
	divalglem8.2	⊢ 𝐷 ∈ ℤ
	divalglem8.3	⊢ 𝐷 ≠ 0
	divalglem8.4	⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) }
Assertion	divalglem8	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑋 < ( abs ‘ 𝐷 ) ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ) → ( 𝐾 ∈ ℤ → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) → 𝑋 = 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		divalglem8.1	⊢ 𝑁 ∈ ℤ
2		divalglem8.2	⊢ 𝐷 ∈ ℤ
3		divalglem8.3	⊢ 𝐷 ≠ 0
4		divalglem8.4	⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) }
5	4	ssrab3	⊢ 𝑆 ⊆ ℕ0
6		nn0sscn	⊢ ℕ0 ⊆ ℂ
7	5 6	sstri	⊢ 𝑆 ⊆ ℂ
8	7	sseli	⊢ ( 𝑌 ∈ 𝑆 → 𝑌 ∈ ℂ )
9	7	sseli	⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ∈ ℂ )
10		nnabscl	⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → ( abs ‘ 𝐷 ) ∈ ℕ )
11	2 3 10	mp2an	⊢ ( abs ‘ 𝐷 ) ∈ ℕ
12	11	nnzi	⊢ ( abs ‘ 𝐷 ) ∈ ℤ
13		zmulcl	⊢ ( ( 𝐾 ∈ ℤ ∧ ( abs ‘ 𝐷 ) ∈ ℤ ) → ( 𝐾 · ( abs ‘ 𝐷 ) ) ∈ ℤ )
14	12 13	mpan2	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · ( abs ‘ 𝐷 ) ) ∈ ℤ )
15	14	zcnd	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · ( abs ‘ 𝐷 ) ) ∈ ℂ )
16		subadd	⊢ ( ( 𝑌 ∈ ℂ ∧ 𝑋 ∈ ℂ ∧ ( 𝐾 · ( abs ‘ 𝐷 ) ) ∈ ℂ ) → ( ( 𝑌 − 𝑋 ) = ( 𝐾 · ( abs ‘ 𝐷 ) ) ↔ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) = 𝑌 ) )
17	8 9 15 16	syl3an	⊢ ( ( 𝑌 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆 ∧ 𝐾 ∈ ℤ ) → ( ( 𝑌 − 𝑋 ) = ( 𝐾 · ( abs ‘ 𝐷 ) ) ↔ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) = 𝑌 ) )
18	17	3com12	⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ∧ 𝐾 ∈ ℤ ) → ( ( 𝑌 − 𝑋 ) = ( 𝐾 · ( abs ‘ 𝐷 ) ) ↔ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) = 𝑌 ) )
19		eqcom	⊢ ( ( 𝑌 − 𝑋 ) = ( 𝐾 · ( abs ‘ 𝐷 ) ) ↔ ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) )
20		eqcom	⊢ ( ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) = 𝑌 ↔ 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) )
21	18 19 20	3bitr3g	⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ↔ 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ) )
22	21	3adant1r	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ 𝑌 ∈ 𝑆 ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ↔ 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ) )
23	22	3adant2r	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ↔ 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ) )
24		breq1	⊢ ( 𝑧 = 𝑌 → ( 𝑧 < ( abs ‘ 𝐷 ) ↔ 𝑌 < ( abs ‘ 𝐷 ) ) )
25		eleq1	⊢ ( 𝑧 = 𝑌 → ( 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ 𝑌 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
26	24 25	imbi12d	⊢ ( 𝑧 = 𝑌 → ( ( 𝑧 < ( abs ‘ 𝐷 ) → 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ↔ ( 𝑌 < ( abs ‘ 𝐷 ) → 𝑌 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) )
27	5	sseli	⊢ ( 𝑧 ∈ 𝑆 → 𝑧 ∈ ℕ0 )
28		elnn0z	⊢ ( 𝑧 ∈ ℕ0 ↔ ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ) )
29	27 28	sylib	⊢ ( 𝑧 ∈ 𝑆 → ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ) )
30	29	anim1i	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) → ( ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ) ∧ 𝑧 < ( abs ‘ 𝐷 ) ) )
31		df-3an	⊢ ( ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) ↔ ( ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ) ∧ 𝑧 < ( abs ‘ 𝐷 ) ) )
32	30 31	sylibr	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) → ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) )
33		0z	⊢ 0 ∈ ℤ
34		elfzm11	⊢ ( ( 0 ∈ ℤ ∧ ( abs ‘ 𝐷 ) ∈ ℤ ) → ( 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) ) )
35	33 12 34	mp2an	⊢ ( 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) )
36	32 35	sylibr	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) → 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) )
37	36	ex	⊢ ( 𝑧 ∈ 𝑆 → ( 𝑧 < ( abs ‘ 𝐷 ) → 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
38	26 37	vtoclga	⊢ ( 𝑌 ∈ 𝑆 → ( 𝑌 < ( abs ‘ 𝐷 ) → 𝑌 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
39		eleq1	⊢ ( 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) → ( 𝑌 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
40	39	biimpd	⊢ ( 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) → ( 𝑌 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) → ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
41	38 40	sylan9	⊢ ( ( 𝑌 ∈ 𝑆 ∧ 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ) → ( 𝑌 < ( abs ‘ 𝐷 ) → ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
42	41	impancom	⊢ ( ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) → ( 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) → ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
43	42	3ad2ant2	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) → ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
44		breq1	⊢ ( 𝑧 = 𝑋 → ( 𝑧 < ( abs ‘ 𝐷 ) ↔ 𝑋 < ( abs ‘ 𝐷 ) ) )
45		eleq1	⊢ ( 𝑧 = 𝑋 → ( 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
46	44 45	imbi12d	⊢ ( 𝑧 = 𝑋 → ( ( 𝑧 < ( abs ‘ 𝐷 ) → 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ↔ ( 𝑋 < ( abs ‘ 𝐷 ) → 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) )
47	46 37	vtoclga	⊢ ( 𝑋 ∈ 𝑆 → ( 𝑋 < ( abs ‘ 𝐷 ) → 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
48	47	imp	⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) → 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) )
49	2 3	divalglem7	⊢ ( ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ≠ 0 → ¬ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
50	48 49	sylan	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ≠ 0 → ¬ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
51	50	3adant2	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ≠ 0 → ¬ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
52	51	con2d	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) → ¬ 𝐾 ≠ 0 ) )
53	43 52	syld	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) → ¬ 𝐾 ≠ 0 ) )
54		df-ne	⊢ ( 𝐾 ≠ 0 ↔ ¬ 𝐾 = 0 )
55	54	con2bii	⊢ ( 𝐾 = 0 ↔ ¬ 𝐾 ≠ 0 )
56	53 55	imbitrrdi	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) → 𝐾 = 0 ) )
57	23 56	sylbid	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) → 𝐾 = 0 ) )
58		oveq1	⊢ ( 𝐾 = 0 → ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 0 · ( abs ‘ 𝐷 ) ) )
59	11	nncni	⊢ ( abs ‘ 𝐷 ) ∈ ℂ
60	59	mul02i	⊢ ( 0 · ( abs ‘ 𝐷 ) ) = 0
61	58 60	eqtrdi	⊢ ( 𝐾 = 0 → ( 𝐾 · ( abs ‘ 𝐷 ) ) = 0 )
62	61	eqeq1d	⊢ ( 𝐾 = 0 → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ↔ 0 = ( 𝑌 − 𝑋 ) ) )
63	62	biimpac	⊢ ( ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ∧ 𝐾 = 0 ) → 0 = ( 𝑌 − 𝑋 ) )
64		subeq0	⊢ ( ( 𝑌 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( ( 𝑌 − 𝑋 ) = 0 ↔ 𝑌 = 𝑋 ) )
65	8 9 64	syl2anr	⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ( 𝑌 − 𝑋 ) = 0 ↔ 𝑌 = 𝑋 ) )
66		eqcom	⊢ ( ( 𝑌 − 𝑋 ) = 0 ↔ 0 = ( 𝑌 − 𝑋 ) )
67		eqcom	⊢ ( 𝑌 = 𝑋 ↔ 𝑋 = 𝑌 )
68	65 66 67	3bitr3g	⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 0 = ( 𝑌 − 𝑋 ) ↔ 𝑋 = 𝑌 ) )
69	63 68	imbitrid	⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ∧ 𝐾 = 0 ) → 𝑋 = 𝑌 ) )
70	69	ad2ant2r	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ) → ( ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ∧ 𝐾 = 0 ) → 𝑋 = 𝑌 ) )
71	70	3adant3	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ∧ 𝐾 = 0 ) → 𝑋 = 𝑌 ) )
72	71	expd	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) → ( 𝐾 = 0 → 𝑋 = 𝑌 ) ) )
73	57 72	mpdd	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) → 𝑋 = 𝑌 ) )
74	73	3expia	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ) → ( 𝐾 ∈ ℤ → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) → 𝑋 = 𝑌 ) ) )
75	74	an4s	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑋 < ( abs ‘ 𝐷 ) ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ) → ( 𝐾 ∈ ℤ → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) → 𝑋 = 𝑌 ) ) )