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 syl6ibr ( ( ( 𝑋𝑆𝑋 < ( 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 syl5ib ( ( 𝑋𝑆𝑌𝑆 ) → ( ( ( 𝐾 · ( 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 ‘ 𝐷 ) ) = ( 𝑌𝑋 ) → 𝑋 = 𝑌 ) ) )