Metamath Proof Explorer

Theorem divalglem0

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

Ref Expression
Hypotheses divalglem0.1 ⊢ 𝑁 ∈ ℤ
divalglem0.2 ⊢ 𝐷 ∈ ℤ
Assertion divalglem0 ( ( 𝑅 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ) ) )

Proof

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