Metamath Proof Explorer

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 ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) → 𝑋 = 𝑌 ) ) )