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