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 = if X ∈ 0 … D − 1 X 0 → X + K ⁢ D = if X ∈ 0 … D − 1 X 0 + K ⁢ D
4 3 eleq1d ⊢ X = if X ∈ 0 … D − 1 X 0 → X + K ⁢ D ∈ 0 … D − 1 ↔ if X ∈ 0 … D − 1 X 0 + K ⁢ D ∈ 0 … D − 1
5 4 notbid ⊢ X = if X ∈ 0 … D − 1 X 0 → ¬ X + K ⁢ D ∈ 0 … D − 1 ↔ ¬ if X ∈ 0 … D − 1 X 0 + K ⁢ D ∈ 0 … D − 1
6 5 imbi2d ⊢ X = if X ∈ 0 … D − 1 X 0 → K ≠ 0 → ¬ X + K ⁢ D ∈ 0 … D − 1 ↔ K ≠ 0 → ¬ if X ∈ 0 … D − 1 X 0 + K ⁢ D ∈ 0 … D − 1
7 neeq1 ⊢ K = if K ∈ ℤ K 0 → K ≠ 0 ↔ if K ∈ ℤ K 0 ≠ 0
8 oveq1 ⊢ K = if K ∈ ℤ K 0 → K ⁢ D = if K ∈ ℤ K 0 ⁢ D
9 8 oveq2d ⊢ K = if K ∈ ℤ K 0 → if X ∈ 0 … D − 1 X 0 + K ⁢ D = if X ∈ 0 … D − 1 X 0 + if K ∈ ℤ K 0 ⁢ D
10 9 eleq1d ⊢ K = if K ∈ ℤ K 0 → if X ∈ 0 … D − 1 X 0 + K ⁢ D ∈ 0 … D − 1 ↔ if X ∈ 0 … D − 1 X 0 + if K ∈ ℤ K 0 ⁢ D ∈ 0 … D − 1
11 10 notbid ⊢ K = if K ∈ ℤ K 0 → ¬ if X ∈ 0 … D − 1 X 0 + K ⁢ D ∈ 0 … D − 1 ↔ ¬ if X ∈ 0 … D − 1 X 0 + if K ∈ ℤ K 0 ⁢ D ∈ 0 … D − 1
12 7 11 imbi12d ⊢ K = if K ∈ ℤ K 0 → K ≠ 0 → ¬ if X ∈ 0 … D − 1 X 0 + K ⁢ D ∈ 0 … D − 1 ↔ if K ∈ ℤ K 0 ≠ 0 → ¬ if X ∈ 0 … D − 1 X 0 + if K ∈ ℤ K 0 ⁢ 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 ⊢ if X ∈ 0 … D − 1 X 0 ∈ 0 … D − 1
23 15 elimel ⊢ if K ∈ ℤ K 0 ∈ ℤ
24 14 22 23 divalglem6 ⊢ if K ∈ ℤ K 0 ≠ 0 → ¬ if X ∈ 0 … D − 1 X 0 + if K ∈ ℤ K 0 ⁢ D ∈ 0 … D − 1
25 6 12 24 dedth2h ⊢ X ∈ 0 … D − 1 ∧ K ∈ ℤ → K ≠ 0 → ¬ X + K ⁢ D ∈ 0 … D − 1