Metamath Proof Explorer

Theorem divalglem9

Description: Lemma for divalg . (Contributed by Paul Chapman, 21-Mar-2011) (Revised by AV, 2-Oct-2020)

Ref Expression
Hypotheses divalglem8.1 ⊢ 𝑁 ∈ ℤ
divalglem8.2 ⊢ 𝐷 ∈ ℤ
divalglem8.3 ⊢ 𝐷 ≠ 0
divalglem8.4 ⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) }
divalglem9.5 ⊢ 𝑅 = inf ( 𝑆 , ℝ , < )
Assertion divalglem9 ∃! 𝑥 ∈ 𝑆 𝑥 < ( abs ‘ 𝐷 )

Proof

Step Hyp Ref Expression
1 divalglem8.1 ⊢ 𝑁 ∈ ℤ
2 divalglem8.2 ⊢ 𝐷 ∈ ℤ
3 divalglem8.3 ⊢ 𝐷 ≠ 0
4 divalglem8.4 ⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) }
5 divalglem9.5 ⊢ 𝑅 = inf ( 𝑆 , ℝ , < )
6 1 2 3 4 divalglem2 ⊢ inf ( 𝑆 , ℝ , < ) ∈ 𝑆
7 5 6 eqeltri ⊢ 𝑅 ∈ 𝑆
8 1 2 3 4 5 divalglem5 ⊢ ( 0 ≤ 𝑅 ∧ 𝑅 < ( abs ‘ 𝐷 ) )
9 8 simpri ⊢ 𝑅 < ( abs ‘ 𝐷 )
10 breq1 ⊢ ( 𝑥 = 𝑅 → ( 𝑥 < ( abs ‘ 𝐷 ) ↔ 𝑅 < ( abs ‘ 𝐷 ) ) )
11 10 rspcev ⊢ ( ( 𝑅 ∈ 𝑆 ∧ 𝑅 < ( abs ‘ 𝐷 ) ) → ∃ 𝑥 ∈ 𝑆 𝑥 < ( abs ‘ 𝐷 ) )
12 7 9 11 mp2an ⊢ ∃ 𝑥 ∈ 𝑆 𝑥 < ( abs ‘ 𝐷 )
13 oveq2 ⊢ ( 𝑟 = 𝑥 → ( 𝑁 − 𝑟 ) = ( 𝑁 − 𝑥 ) )
14 13 breq2d ⊢ ( 𝑟 = 𝑥 → ( 𝐷 ∥ ( 𝑁 − 𝑟 ) ↔ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) )
15 14 4 elrab2 ⊢ ( 𝑥 ∈ 𝑆 ↔ ( 𝑥 ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) )
16 15 simplbi ⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ℕ0 )
17 16 nn0zd ⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ℤ )
18 oveq2 ⊢ ( 𝑟 = 𝑦 → ( 𝑁 − 𝑟 ) = ( 𝑁 − 𝑦 ) )
19 18 breq2d ⊢ ( 𝑟 = 𝑦 → ( 𝐷 ∥ ( 𝑁 − 𝑟 ) ↔ 𝐷 ∥ ( 𝑁 − 𝑦 ) ) )
20 19 4 elrab2 ⊢ ( 𝑦 ∈ 𝑆 ↔ ( 𝑦 ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − 𝑦 ) ) )
21 20 simplbi ⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ℕ0 )
22 21 nn0zd ⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ℤ )
23 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑁 − 𝑥 ) ∈ ℤ )
24 1 23 mpan ⊢ ( 𝑥 ∈ ℤ → ( 𝑁 − 𝑥 ) ∈ ℤ )
25 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑁 − 𝑦 ) ∈ ℤ )
26 1 25 mpan ⊢ ( 𝑦 ∈ ℤ → ( 𝑁 − 𝑦 ) ∈ ℤ )
27 24 26 anim12i ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑁 − 𝑥 ) ∈ ℤ ∧ ( 𝑁 − 𝑦 ) ∈ ℤ ) )
28 17 22 27 syl2an ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑁 − 𝑥 ) ∈ ℤ ∧ ( 𝑁 − 𝑦 ) ∈ ℤ ) )
29 15 simprbi ⊢ ( 𝑥 ∈ 𝑆 → 𝐷 ∥ ( 𝑁 − 𝑥 ) )
30 20 simprbi ⊢ ( 𝑦 ∈ 𝑆 → 𝐷 ∥ ( 𝑁 − 𝑦 ) )
31 29 30 anim12i ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐷 ∥ ( 𝑁 − 𝑥 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑦 ) ) )
32 dvds2sub ⊢ ( ( 𝐷 ∈ ℤ ∧ ( 𝑁 − 𝑥 ) ∈ ℤ ∧ ( 𝑁 − 𝑦 ) ∈ ℤ ) → ( ( 𝐷 ∥ ( 𝑁 − 𝑥 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑦 ) ) → 𝐷 ∥ ( ( 𝑁 − 𝑥 ) − ( 𝑁 − 𝑦 ) ) ) )
33 2 32 mp3an1 ⊢ ( ( ( 𝑁 − 𝑥 ) ∈ ℤ ∧ ( 𝑁 − 𝑦 ) ∈ ℤ ) → ( ( 𝐷 ∥ ( 𝑁 − 𝑥 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑦 ) ) → 𝐷 ∥ ( ( 𝑁 − 𝑥 ) − ( 𝑁 − 𝑦 ) ) ) )
34 28 31 33 sylc ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝐷 ∥ ( ( 𝑁 − 𝑥 ) − ( 𝑁 − 𝑦 ) ) )
35 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
36 zcn ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
37 1 zrei ⊢ 𝑁 ∈ ℝ
38 37 recni ⊢ 𝑁 ∈ ℂ
39 38 subidi ⊢ ( 𝑁 − 𝑁 ) = 0
40 39 oveq1i ⊢ ( ( 𝑁 − 𝑁 ) − ( 𝑥 − 𝑦 ) ) = ( 0 − ( 𝑥 − 𝑦 ) )
41 0cn ⊢ 0 ∈ ℂ
42 subsub2 ⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 0 − ( 𝑥 − 𝑦 ) ) = ( 0 + ( 𝑦 − 𝑥 ) ) )
43 41 42 mp3an1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 0 − ( 𝑥 − 𝑦 ) ) = ( 0 + ( 𝑦 − 𝑥 ) ) )
44 40 43 eqtrid ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑁 − 𝑁 ) − ( 𝑥 − 𝑦 ) ) = ( 0 + ( 𝑦 − 𝑥 ) ) )
45 sub4 ⊢ ( ( ( 𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( 𝑁 − 𝑁 ) − ( 𝑥 − 𝑦 ) ) = ( ( 𝑁 − 𝑥 ) − ( 𝑁 − 𝑦 ) ) )
46 38 38 45 mpanl12 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑁 − 𝑁 ) − ( 𝑥 − 𝑦 ) ) = ( ( 𝑁 − 𝑥 ) − ( 𝑁 − 𝑦 ) ) )
47 subcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑦 − 𝑥 ) ∈ ℂ )
48 47 ancoms ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑦 − 𝑥 ) ∈ ℂ )
49 48 addlidd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 0 + ( 𝑦 − 𝑥 ) ) = ( 𝑦 − 𝑥 ) )
50 44 46 49 3eqtr3d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑁 − 𝑥 ) − ( 𝑁 − 𝑦 ) ) = ( 𝑦 − 𝑥 ) )
51 35 36 50 syl2an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑁 − 𝑥 ) − ( 𝑁 − 𝑦 ) ) = ( 𝑦 − 𝑥 ) )
52 17 22 51 syl2an ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑁 − 𝑥 ) − ( 𝑁 − 𝑦 ) ) = ( 𝑦 − 𝑥 ) )
53 52 breq2d ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐷 ∥ ( ( 𝑁 − 𝑥 ) − ( 𝑁 − 𝑦 ) ) ↔ 𝐷 ∥ ( 𝑦 − 𝑥 ) ) )
54 34 53 mpbid ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝐷 ∥ ( 𝑦 − 𝑥 ) )
55 zsubcl ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑦 − 𝑥 ) ∈ ℤ )
56 55 ancoms ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑦 − 𝑥 ) ∈ ℤ )
57 absdvdsb ⊢ ( ( 𝐷 ∈ ℤ ∧ ( 𝑦 − 𝑥 ) ∈ ℤ ) → ( 𝐷 ∥ ( 𝑦 − 𝑥 ) ↔ ( abs ‘ 𝐷 ) ∥ ( 𝑦 − 𝑥 ) ) )
58 2 56 57 sylancr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝐷 ∥ ( 𝑦 − 𝑥 ) ↔ ( abs ‘ 𝐷 ) ∥ ( 𝑦 − 𝑥 ) ) )
59 17 22 58 syl2an ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐷 ∥ ( 𝑦 − 𝑥 ) ↔ ( abs ‘ 𝐷 ) ∥ ( 𝑦 − 𝑥 ) ) )
60 54 59 mpbid ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ 𝐷 ) ∥ ( 𝑦 − 𝑥 ) )
61 nnabscl ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → ( abs ‘ 𝐷 ) ∈ ℕ )
62 2 3 61 mp2an ⊢ ( abs ‘ 𝐷 ) ∈ ℕ
63 62 nnzi ⊢ ( abs ‘ 𝐷 ) ∈ ℤ
64 divides ⊢ ( ( ( abs ‘ 𝐷 ) ∈ ℤ ∧ ( 𝑦 − 𝑥 ) ∈ ℤ ) → ( ( abs ‘ 𝐷 ) ∥ ( 𝑦 − 𝑥 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · ( abs ‘ 𝐷 ) ) = ( 𝑦 − 𝑥 ) ) )
65 63 56 64 sylancr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( abs ‘ 𝐷 ) ∥ ( 𝑦 − 𝑥 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · ( abs ‘ 𝐷 ) ) = ( 𝑦 − 𝑥 ) ) )
66 17 22 65 syl2an ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( abs ‘ 𝐷 ) ∥ ( 𝑦 − 𝑥 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · ( abs ‘ 𝐷 ) ) = ( 𝑦 − 𝑥 ) ) )
67 60 66 mpbid ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ∃ 𝑘 ∈ ℤ ( 𝑘 · ( abs ‘ 𝐷 ) ) = ( 𝑦 − 𝑥 ) )
68 67 adantr ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑦 < ( abs ‘ 𝐷 ) ) ) → ∃ 𝑘 ∈ ℤ ( 𝑘 · ( abs ‘ 𝐷 ) ) = ( 𝑦 − 𝑥 ) )
69 1 2 3 4 divalglem8 ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑦 < ( abs ‘ 𝐷 ) ) ) → ( 𝑘 ∈ ℤ → ( ( 𝑘 · ( abs ‘ 𝐷 ) ) = ( 𝑦 − 𝑥 ) → 𝑥 = 𝑦 ) ) )
70 69 rexlimdv ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑦 < ( abs ‘ 𝐷 ) ) ) → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · ( abs ‘ 𝐷 ) ) = ( 𝑦 − 𝑥 ) → 𝑥 = 𝑦 ) )
71 68 70 mpd ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑦 < ( abs ‘ 𝐷 ) ) ) → 𝑥 = 𝑦 )
72 71 ex ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑦 < ( abs ‘ 𝐷 ) ) → 𝑥 = 𝑦 ) )
73 72 rgen2 ⊢ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑦 < ( abs ‘ 𝐷 ) ) → 𝑥 = 𝑦 )
74 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 < ( abs ‘ 𝐷 ) ↔ 𝑦 < ( abs ‘ 𝐷 ) ) )
75 74 reu4 ⊢ ( ∃! 𝑥 ∈ 𝑆 𝑥 < ( abs ‘ 𝐷 ) ↔ ( ∃ 𝑥 ∈ 𝑆 𝑥 < ( abs ‘ 𝐷 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑦 < ( abs ‘ 𝐷 ) ) → 𝑥 = 𝑦 ) ) )
76 12 73 75 mpbir2an ⊢ ∃! 𝑥 ∈ 𝑆 𝑥 < ( abs ‘ 𝐷 )