Metamath Proof Explorer

Theorem divalglem7

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

Ref Expression
Hypotheses divalglem7.1 ⊢ 𝐷 ∈ ℤ
divalglem7.2 ⊢ 𝐷 ≠ 0
Assertion divalglem7 ( ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ≠ 0 → ¬ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 divalglem7.1 ⊢ 𝐷 ∈ ℤ
2 divalglem7.2 ⊢ 𝐷 ≠ 0
3 oveq1 ⊢ ( 𝑋 = if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) → ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) = ( if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) )
4 3 eleq1d ⊢ ( 𝑋 = if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) → ( ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ ( if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
5 4 notbid ⊢ ( 𝑋 = if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) → ( ¬ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ ¬ ( if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
6 5 imbi2d ⊢ ( 𝑋 = if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) → ( ( 𝐾 ≠ 0 → ¬ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ↔ ( 𝐾 ≠ 0 → ¬ ( if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) )
7 neeq1 ⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( 𝐾 ≠ 0 ↔ if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ≠ 0 ) )
8 oveq1 ⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · ( abs ‘ 𝐷 ) ) )
9 8 oveq2d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) = ( if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) + ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · ( abs ‘ 𝐷 ) ) ) )
10 9 eleq1d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( ( if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ ( if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) + ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
11 10 notbid ⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( ¬ ( if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ ¬ ( if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) + ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )
12 7 11 imbi12d ⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( ( 𝐾 ≠ 0 → ¬ ( if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ↔ ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ≠ 0 → ¬ ( if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) + ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) )
13 nnabscl ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → ( abs ‘ 𝐷 ) ∈ ℕ )
14 1 2 13 mp2an ⊢ ( abs ‘ 𝐷 ) ∈ ℕ
15 0z ⊢ 0 ∈ ℤ
16 0le0 ⊢ 0 ≤ 0
17 14 nngt0i ⊢ 0 < ( abs ‘ 𝐷 )
18 14 nnzi ⊢ ( abs ‘ 𝐷 ) ∈ ℤ
19 elfzm11 ⊢ ( ( 0 ∈ ℤ ∧ ( abs ‘ 𝐷 ) ∈ ℤ ) → ( 0 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ ( 0 ∈ ℤ ∧ 0 ≤ 0 ∧ 0 < ( abs ‘ 𝐷 ) ) ) )
20 15 18 19 mp2an ⊢ ( 0 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ ( 0 ∈ ℤ ∧ 0 ≤ 0 ∧ 0 < ( abs ‘ 𝐷 ) ) )
21 15 16 17 20 mpbir3an ⊢ 0 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) )
22 21 elimel ⊢ if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) )
23 15 elimel ⊢ if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ∈ ℤ
24 14 22 23 divalglem6 ⊢ ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ≠ 0 → ¬ ( if ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) , 𝑋 , 0 ) + ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) )
25 6 12 24 dedth2h ⊢ ( ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ≠ 0 → ¬ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) )