This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem divalglem10

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

Ref Expression
Hypotheses divalglem8.1 ⊢ 𝑁 ∈ ℤ
divalglem8.2 ⊢ 𝐷 ∈ ℤ
divalglem8.3 ⊢ 𝐷 ≠ 0
divalglem8.4 ⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) }
Assertion divalglem10 ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) )

Proof

Step Hyp Ref Expression
1 divalglem8.1 ⊢ 𝑁 ∈ ℤ
2 divalglem8.2 ⊢ 𝐷 ∈ ℤ
3 divalglem8.3 ⊢ 𝐷 ≠ 0
4 divalglem8.4 ⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) }
5 eqid ⊢ inf ( 𝑆 , ℝ , < ) = inf ( 𝑆 , ℝ , < )
6 1 2 3 4 5 divalglem9 ⊢ ∃! 𝑥 ∈ 𝑆 𝑥 < ( abs ‘ 𝐷 )
7 elnn0z ⊢ ( 𝑥 ∈ ℕ0 ↔ ( 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥 ) )
8 7 anbi2i ⊢ ( ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑥 ∈ ℕ0 ) ↔ ( 𝑥 < ( abs ‘ 𝐷 ) ∧ ( 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥 ) ) )
9 an12 ⊢ ( ( 𝑥 < ( abs ‘ 𝐷 ) ∧ ( 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥 ) ) ↔ ( 𝑥 ∈ ℤ ∧ ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 0 ≤ 𝑥 ) ) )
10 ancom ⊢ ( ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 0 ≤ 𝑥 ) ↔ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) )
11 10 anbi2i ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 0 ≤ 𝑥 ) ) ↔ ( 𝑥 ∈ ℤ ∧ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ) )
12 9 11 bitri ⊢ ( ( 𝑥 < ( abs ‘ 𝐷 ) ∧ ( 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥 ) ) ↔ ( 𝑥 ∈ ℤ ∧ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ) )
13 8 12 bitri ⊢ ( ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑥 ∈ ℕ0 ) ↔ ( 𝑥 ∈ ℤ ∧ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ) )
14 13 anbi1i ⊢ ( ( ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ↔ ( ( 𝑥 ∈ ℤ ∧ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) )
15 anass ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ↔ ( 𝑥 ∈ ℤ ∧ ( ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ) )
16 14 15 bitri ⊢ ( ( ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ↔ ( 𝑥 ∈ ℤ ∧ ( ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ) )
17 oveq2 ⊢ ( 𝑟 = 𝑥 → ( ( 𝑞 · 𝐷 ) + 𝑟 ) = ( ( 𝑞 · 𝐷 ) + 𝑥 ) )
18 17 eqeq2d ⊢ ( 𝑟 = 𝑥 → ( 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ↔ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) )
19 18 rexbidv ⊢ ( 𝑟 = 𝑥 → ( ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ↔ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) )
20 1 2 3 4 divalglem4 ⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) }
21 19 20 elrab2 ⊢ ( 𝑥 ∈ 𝑆 ↔ ( 𝑥 ∈ ℕ0 ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) )
22 21 anbi2i ⊢ ( ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑥 ∈ 𝑆 ) ↔ ( 𝑥 < ( abs ‘ 𝐷 ) ∧ ( 𝑥 ∈ ℕ0 ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ) )
23 ancom ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ↔ ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑥 ∈ 𝑆 ) )
24 anass ⊢ ( ( ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ↔ ( 𝑥 < ( abs ‘ 𝐷 ) ∧ ( 𝑥 ∈ ℕ0 ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ) )
25 22 23 24 3bitr4i ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ↔ ( ( 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) )
26 df-3an ⊢ ( ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ↔ ( ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) )
27 26 rexbii ⊢ ( ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ↔ ∃ 𝑞 ∈ ℤ ( ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) )
28 r19.42v ⊢ ( ∃ 𝑞 ∈ ℤ ( ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ↔ ( ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) )
29 27 28 bitri ⊢ ( ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ↔ ( ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) )
30 29 anbi2i ⊢ ( ( 𝑥 ∈ ℤ ∧ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ) ↔ ( 𝑥 ∈ ℤ ∧ ( ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ) )
31 16 25 30 3bitr4i ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ↔ ( 𝑥 ∈ ℤ ∧ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ) )
32 31 eubii ⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝑆 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) ↔ ∃! 𝑥 ( 𝑥 ∈ ℤ ∧ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ) )
33 df-reu ⊢ ( ∃! 𝑥 ∈ 𝑆 𝑥 < ( abs ‘ 𝐷 ) ↔ ∃! 𝑥 ( 𝑥 ∈ 𝑆 ∧ 𝑥 < ( abs ‘ 𝐷 ) ) )
34 df-reu ⊢ ( ∃! 𝑥 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ↔ ∃! 𝑥 ( 𝑥 ∈ ℤ ∧ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ) )
35 32 33 34 3bitr4i ⊢ ( ∃! 𝑥 ∈ 𝑆 𝑥 < ( abs ‘ 𝐷 ) ↔ ∃! 𝑥 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) )
36 6 35 mpbi ⊢ ∃! 𝑥 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) )
37 breq2 ⊢ ( 𝑥 = 𝑟 → ( 0 ≤ 𝑥 ↔ 0 ≤ 𝑟 ) )
38 breq1 ⊢ ( 𝑥 = 𝑟 → ( 𝑥 < ( abs ‘ 𝐷 ) ↔ 𝑟 < ( abs ‘ 𝐷 ) ) )
39 oveq2 ⊢ ( 𝑥 = 𝑟 → ( ( 𝑞 · 𝐷 ) + 𝑥 ) = ( ( 𝑞 · 𝐷 ) + 𝑟 ) )
40 39 eqeq2d ⊢ ( 𝑥 = 𝑟 → ( 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ↔ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )
41 37 38 40 3anbi123d ⊢ ( 𝑥 = 𝑟 → ( ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ↔ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ) )
42 41 rexbidv ⊢ ( 𝑥 = 𝑟 → ( ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ↔ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ) )
43 42 cbvreuvw ⊢ ( ∃! 𝑥 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑥 ∧ 𝑥 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑥 ) ) ↔ ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )
44 36 43 mpbi ⊢ ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) )