Metamath Proof Explorer

Theorem divalglem7

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

Ref Expression
Hypotheses divalglem7.1 ⊢D∈ℤ
divalglem7.2 ⊢D≠0
Assertion divalglem7 ⊢X∈0…D−1∧K∈ℤ→K≠0→¬X+K⁢D∈0…D−1

Proof

Step Hyp Ref Expression
1 divalglem7.1 ⊢D∈ℤ
2 divalglem7.2 ⊢D≠0
3 oveq1 ⊢X=ifX∈0…D−1X0→X+K⁢D=ifX∈0…D−1X0+K⁢D
4 3 eleq1d ⊢X=ifX∈0…D−1X0→X+K⁢D∈0…D−1↔ifX∈0…D−1X0+K⁢D∈0…D−1
5 4 notbid ⊢X=ifX∈0…D−1X0→¬X+K⁢D∈0…D−1↔¬ifX∈0…D−1X0+K⁢D∈0…D−1
6 5 imbi2d ⊢X=ifX∈0…D−1X0→K≠0→¬X+K⁢D∈0…D−1↔K≠0→¬ifX∈0…D−1X0+K⁢D∈0…D−1
7 neeq1 ⊢K=ifK∈ℤK0→K≠0↔ifK∈ℤK0≠0
8 oveq1 ⊢K=ifK∈ℤK0→K⁢D=ifK∈ℤK0⁢D
9 8 oveq2d ⊢K=ifK∈ℤK0→ifX∈0…D−1X0+K⁢D=ifX∈0…D−1X0+ifK∈ℤK0⁢D
10 9 eleq1d ⊢K=ifK∈ℤK0→ifX∈0…D−1X0+K⁢D∈0…D−1↔ifX∈0…D−1X0+ifK∈ℤK0⁢D∈0…D−1
11 10 notbid ⊢K=ifK∈ℤK0→¬ifX∈0…D−1X0+K⁢D∈0…D−1↔¬ifX∈0…D−1X0+ifK∈ℤK0⁢D∈0…D−1
12 7 11 imbi12d ⊢K=ifK∈ℤK0→K≠0→¬ifX∈0…D−1X0+K⁢D∈0…D−1↔ifK∈ℤK0≠0→¬ifX∈0…D−1X0+ifK∈ℤK0⁢D∈0…D−1
13 nnabscl ⊢D∈ℤ∧D≠0→D∈ℕ
14 1 2 13 mp2an ⊢D∈ℕ
15 0z ⊢0∈ℤ
16 0le0 ⊢0≤0
17 14 nngt0i ⊢0<D
18 14 nnzi ⊢D∈ℤ
19 elfzm11 ⊢0∈ℤ∧D∈ℤ→0∈0…D−1↔0∈ℤ∧0≤0∧0<D
20 15 18 19 mp2an ⊢0∈0…D−1↔0∈ℤ∧0≤0∧0<D
21 15 16 17 20 mpbir3an ⊢0∈0…D−1
22 21 elimel ⊢ifX∈0…D−1X0∈0…D−1
23 15 elimel ⊢ifK∈ℤK0∈ℤ
24 14 22 23 divalglem6 ⊢ifK∈ℤK0≠0→¬ifX∈0…D−1X0+ifK∈ℤK0⁢D∈0…D−1
25 6 12 24 dedth2h ⊢X∈0…D−1∧K∈ℤ→K≠0→¬X+K⁢D∈0…D−1