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 ∣ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) }