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

Metamath Proof Explorer

Theorem divalglem4

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

Ref Expression
Hypotheses divalglem0.1 ⊢ 𝑁 ∈ ℤ
divalglem0.2 ⊢ 𝐷 ∈ ℤ
divalglem1.3 ⊢ 𝐷 ≠ 0
divalglem2.4 ⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) }
Assertion divalglem4 𝑆 = { 𝑟 ∈ ℕ0 ∣ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) }

Proof

Step Hyp Ref Expression
1 divalglem0.1 ⊢ 𝑁 ∈ ℤ
2 divalglem0.2 ⊢ 𝐷 ∈ ℤ
3 divalglem1.3 ⊢ 𝐷 ≠ 0
4 divalglem2.4 ⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) }
5 nn0z ⊢ ( 𝑧 ∈ ℕ0 → 𝑧 ∈ ℤ )
6 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 𝑁 − 𝑧 ) ∈ ℤ )
7 1 5 6 sylancr ⊢ ( 𝑧 ∈ ℕ0 → ( 𝑁 − 𝑧 ) ∈ ℤ )
8 divides ⊢ ( ( 𝐷 ∈ ℤ ∧ ( 𝑁 − 𝑧 ) ∈ ℤ ) → ( 𝐷 ∥ ( 𝑁 − 𝑧 ) ↔ ∃ 𝑞 ∈ ℤ ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑧 ) ) )
9 2 7 8 sylancr ⊢ ( 𝑧 ∈ ℕ0 → ( 𝐷 ∥ ( 𝑁 − 𝑧 ) ↔ ∃ 𝑞 ∈ ℤ ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑧 ) ) )
10 nn0cn ⊢ ( 𝑧 ∈ ℕ0 → 𝑧 ∈ ℂ )
11 zmulcl ⊢ ( ( 𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( 𝑞 · 𝐷 ) ∈ ℤ )
12 2 11 mpan2 ⊢ ( 𝑞 ∈ ℤ → ( 𝑞 · 𝐷 ) ∈ ℤ )
13 12 zcnd ⊢ ( 𝑞 ∈ ℤ → ( 𝑞 · 𝐷 ) ∈ ℂ )
14 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
15 1 14 ax-mp ⊢ 𝑁 ∈ ℂ
16 subadd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ ( 𝑞 · 𝐷 ) ∈ ℂ ) → ( ( 𝑁 − 𝑧 ) = ( 𝑞 · 𝐷 ) ↔ ( 𝑧 + ( 𝑞 · 𝐷 ) ) = 𝑁 ) )
17 15 16 mp3an1 ⊢ ( ( 𝑧 ∈ ℂ ∧ ( 𝑞 · 𝐷 ) ∈ ℂ ) → ( ( 𝑁 − 𝑧 ) = ( 𝑞 · 𝐷 ) ↔ ( 𝑧 + ( 𝑞 · 𝐷 ) ) = 𝑁 ) )
18 addcom ⊢ ( ( 𝑧 ∈ ℂ ∧ ( 𝑞 · 𝐷 ) ∈ ℂ ) → ( 𝑧 + ( 𝑞 · 𝐷 ) ) = ( ( 𝑞 · 𝐷 ) + 𝑧 ) )
19 18 eqeq1d ⊢ ( ( 𝑧 ∈ ℂ ∧ ( 𝑞 · 𝐷 ) ∈ ℂ ) → ( ( 𝑧 + ( 𝑞 · 𝐷 ) ) = 𝑁 ↔ ( ( 𝑞 · 𝐷 ) + 𝑧 ) = 𝑁 ) )
20 17 19 bitrd ⊢ ( ( 𝑧 ∈ ℂ ∧ ( 𝑞 · 𝐷 ) ∈ ℂ ) → ( ( 𝑁 − 𝑧 ) = ( 𝑞 · 𝐷 ) ↔ ( ( 𝑞 · 𝐷 ) + 𝑧 ) = 𝑁 ) )
21 10 13 20 syl2an ⊢ ( ( 𝑧 ∈ ℕ0 ∧ 𝑞 ∈ ℤ ) → ( ( 𝑁 − 𝑧 ) = ( 𝑞 · 𝐷 ) ↔ ( ( 𝑞 · 𝐷 ) + 𝑧 ) = 𝑁 ) )
22 eqcom ⊢ ( ( 𝑁 − 𝑧 ) = ( 𝑞 · 𝐷 ) ↔ ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑧 ) )
23 eqcom ⊢ ( ( ( 𝑞 · 𝐷 ) + 𝑧 ) = 𝑁 ↔ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑧 ) )
24 21 22 23 3bitr3g ⊢ ( ( 𝑧 ∈ ℕ0 ∧ 𝑞 ∈ ℤ ) → ( ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑧 ) ↔ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑧 ) ) )
25 24 rexbidva ⊢ ( 𝑧 ∈ ℕ0 → ( ∃ 𝑞 ∈ ℤ ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑧 ) ↔ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑧 ) ) )
26 9 25 bitrd ⊢ ( 𝑧 ∈ ℕ0 → ( 𝐷 ∥ ( 𝑁 − 𝑧 ) ↔ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑧 ) ) )
27 26 pm5.32i ⊢ ( ( 𝑧 ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − 𝑧 ) ) ↔ ( 𝑧 ∈ ℕ0 ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑧 ) ) )
28 oveq2 ⊢ ( 𝑟 = 𝑧 → ( 𝑁 − 𝑟 ) = ( 𝑁 − 𝑧 ) )
29 28 breq2d ⊢ ( 𝑟 = 𝑧 → ( 𝐷 ∥ ( 𝑁 − 𝑟 ) ↔ 𝐷 ∥ ( 𝑁 − 𝑧 ) ) )
30 29 4 elrab2 ⊢ ( 𝑧 ∈ 𝑆 ↔ ( 𝑧 ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − 𝑧 ) ) )
31 oveq2 ⊢ ( 𝑟 = 𝑧 → ( ( 𝑞 · 𝐷 ) + 𝑟 ) = ( ( 𝑞 · 𝐷 ) + 𝑧 ) )
32 31 eqeq2d ⊢ ( 𝑟 = 𝑧 → ( 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ↔ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑧 ) ) )
33 32 rexbidv ⊢ ( 𝑟 = 𝑧 → ( ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ↔ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑧 ) ) )
34 33 elrab ⊢ ( 𝑧 ∈ { 𝑟 ∈ ℕ0 ∣ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) } ↔ ( 𝑧 ∈ ℕ0 ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑧 ) ) )
35 27 30 34 3bitr4i ⊢ ( 𝑧 ∈ 𝑆 ↔ 𝑧 ∈ { 𝑟 ∈ ℕ0 ∣ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) } )
36 35 eqriv ⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) }