Metamath Proof Explorer

Theorem divalglem4

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

Ref Expression
Hypotheses divalglem0.1 ⊢N∈ℤ
divalglem0.2 ⊢D∈ℤ
divalglem1.3 ⊢D≠0
divalglem2.4 ⊢S=r∈ℕ0|D∥N−r
Assertion divalglem4 ⊢S=r∈ℕ0|∃q∈ℤN=q⁢D+r

Proof

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