Metamath Proof Explorer

Theorem pfxccatin12lem4

Description: Lemma 4 for pfxccatin12 . (Contributed by Alexander van der Vekens, 30-Mar-2018) (Revised by Alexander van der Vekens, 23-May-2018)

Ref Expression
Assertion pfxccatin12lem4 ⊢ L ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ N ∈ ℤ → K ∈ 0 ..^ N − M ∧ ¬ K ∈ 0 ..^ L − M → K ∈ L − M ..^ L − M + N - L

Proof

Step Hyp Ref Expression
1 nn0z ⊢ L ∈ ℕ 0 → L ∈ ℤ
2 nn0z ⊢ M ∈ ℕ 0 → M ∈ ℤ
3 zsubcl ⊢ L ∈ ℤ ∧ M ∈ ℤ → L − M ∈ ℤ
4 1 2 3 syl2an ⊢ L ∈ ℕ 0 ∧ M ∈ ℕ 0 → L − M ∈ ℤ
5 4 3adant3 ⊢ L ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ N ∈ ℤ → L − M ∈ ℤ
6 elfzonelfzo ⊢ L − M ∈ ℤ → K ∈ 0 ..^ N − M ∧ ¬ K ∈ 0 ..^ L − M → K ∈ L − M ..^ N − M
7 6 imp ⊢ L − M ∈ ℤ ∧ K ∈ 0 ..^ N − M ∧ ¬ K ∈ 0 ..^ L − M → K ∈ L − M ..^ N − M
8 5 7 sylan ⊢ L ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ N ∈ ℤ ∧ K ∈ 0 ..^ N − M ∧ ¬ K ∈ 0 ..^ L − M → K ∈ L − M ..^ N − M
9 nn0cn ⊢ L ∈ ℕ 0 → L ∈ ℂ
10 nn0cn ⊢ M ∈ ℕ 0 → M ∈ ℂ
11 zcn ⊢ N ∈ ℤ → N ∈ ℂ
12 npncan3 ⊢ L ∈ ℂ ∧ M ∈ ℂ ∧ N ∈ ℂ → L − M + N - L = N − M
13 9 10 11 12 syl3an ⊢ L ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ N ∈ ℤ → L − M + N - L = N − M
14 13 oveq2d ⊢ L ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ N ∈ ℤ → L − M ..^ L − M + N - L = L − M ..^ N − M
15 14 eleq2d ⊢ L ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ N ∈ ℤ → K ∈ L − M ..^ L − M + N - L ↔ K ∈ L − M ..^ N − M
16 15 adantr ⊢ L ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ N ∈ ℤ ∧ K ∈ 0 ..^ N − M ∧ ¬ K ∈ 0 ..^ L − M → K ∈ L − M ..^ L − M + N - L ↔ K ∈ L − M ..^ N − M
17 8 16 mpbird ⊢ L ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ N ∈ ℤ ∧ K ∈ 0 ..^ N − M ∧ ¬ K ∈ 0 ..^ L − M → K ∈ L − M ..^ L − M + N - L
18 17 ex ⊢ L ∈ ℕ 0 ∧ M ∈ ℕ 0 ∧ N ∈ ℤ → K ∈ 0 ..^ N − M ∧ ¬ K ∈ 0 ..^ L − M → K ∈ L − M ..^ L − M + N - L