Metamath Proof Explorer

Theorem crctcshwlkn0lem2

Description: Lemma for crctcshwlkn0 . (Contributed by AV, 12-Mar-2021)

Ref Expression
Hypotheses crctcshwlkn0lem.s ⊢ φ → S ∈ 1 ..^ N
crctcshwlkn0lem.q ⊢ Q = x ∈ 0 … N ⟼ if x ≤ N − S P ⁡ x + S P ⁡ x + S - N
Assertion crctcshwlkn0lem2 ⊢ φ ∧ J ∈ 0 … N − S → Q ⁡ J = P ⁡ J + S

Proof

Step Hyp Ref Expression
1 crctcshwlkn0lem.s ⊢ φ → S ∈ 1 ..^ N
2 crctcshwlkn0lem.q ⊢ Q = x ∈ 0 … N ⟼ if x ≤ N − S P ⁡ x + S P ⁡ x + S - N
3 breq1 ⊢ x = J → x ≤ N − S ↔ J ≤ N − S
4 fvoveq1 ⊢ x = J → P ⁡ x + S = P ⁡ J + S
5 oveq1 ⊢ x = J → x + S = J + S
6 5 fvoveq1d ⊢ x = J → P ⁡ x + S - N = P ⁡ J + S - N
7 3 4 6 ifbieq12d ⊢ x = J → if x ≤ N − S P ⁡ x + S P ⁡ x + S - N = if J ≤ N − S P ⁡ J + S P ⁡ J + S - N
8 fzo0ss1 ⊢ 1 ..^ N ⊆ 0 ..^ N
9 8 sseli ⊢ S ∈ 1 ..^ N → S ∈ 0 ..^ N
10 elfzoel2 ⊢ S ∈ 0 ..^ N → N ∈ ℤ
11 elfzonn0 ⊢ S ∈ 0 ..^ N → S ∈ ℕ 0
12 eluzmn ⊢ N ∈ ℤ ∧ S ∈ ℕ 0 → N ∈ ℤ ≥ N − S
13 10 11 12 syl2anc ⊢ S ∈ 0 ..^ N → N ∈ ℤ ≥ N − S
14 fzss2 ⊢ N ∈ ℤ ≥ N − S → 0 … N − S ⊆ 0 … N
15 13 14 syl ⊢ S ∈ 0 ..^ N → 0 … N − S ⊆ 0 … N
16 15 sseld ⊢ S ∈ 0 ..^ N → J ∈ 0 … N − S → J ∈ 0 … N
17 1 9 16 3syl ⊢ φ → J ∈ 0 … N − S → J ∈ 0 … N
18 17 imp ⊢ φ ∧ J ∈ 0 … N − S → J ∈ 0 … N
19 fvex ⊢ P ⁡ J + S ∈ V
20 fvex ⊢ P ⁡ J + S - N ∈ V
21 19 20 ifex ⊢ if J ≤ N − S P ⁡ J + S P ⁡ J + S - N ∈ V
22 21 a1i ⊢ φ ∧ J ∈ 0 … N − S → if J ≤ N − S P ⁡ J + S P ⁡ J + S - N ∈ V
23 2 7 18 22 fvmptd3 ⊢ φ ∧ J ∈ 0 … N − S → Q ⁡ J = if J ≤ N − S P ⁡ J + S P ⁡ J + S - N
24 elfzle2 ⊢ J ∈ 0 … N − S → J ≤ N − S
25 24 adantl ⊢ φ ∧ J ∈ 0 … N − S → J ≤ N − S
26 25 iftrued ⊢ φ ∧ J ∈ 0 … N − S → if J ≤ N − S P ⁡ J + S P ⁡ J + S - N = P ⁡ J + S
27 23 26 eqtrd ⊢ φ ∧ J ∈ 0 … N − S → Q ⁡ J = P ⁡ J + S