Metamath Proof Explorer

Theorem divalglem0

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

Ref Expression
Hypotheses divalglem0.1 ⊢ N ∈ ℤ
divalglem0.2 ⊢ D ∈ ℤ
Assertion divalglem0 ⊢ R ∈ ℤ ∧ K ∈ ℤ → D ∥ N − R → D ∥ N − R − K ⁢ D

Proof

Step Hyp Ref Expression
1 divalglem0.1 ⊢ N ∈ ℤ
2 divalglem0.2 ⊢ D ∈ ℤ
3 iddvds ⊢ D ∈ ℤ → D ∥ D
4 dvdsabsb ⊢ D ∈ ℤ ∧ D ∈ ℤ → D ∥ D ↔ D ∥ D
5 4 anidms ⊢ D ∈ ℤ → D ∥ D ↔ D ∥ D
6 3 5 mpbid ⊢ D ∈ ℤ → D ∥ D
7 2 6 ax-mp ⊢ D ∥ D
8 nn0abscl ⊢ D ∈ ℤ → D ∈ ℕ 0
9 2 8 ax-mp ⊢ D ∈ ℕ 0
10 9 nn0zi ⊢ D ∈ ℤ
11 dvdsmultr2 ⊢ D ∈ ℤ ∧ K ∈ ℤ ∧ D ∈ ℤ → D ∥ D → D ∥ K ⁢ D
12 2 10 11 mp3an13 ⊢ K ∈ ℤ → D ∥ D → D ∥ K ⁢ D
13 7 12 mpi ⊢ K ∈ ℤ → D ∥ K ⁢ D
14 13 adantl ⊢ R ∈ ℤ ∧ K ∈ ℤ → D ∥ K ⁢ D
15 zsubcl ⊢ N ∈ ℤ ∧ R ∈ ℤ → N − R ∈ ℤ
16 1 15 mpan ⊢ R ∈ ℤ → N − R ∈ ℤ
17 zmulcl ⊢ K ∈ ℤ ∧ D ∈ ℤ → K ⁢ D ∈ ℤ
18 10 17 mpan2 ⊢ K ∈ ℤ → K ⁢ D ∈ ℤ
19 dvds2add ⊢ D ∈ ℤ ∧ N − R ∈ ℤ ∧ K ⁢ D ∈ ℤ → D ∥ N − R ∧ D ∥ K ⁢ D → D ∥ N - R + K ⁢ D
20 2 16 18 19 mp3an3an ⊢ R ∈ ℤ ∧ K ∈ ℤ → D ∥ N − R ∧ D ∥ K ⁢ D → D ∥ N - R + K ⁢ D
21 14 20 mpan2d ⊢ R ∈ ℤ ∧ K ∈ ℤ → D ∥ N − R → D ∥ N - R + K ⁢ D
22 zcn ⊢ N ∈ ℤ → N ∈ ℂ
23 1 22 ax-mp ⊢ N ∈ ℂ
24 zcn ⊢ R ∈ ℤ → R ∈ ℂ
25 18 zcnd ⊢ K ∈ ℤ → K ⁢ D ∈ ℂ
26 subsub ⊢ N ∈ ℂ ∧ R ∈ ℂ ∧ K ⁢ D ∈ ℂ → N − R − K ⁢ D = N - R + K ⁢ D
27 23 24 25 26 mp3an3an ⊢ R ∈ ℤ ∧ K ∈ ℤ → N − R − K ⁢ D = N - R + K ⁢ D
28 27 breq2d ⊢ R ∈ ℤ ∧ K ∈ ℤ → D ∥ N − R − K ⁢ D ↔ D ∥ N - R + K ⁢ D
29 21 28 sylibrd ⊢ R ∈ ℤ ∧ K ∈ ℤ → D ∥ N − R → D ∥ N − R − K ⁢ D