Metamath Proof Explorer

Theorem crctcshwlkn0lem7

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
crctcshwlkn0lem.h ⊢ H = F cyclShift S
crctcshwlkn0lem.n ⊢ N = F
crctcshwlkn0lem.f ⊢ φ → F ∈ Word A
crctcshwlkn0lem.p ⊢ φ → ∀ i ∈ 0 ..^ N if- P ⁡ i = P ⁡ i + 1 I ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ I ⁡ F ⁡ i
crctcshwlkn0lem.e ⊢ φ → P ⁡ N = P ⁡ 0
Assertion crctcshwlkn0lem7 ⊢ φ → ∀ j ∈ 0 ..^ N if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j

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 crctcshwlkn0lem.h ⊢ H = F cyclShift S
4 crctcshwlkn0lem.n ⊢ N = F
5 crctcshwlkn0lem.f ⊢ φ → F ∈ Word A
6 crctcshwlkn0lem.p ⊢ φ → ∀ i ∈ 0 ..^ N if- P ⁡ i = P ⁡ i + 1 I ⁡ F ⁡ i = P ⁡ i P ⁡ i P ⁡ i + 1 ⊆ I ⁡ F ⁡ i
7 crctcshwlkn0lem.e ⊢ φ → P ⁡ N = P ⁡ 0
8 1 2 3 4 5 6 crctcshwlkn0lem4 ⊢ φ → ∀ j ∈ 0 ..^ N − S if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j
9 eqidd ⊢ φ → N − S = N − S
10 1 2 3 4 5 6 7 crctcshwlkn0lem6 ⊢ φ ∧ N − S = N − S → if- Q ⁡ N − S = Q ⁡ N - S + 1 I ⁡ H ⁡ N − S = Q ⁡ N − S Q ⁡ N − S Q ⁡ N - S + 1 ⊆ I ⁡ H ⁡ N − S
11 9 10 mpdan ⊢ φ → if- Q ⁡ N − S = Q ⁡ N - S + 1 I ⁡ H ⁡ N − S = Q ⁡ N − S Q ⁡ N − S Q ⁡ N - S + 1 ⊆ I ⁡ H ⁡ N − S
12 ovex ⊢ N − S ∈ V
13 wkslem1 ⊢ j = N − S → if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j ↔ if- Q ⁡ N − S = Q ⁡ N - S + 1 I ⁡ H ⁡ N − S = Q ⁡ N − S Q ⁡ N − S Q ⁡ N - S + 1 ⊆ I ⁡ H ⁡ N − S
14 12 13 ralsn ⊢ ∀ j ∈ N − S if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j ↔ if- Q ⁡ N − S = Q ⁡ N - S + 1 I ⁡ H ⁡ N − S = Q ⁡ N − S Q ⁡ N − S Q ⁡ N - S + 1 ⊆ I ⁡ H ⁡ N − S
15 11 14 sylibr ⊢ φ → ∀ j ∈ N − S if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j
16 ralunb ⊢ ∀ j ∈ 0 ..^ N − S ∪ N − S if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j ↔ ∀ j ∈ 0 ..^ N − S if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j ∧ ∀ j ∈ N − S if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j
17 8 15 16 sylanbrc ⊢ φ → ∀ j ∈ 0 ..^ N − S ∪ N − S if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j
18 elfzo1 ⊢ S ∈ 1 ..^ N ↔ S ∈ ℕ ∧ N ∈ ℕ ∧ S < N
19 nnz ⊢ N ∈ ℕ → N ∈ ℤ
20 nnz ⊢ S ∈ ℕ → S ∈ ℤ
21 zsubcl ⊢ N ∈ ℤ ∧ S ∈ ℤ → N − S ∈ ℤ
22 19 20 21 syl2anr ⊢ S ∈ ℕ ∧ N ∈ ℕ → N − S ∈ ℤ
23 22 3adant3 ⊢ S ∈ ℕ ∧ N ∈ ℕ ∧ S < N → N − S ∈ ℤ
24 nnre ⊢ S ∈ ℕ → S ∈ ℝ
25 nnre ⊢ N ∈ ℕ → N ∈ ℝ
26 posdif ⊢ S ∈ ℝ ∧ N ∈ ℝ → S < N ↔ 0 < N − S
27 0re ⊢ 0 ∈ ℝ
28 resubcl ⊢ N ∈ ℝ ∧ S ∈ ℝ → N − S ∈ ℝ
29 28 ancoms ⊢ S ∈ ℝ ∧ N ∈ ℝ → N − S ∈ ℝ
30 ltle ⊢ 0 ∈ ℝ ∧ N − S ∈ ℝ → 0 < N − S → 0 ≤ N − S
31 27 29 30 sylancr ⊢ S ∈ ℝ ∧ N ∈ ℝ → 0 < N − S → 0 ≤ N − S
32 26 31 sylbid ⊢ S ∈ ℝ ∧ N ∈ ℝ → S < N → 0 ≤ N − S
33 24 25 32 syl2an ⊢ S ∈ ℕ ∧ N ∈ ℕ → S < N → 0 ≤ N − S
34 33 3impia ⊢ S ∈ ℕ ∧ N ∈ ℕ ∧ S < N → 0 ≤ N − S
35 elnn0z ⊢ N − S ∈ ℕ 0 ↔ N − S ∈ ℤ ∧ 0 ≤ N − S
36 23 34 35 sylanbrc ⊢ S ∈ ℕ ∧ N ∈ ℕ ∧ S < N → N − S ∈ ℕ 0
37 elnn0uz ⊢ N − S ∈ ℕ 0 ↔ N − S ∈ ℤ ≥ 0
38 36 37 sylib ⊢ S ∈ ℕ ∧ N ∈ ℕ ∧ S < N → N − S ∈ ℤ ≥ 0
39 fzosplitsn ⊢ N − S ∈ ℤ ≥ 0 → 0 ..^ N - S + 1 = 0 ..^ N − S ∪ N − S
40 38 39 syl ⊢ S ∈ ℕ ∧ N ∈ ℕ ∧ S < N → 0 ..^ N - S + 1 = 0 ..^ N − S ∪ N − S
41 18 40 sylbi ⊢ S ∈ 1 ..^ N → 0 ..^ N - S + 1 = 0 ..^ N − S ∪ N − S
42 1 41 syl ⊢ φ → 0 ..^ N - S + 1 = 0 ..^ N − S ∪ N − S
43 42 raleqdv ⊢ φ → ∀ j ∈ 0 ..^ N - S + 1 if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j ↔ ∀ j ∈ 0 ..^ N − S ∪ N − S if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j
44 17 43 mpbird ⊢ φ → ∀ j ∈ 0 ..^ N - S + 1 if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j
45 1 2 3 4 5 6 crctcshwlkn0lem5 ⊢ φ → ∀ j ∈ N - S + 1 ..^ N if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j
46 ralunb ⊢ ∀ j ∈ 0 ..^ N - S + 1 ∪ N - S + 1 ..^ N if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j ↔ ∀ j ∈ 0 ..^ N - S + 1 if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j ∧ ∀ j ∈ N - S + 1 ..^ N if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j
47 44 45 46 sylanbrc ⊢ φ → ∀ j ∈ 0 ..^ N - S + 1 ∪ N - S + 1 ..^ N if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j
48 nnsub ⊢ S ∈ ℕ ∧ N ∈ ℕ → S < N ↔ N − S ∈ ℕ
49 48 biimp3a ⊢ S ∈ ℕ ∧ N ∈ ℕ ∧ S < N → N − S ∈ ℕ
50 nnnn0 ⊢ N − S ∈ ℕ → N − S ∈ ℕ 0
51 peano2nn0 ⊢ N − S ∈ ℕ 0 → N - S + 1 ∈ ℕ 0
52 49 50 51 3syl ⊢ S ∈ ℕ ∧ N ∈ ℕ ∧ S < N → N - S + 1 ∈ ℕ 0
53 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
54 53 3ad2ant2 ⊢ S ∈ ℕ ∧ N ∈ ℕ ∧ S < N → N ∈ ℕ 0
55 25 anim1i ⊢ N ∈ ℕ ∧ S ∈ ℕ → N ∈ ℝ ∧ S ∈ ℕ
56 55 ancoms ⊢ S ∈ ℕ ∧ N ∈ ℕ → N ∈ ℝ ∧ S ∈ ℕ
57 crctcshwlkn0lem1 ⊢ N ∈ ℝ ∧ S ∈ ℕ → N - S + 1 ≤ N
58 56 57 syl ⊢ S ∈ ℕ ∧ N ∈ ℕ → N - S + 1 ≤ N
59 58 3adant3 ⊢ S ∈ ℕ ∧ N ∈ ℕ ∧ S < N → N - S + 1 ≤ N
60 elfz2nn0 ⊢ N - S + 1 ∈ 0 … N ↔ N - S + 1 ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ N - S + 1 ≤ N
61 52 54 59 60 syl3anbrc ⊢ S ∈ ℕ ∧ N ∈ ℕ ∧ S < N → N - S + 1 ∈ 0 … N
62 18 61 sylbi ⊢ S ∈ 1 ..^ N → N - S + 1 ∈ 0 … N
63 fzosplit ⊢ N - S + 1 ∈ 0 … N → 0 ..^ N = 0 ..^ N - S + 1 ∪ N - S + 1 ..^ N
64 1 62 63 3syl ⊢ φ → 0 ..^ N = 0 ..^ N - S + 1 ∪ N - S + 1 ..^ N
65 64 raleqdv ⊢ φ → ∀ j ∈ 0 ..^ N if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j ↔ ∀ j ∈ 0 ..^ N - S + 1 ∪ N - S + 1 ..^ N if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j
66 47 65 mpbird ⊢ φ → ∀ j ∈ 0 ..^ N if- Q ⁡ j = Q ⁡ j + 1 I ⁡ H ⁡ j = Q ⁡ j Q ⁡ j Q ⁡ j + 1 ⊆ I ⁡ H ⁡ j