# Metamath Proof Explorer

## Theorem crctcshwlkn0lem2

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

Ref Expression
Hypotheses crctcshwlkn0lem.s ${⊢}{\phi }\to {S}\in \left(1..^{N}\right)$
crctcshwlkn0lem.q ${⊢}{Q}=\left({x}\in \left(0\dots {N}\right)⟼if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)\right)$
Assertion crctcshwlkn0lem2 ${⊢}\left({\phi }\wedge {J}\in \left(0\dots {N}-{S}\right)\right)\to {Q}\left({J}\right)={P}\left({J}+{S}\right)$

### Proof

Step Hyp Ref Expression
1 crctcshwlkn0lem.s ${⊢}{\phi }\to {S}\in \left(1..^{N}\right)$
2 crctcshwlkn0lem.q ${⊢}{Q}=\left({x}\in \left(0\dots {N}\right)⟼if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)\right)$
3 breq1 ${⊢}{x}={J}\to \left({x}\le {N}-{S}↔{J}\le {N}-{S}\right)$
4 fvoveq1 ${⊢}{x}={J}\to {P}\left({x}+{S}\right)={P}\left({J}+{S}\right)$
5 oveq1 ${⊢}{x}={J}\to {x}+{S}={J}+{S}$
6 5 fvoveq1d ${⊢}{x}={J}\to {P}\left({x}+{S}-{N}\right)={P}\left({J}+{S}-{N}\right)$
7 3 4 6 ifbieq12d ${⊢}{x}={J}\to if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)=if\left({J}\le {N}-{S},{P}\left({J}+{S}\right),{P}\left({J}+{S}-{N}\right)\right)$
8 fzo0ss1 ${⊢}\left(1..^{N}\right)\subseteq \left(0..^{N}\right)$
9 8 sseli ${⊢}{S}\in \left(1..^{N}\right)\to {S}\in \left(0..^{N}\right)$
10 elfzoel2 ${⊢}{S}\in \left(0..^{N}\right)\to {N}\in ℤ$
11 elfzonn0 ${⊢}{S}\in \left(0..^{N}\right)\to {S}\in {ℕ}_{0}$
12 eluzmn ${⊢}\left({N}\in ℤ\wedge {S}\in {ℕ}_{0}\right)\to {N}\in {ℤ}_{\ge \left({N}-{S}\right)}$
13 10 11 12 syl2anc ${⊢}{S}\in \left(0..^{N}\right)\to {N}\in {ℤ}_{\ge \left({N}-{S}\right)}$
14 fzss2 ${⊢}{N}\in {ℤ}_{\ge \left({N}-{S}\right)}\to \left(0\dots {N}-{S}\right)\subseteq \left(0\dots {N}\right)$
15 13 14 syl ${⊢}{S}\in \left(0..^{N}\right)\to \left(0\dots {N}-{S}\right)\subseteq \left(0\dots {N}\right)$
16 15 sseld ${⊢}{S}\in \left(0..^{N}\right)\to \left({J}\in \left(0\dots {N}-{S}\right)\to {J}\in \left(0\dots {N}\right)\right)$
17 1 9 16 3syl ${⊢}{\phi }\to \left({J}\in \left(0\dots {N}-{S}\right)\to {J}\in \left(0\dots {N}\right)\right)$
18 17 imp ${⊢}\left({\phi }\wedge {J}\in \left(0\dots {N}-{S}\right)\right)\to {J}\in \left(0\dots {N}\right)$
19 fvex ${⊢}{P}\left({J}+{S}\right)\in \mathrm{V}$
20 fvex ${⊢}{P}\left({J}+{S}-{N}\right)\in \mathrm{V}$
21 19 20 ifex ${⊢}if\left({J}\le {N}-{S},{P}\left({J}+{S}\right),{P}\left({J}+{S}-{N}\right)\right)\in \mathrm{V}$
22 21 a1i ${⊢}\left({\phi }\wedge {J}\in \left(0\dots {N}-{S}\right)\right)\to if\left({J}\le {N}-{S},{P}\left({J}+{S}\right),{P}\left({J}+{S}-{N}\right)\right)\in \mathrm{V}$
23 2 7 18 22 fvmptd3 ${⊢}\left({\phi }\wedge {J}\in \left(0\dots {N}-{S}\right)\right)\to {Q}\left({J}\right)=if\left({J}\le {N}-{S},{P}\left({J}+{S}\right),{P}\left({J}+{S}-{N}\right)\right)$
24 elfzle2 ${⊢}{J}\in \left(0\dots {N}-{S}\right)\to {J}\le {N}-{S}$
25 24 adantl ${⊢}\left({\phi }\wedge {J}\in \left(0\dots {N}-{S}\right)\right)\to {J}\le {N}-{S}$
26 25 iftrued ${⊢}\left({\phi }\wedge {J}\in \left(0\dots {N}-{S}\right)\right)\to if\left({J}\le {N}-{S},{P}\left({J}+{S}\right),{P}\left({J}+{S}-{N}\right)\right)={P}\left({J}+{S}\right)$
27 23 26 eqtrd ${⊢}\left({\phi }\wedge {J}\in \left(0\dots {N}-{S}\right)\right)\to {Q}\left({J}\right)={P}\left({J}+{S}\right)$