# Metamath Proof Explorer

## Theorem crctcshwlkn0lem3

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 crctcshwlkn0lem3 ${⊢}\left({\phi }\wedge {J}\in \left({N}-{S}+1\dots {N}\right)\right)\to {Q}\left({J}\right)={P}\left({J}+{S}-{N}\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 0zd ${⊢}{S}\in \left(1..^{N}\right)\to 0\in ℤ$
9 elfzoel2 ${⊢}{S}\in \left(1..^{N}\right)\to {N}\in ℤ$
10 elfzoelz ${⊢}{S}\in \left(1..^{N}\right)\to {S}\in ℤ$
11 9 10 zsubcld ${⊢}{S}\in \left(1..^{N}\right)\to {N}-{S}\in ℤ$
12 11 peano2zd ${⊢}{S}\in \left(1..^{N}\right)\to {N}-{S}+1\in ℤ$
13 elfzo1 ${⊢}{S}\in \left(1..^{N}\right)↔\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)$
14 nnre ${⊢}{S}\in ℕ\to {S}\in ℝ$
15 nnre ${⊢}{N}\in ℕ\to {N}\in ℝ$
16 posdif ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to \left({S}<{N}↔0<{N}-{S}\right)$
17 0red ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to 0\in ℝ$
18 resubcl ${⊢}\left({N}\in ℝ\wedge {S}\in ℝ\right)\to {N}-{S}\in ℝ$
19 18 ancoms ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to {N}-{S}\in ℝ$
20 ltle ${⊢}\left(0\in ℝ\wedge {N}-{S}\in ℝ\right)\to \left(0<{N}-{S}\to 0\le {N}-{S}\right)$
21 17 19 20 syl2anc ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to \left(0<{N}-{S}\to 0\le {N}-{S}\right)$
22 19 lep1d ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to {N}-{S}\le {N}-{S}+1$
23 1red ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to 1\in ℝ$
24 19 23 readdcld ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to {N}-{S}+1\in ℝ$
25 letr ${⊢}\left(0\in ℝ\wedge {N}-{S}\in ℝ\wedge {N}-{S}+1\in ℝ\right)\to \left(\left(0\le {N}-{S}\wedge {N}-{S}\le {N}-{S}+1\right)\to 0\le {N}-{S}+1\right)$
26 17 19 24 25 syl3anc ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left(0\le {N}-{S}\wedge {N}-{S}\le {N}-{S}+1\right)\to 0\le {N}-{S}+1\right)$
27 22 26 mpan2d ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to \left(0\le {N}-{S}\to 0\le {N}-{S}+1\right)$
28 21 27 syld ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to \left(0<{N}-{S}\to 0\le {N}-{S}+1\right)$
29 16 28 sylbid ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to \left({S}<{N}\to 0\le {N}-{S}+1\right)$
30 14 15 29 syl2an ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to \left({S}<{N}\to 0\le {N}-{S}+1\right)$
31 30 3impia ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to 0\le {N}-{S}+1$
32 13 31 sylbi ${⊢}{S}\in \left(1..^{N}\right)\to 0\le {N}-{S}+1$
33 eluz2 ${⊢}{N}-{S}+1\in {ℤ}_{\ge 0}↔\left(0\in ℤ\wedge {N}-{S}+1\in ℤ\wedge 0\le {N}-{S}+1\right)$
34 8 12 32 33 syl3anbrc ${⊢}{S}\in \left(1..^{N}\right)\to {N}-{S}+1\in {ℤ}_{\ge 0}$
35 1 34 syl ${⊢}{\phi }\to {N}-{S}+1\in {ℤ}_{\ge 0}$
36 fzss1 ${⊢}{N}-{S}+1\in {ℤ}_{\ge 0}\to \left({N}-{S}+1\dots {N}\right)\subseteq \left(0\dots {N}\right)$
37 35 36 syl ${⊢}{\phi }\to \left({N}-{S}+1\dots {N}\right)\subseteq \left(0\dots {N}\right)$
38 37 sselda ${⊢}\left({\phi }\wedge {J}\in \left({N}-{S}+1\dots {N}\right)\right)\to {J}\in \left(0\dots {N}\right)$
39 fvex ${⊢}{P}\left({J}+{S}\right)\in \mathrm{V}$
40 fvex ${⊢}{P}\left({J}+{S}-{N}\right)\in \mathrm{V}$
41 39 40 ifex ${⊢}if\left({J}\le {N}-{S},{P}\left({J}+{S}\right),{P}\left({J}+{S}-{N}\right)\right)\in \mathrm{V}$
42 41 a1i ${⊢}\left({\phi }\wedge {J}\in \left({N}-{S}+1\dots {N}\right)\right)\to if\left({J}\le {N}-{S},{P}\left({J}+{S}\right),{P}\left({J}+{S}-{N}\right)\right)\in \mathrm{V}$
43 2 7 38 42 fvmptd3 ${⊢}\left({\phi }\wedge {J}\in \left({N}-{S}+1\dots {N}\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)$
44 elfz2 ${⊢}{J}\in \left({N}-{S}+1\dots {N}\right)↔\left(\left({N}-{S}+1\in ℤ\wedge {N}\in ℤ\wedge {J}\in ℤ\right)\wedge \left({N}-{S}+1\le {J}\wedge {J}\le {N}\right)\right)$
45 zre ${⊢}{S}\in ℤ\to {S}\in ℝ$
46 zre ${⊢}{J}\in ℤ\to {J}\in ℝ$
47 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
48 46 47 anim12i ${⊢}\left({J}\in ℤ\wedge {N}\in ℤ\right)\to \left({J}\in ℝ\wedge {N}\in ℝ\right)$
49 simprr ${⊢}\left({S}\in ℝ\wedge \left({J}\in ℝ\wedge {N}\in ℝ\right)\right)\to {N}\in ℝ$
50 simpl ${⊢}\left({S}\in ℝ\wedge \left({J}\in ℝ\wedge {N}\in ℝ\right)\right)\to {S}\in ℝ$
51 49 50 resubcld ${⊢}\left({S}\in ℝ\wedge \left({J}\in ℝ\wedge {N}\in ℝ\right)\right)\to {N}-{S}\in ℝ$
52 51 ltp1d ${⊢}\left({S}\in ℝ\wedge \left({J}\in ℝ\wedge {N}\in ℝ\right)\right)\to {N}-{S}<{N}-{S}+1$
53 1red ${⊢}\left({S}\in ℝ\wedge \left({J}\in ℝ\wedge {N}\in ℝ\right)\right)\to 1\in ℝ$
54 51 53 readdcld ${⊢}\left({S}\in ℝ\wedge \left({J}\in ℝ\wedge {N}\in ℝ\right)\right)\to {N}-{S}+1\in ℝ$
55 simprl ${⊢}\left({S}\in ℝ\wedge \left({J}\in ℝ\wedge {N}\in ℝ\right)\right)\to {J}\in ℝ$
56 ltletr ${⊢}\left({N}-{S}\in ℝ\wedge {N}-{S}+1\in ℝ\wedge {J}\in ℝ\right)\to \left(\left({N}-{S}<{N}-{S}+1\wedge {N}-{S}+1\le {J}\right)\to {N}-{S}<{J}\right)$
57 51 54 55 56 syl3anc ${⊢}\left({S}\in ℝ\wedge \left({J}\in ℝ\wedge {N}\in ℝ\right)\right)\to \left(\left({N}-{S}<{N}-{S}+1\wedge {N}-{S}+1\le {J}\right)\to {N}-{S}<{J}\right)$
58 52 57 mpand ${⊢}\left({S}\in ℝ\wedge \left({J}\in ℝ\wedge {N}\in ℝ\right)\right)\to \left({N}-{S}+1\le {J}\to {N}-{S}<{J}\right)$
59 51 55 ltnled ${⊢}\left({S}\in ℝ\wedge \left({J}\in ℝ\wedge {N}\in ℝ\right)\right)\to \left({N}-{S}<{J}↔¬{J}\le {N}-{S}\right)$
60 58 59 sylibd ${⊢}\left({S}\in ℝ\wedge \left({J}\in ℝ\wedge {N}\in ℝ\right)\right)\to \left({N}-{S}+1\le {J}\to ¬{J}\le {N}-{S}\right)$
61 45 48 60 syl2an ${⊢}\left({S}\in ℤ\wedge \left({J}\in ℤ\wedge {N}\in ℤ\right)\right)\to \left({N}-{S}+1\le {J}\to ¬{J}\le {N}-{S}\right)$
62 61 expcom ${⊢}\left({J}\in ℤ\wedge {N}\in ℤ\right)\to \left({S}\in ℤ\to \left({N}-{S}+1\le {J}\to ¬{J}\le {N}-{S}\right)\right)$
63 62 ancoms ${⊢}\left({N}\in ℤ\wedge {J}\in ℤ\right)\to \left({S}\in ℤ\to \left({N}-{S}+1\le {J}\to ¬{J}\le {N}-{S}\right)\right)$
64 63 3adant1 ${⊢}\left({N}-{S}+1\in ℤ\wedge {N}\in ℤ\wedge {J}\in ℤ\right)\to \left({S}\in ℤ\to \left({N}-{S}+1\le {J}\to ¬{J}\le {N}-{S}\right)\right)$
65 10 64 syl5com ${⊢}{S}\in \left(1..^{N}\right)\to \left(\left({N}-{S}+1\in ℤ\wedge {N}\in ℤ\wedge {J}\in ℤ\right)\to \left({N}-{S}+1\le {J}\to ¬{J}\le {N}-{S}\right)\right)$
66 65 com13 ${⊢}{N}-{S}+1\le {J}\to \left(\left({N}-{S}+1\in ℤ\wedge {N}\in ℤ\wedge {J}\in ℤ\right)\to \left({S}\in \left(1..^{N}\right)\to ¬{J}\le {N}-{S}\right)\right)$
67 66 adantr ${⊢}\left({N}-{S}+1\le {J}\wedge {J}\le {N}\right)\to \left(\left({N}-{S}+1\in ℤ\wedge {N}\in ℤ\wedge {J}\in ℤ\right)\to \left({S}\in \left(1..^{N}\right)\to ¬{J}\le {N}-{S}\right)\right)$
68 67 impcom ${⊢}\left(\left({N}-{S}+1\in ℤ\wedge {N}\in ℤ\wedge {J}\in ℤ\right)\wedge \left({N}-{S}+1\le {J}\wedge {J}\le {N}\right)\right)\to \left({S}\in \left(1..^{N}\right)\to ¬{J}\le {N}-{S}\right)$
69 68 com12 ${⊢}{S}\in \left(1..^{N}\right)\to \left(\left(\left({N}-{S}+1\in ℤ\wedge {N}\in ℤ\wedge {J}\in ℤ\right)\wedge \left({N}-{S}+1\le {J}\wedge {J}\le {N}\right)\right)\to ¬{J}\le {N}-{S}\right)$
70 44 69 syl5bi ${⊢}{S}\in \left(1..^{N}\right)\to \left({J}\in \left({N}-{S}+1\dots {N}\right)\to ¬{J}\le {N}-{S}\right)$
71 1 70 syl ${⊢}{\phi }\to \left({J}\in \left({N}-{S}+1\dots {N}\right)\to ¬{J}\le {N}-{S}\right)$
72 71 imp ${⊢}\left({\phi }\wedge {J}\in \left({N}-{S}+1\dots {N}\right)\right)\to ¬{J}\le {N}-{S}$
73 72 iffalsed ${⊢}\left({\phi }\wedge {J}\in \left({N}-{S}+1\dots {N}\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}-{N}\right)$
74 43 73 eqtrd ${⊢}\left({\phi }\wedge {J}\in \left({N}-{S}+1\dots {N}\right)\right)\to {Q}\left({J}\right)={P}\left({J}+{S}-{N}\right)$