Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  crctcshwlkn0lem6 Structured version   Visualization version   GIF version

Theorem crctcshwlkn0lem6 26610
 Description: Lemma for crctcshwlkn0 26616. (Contributed by AV, 12-Mar-2021.)
Hypotheses
Ref Expression
crctcshwlkn0lem.s (𝜑𝑆 ∈ (1..^𝑁))
crctcshwlkn0lem.q 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
crctcshwlkn0lem.h 𝐻 = (𝐹 cyclShift 𝑆)
crctcshwlkn0lem.n 𝑁 = (#‘𝐹)
crctcshwlkn0lem.f (𝜑𝐹 ∈ Word 𝐴)
crctcshwlkn0lem.p (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹𝑖)) = {(𝑃𝑖)}, {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹𝑖))))
crctcshwlkn0lem.e (𝜑 → (𝑃𝑁) = (𝑃‘0))
Assertion
Ref Expression
crctcshwlkn0lem6 ((𝜑𝐽 = (𝑁𝑆)) → if-((𝑄𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻𝐽)) = {(𝑄𝐽)}, {(𝑄𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻𝐽))))
Distinct variable groups:   𝑥,𝐽   𝑥,𝑁   𝑥,𝑃   𝑥,𝑆   𝜑,𝑥   𝑖,𝐹   𝑖,𝐼   𝑖,𝑁   𝑃,𝑖   𝑆,𝑖   𝜑,𝑖
Allowed substitution hints:   𝐴(𝑥,𝑖)   𝑄(𝑥,𝑖)   𝐹(𝑥)   𝐻(𝑥,𝑖)   𝐼(𝑥)   𝐽(𝑖)

Proof of Theorem crctcshwlkn0lem6
StepHypRef Expression
1 oveq1 6622 . . . . . . . . 9 (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
2 0p1e1 11092 . . . . . . . . 9 (0 + 1) = 1
31, 2syl6eq 2671 . . . . . . . 8 (𝑖 = 0 → (𝑖 + 1) = 1)
4 wkslem2 26408 . . . . . . . 8 ((𝑖 = 0 ∧ (𝑖 + 1) = 1) → (if-((𝑃𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹𝑖)) = {(𝑃𝑖)}, {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹𝑖))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
53, 4mpdan 701 . . . . . . 7 (𝑖 = 0 → (if-((𝑃𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹𝑖)) = {(𝑃𝑖)}, {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹𝑖))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
6 crctcshwlkn0lem.p . . . . . . 7 (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹𝑖)) = {(𝑃𝑖)}, {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹𝑖))))
7 crctcshwlkn0lem.s . . . . . . . . 9 (𝜑𝑆 ∈ (1..^𝑁))
8 elfzo1 12474 . . . . . . . . . 10 (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁))
9 simp2 1060 . . . . . . . . . 10 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ∈ ℕ)
108, 9sylbi 207 . . . . . . . . 9 (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℕ)
117, 10syl 17 . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
12 lbfzo0 12464 . . . . . . . 8 (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
1311, 12sylibr 224 . . . . . . 7 (𝜑 → 0 ∈ (0..^𝑁))
145, 6, 13rspcdva 3305 . . . . . 6 (𝜑 → if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
15 crctcshwlkn0lem.e . . . . . . 7 (𝜑 → (𝑃𝑁) = (𝑃‘0))
16 eqeq1 2625 . . . . . . . 8 ((𝑃𝑁) = (𝑃‘0) → ((𝑃𝑁) = (𝑃‘1) ↔ (𝑃‘0) = (𝑃‘1)))
17 sneq 4165 . . . . . . . . 9 ((𝑃𝑁) = (𝑃‘0) → {(𝑃𝑁)} = {(𝑃‘0)})
1817eqeq2d 2631 . . . . . . . 8 ((𝑃𝑁) = (𝑃‘0) → ((𝐼‘(𝐹‘0)) = {(𝑃𝑁)} ↔ (𝐼‘(𝐹‘0)) = {(𝑃‘0)}))
19 preq1 4245 . . . . . . . . 9 ((𝑃𝑁) = (𝑃‘0) → {(𝑃𝑁), (𝑃‘1)} = {(𝑃‘0), (𝑃‘1)})
2019sseq1d 3617 . . . . . . . 8 ((𝑃𝑁) = (𝑃‘0) → ({(𝑃𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ↔ {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
2116, 18, 20ifpbi123d 1026 . . . . . . 7 ((𝑃𝑁) = (𝑃‘0) → (if-((𝑃𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
2215, 21syl 17 . . . . . 6 (𝜑 → (if-((𝑃𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
2314, 22mpbird 247 . . . . 5 (𝜑 → if-((𝑃𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
24 nncn 10988 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
25 nncn 10988 . . . . . . . . . 10 (𝑆 ∈ ℕ → 𝑆 ∈ ℂ)
26 npcan 10250 . . . . . . . . . 10 ((𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ) → ((𝑁𝑆) + 𝑆) = 𝑁)
2724, 25, 26syl2anr 495 . . . . . . . . 9 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁𝑆) + 𝑆) = 𝑁)
28 simpr 477 . . . . . . . . . 10 (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁𝑆) + 𝑆) = 𝑁) → ((𝑁𝑆) + 𝑆) = 𝑁)
29 oveq1 6622 . . . . . . . . . . 11 (((𝑁𝑆) + 𝑆) = 𝑁 → (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = (𝑁 mod (#‘𝐹)))
30 crctcshwlkn0lem.n . . . . . . . . . . . . . . 15 𝑁 = (#‘𝐹)
3130eqcomi 2630 . . . . . . . . . . . . . 14 (#‘𝐹) = 𝑁
3231a1i 11 . . . . . . . . . . . . 13 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (#‘𝐹) = 𝑁)
3332oveq2d 6631 . . . . . . . . . . . 12 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod (#‘𝐹)) = (𝑁 mod 𝑁))
34 nnrp 11802 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ+)
35 modid0 12652 . . . . . . . . . . . . . 14 (𝑁 ∈ ℝ+ → (𝑁 mod 𝑁) = 0)
3634, 35syl 17 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (𝑁 mod 𝑁) = 0)
3736adantl 482 . . . . . . . . . . . 12 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod 𝑁) = 0)
3833, 37eqtrd 2655 . . . . . . . . . . 11 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod (#‘𝐹)) = 0)
3929, 38sylan9eqr 2677 . . . . . . . . . 10 (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁𝑆) + 𝑆) = 𝑁) → (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0)
40 simpl 473 . . . . . . . . . 10 (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁𝑆) + 𝑆) = 𝑁) → (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ))
4128, 39, 403jca 1240 . . . . . . . . 9 (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁𝑆) + 𝑆) = 𝑁) → (((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
4227, 41mpdan 701 . . . . . . . 8 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
43423adant3 1079 . . . . . . 7 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
448, 43sylbi 207 . . . . . 6 (𝑆 ∈ (1..^𝑁) → (((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
45 simp1 1059 . . . . . . . . 9 ((((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑁𝑆) + 𝑆) = 𝑁)
4645fveq2d 6162 . . . . . . . 8 ((((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝑃‘((𝑁𝑆) + 𝑆)) = (𝑃𝑁))
4746eqeq1d 2623 . . . . . . 7 ((((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃‘((𝑁𝑆) + 𝑆)) = (𝑃‘1) ↔ (𝑃𝑁) = (𝑃‘1)))
48 simp2 1060 . . . . . . . . . 10 ((((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0)
4948fveq2d 6162 . . . . . . . . 9 ((((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹))) = (𝐹‘0))
5049fveq2d 6162 . . . . . . . 8 ((((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) = (𝐼‘(𝐹‘0)))
5146sneqd 4167 . . . . . . . 8 ((((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → {(𝑃‘((𝑁𝑆) + 𝑆))} = {(𝑃𝑁)})
5250, 51eqeq12d 2636 . . . . . . 7 ((((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) = {(𝑃‘((𝑁𝑆) + 𝑆))} ↔ (𝐼‘(𝐹‘0)) = {(𝑃𝑁)}))
5346preq1d 4251 . . . . . . . 8 ((((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → {(𝑃‘((𝑁𝑆) + 𝑆)), (𝑃‘1)} = {(𝑃𝑁), (𝑃‘1)})
5453, 50sseq12d 3619 . . . . . . 7 ((((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ({(𝑃‘((𝑁𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) ↔ {(𝑃𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
5547, 52, 54ifpbi123d 1026 . . . . . 6 ((((𝑁𝑆) + 𝑆) = 𝑁 ∧ (((𝑁𝑆) + 𝑆) mod (#‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (if-((𝑃‘((𝑁𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) = {(𝑃‘((𝑁𝑆) + 𝑆))}, {(𝑃‘((𝑁𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹))))) ↔ if-((𝑃𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
567, 44, 553syl 18 . . . . 5 (𝜑 → (if-((𝑃‘((𝑁𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) = {(𝑃‘((𝑁𝑆) + 𝑆))}, {(𝑃‘((𝑁𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹))))) ↔ if-((𝑃𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃𝑁)}, {(𝑃𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
5723, 56mpbird 247 . . . 4 (𝜑 → if-((𝑃‘((𝑁𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) = {(𝑃‘((𝑁𝑆) + 𝑆))}, {(𝑃‘((𝑁𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹))))))
58 nnsub 11019 . . . . . . . . . . 11 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 ↔ (𝑁𝑆) ∈ ℕ))
5958biimp3a 1429 . . . . . . . . . 10 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁𝑆) ∈ ℕ)
6059nnnn0d 11311 . . . . . . . . 9 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁𝑆) ∈ ℕ0)
618, 60sylbi 207 . . . . . . . 8 (𝑆 ∈ (1..^𝑁) → (𝑁𝑆) ∈ ℕ0)
627, 61syl 17 . . . . . . 7 (𝜑 → (𝑁𝑆) ∈ ℕ0)
63 nn0fz0 12394 . . . . . . 7 ((𝑁𝑆) ∈ ℕ0 ↔ (𝑁𝑆) ∈ (0...(𝑁𝑆)))
6462, 63sylib 208 . . . . . 6 (𝜑 → (𝑁𝑆) ∈ (0...(𝑁𝑆)))
65 crctcshwlkn0lem.q . . . . . . 7 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
667, 65crctcshwlkn0lem2 26606 . . . . . 6 ((𝜑 ∧ (𝑁𝑆) ∈ (0...(𝑁𝑆))) → (𝑄‘(𝑁𝑆)) = (𝑃‘((𝑁𝑆) + 𝑆)))
6764, 66mpdan 701 . . . . 5 (𝜑 → (𝑄‘(𝑁𝑆)) = (𝑃‘((𝑁𝑆) + 𝑆)))
68 elfzoel2 12426 . . . . . . . . . . . . 13 (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℤ)
69 elfzoelz 12427 . . . . . . . . . . . . 13 (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ ℤ)
7068, 69zsubcld 11447 . . . . . . . . . . . 12 (𝑆 ∈ (1..^𝑁) → (𝑁𝑆) ∈ ℤ)
7170peano2zd 11445 . . . . . . . . . . 11 (𝑆 ∈ (1..^𝑁) → ((𝑁𝑆) + 1) ∈ ℤ)
72 nnre 10987 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
7372anim1i 591 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑆 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ))
7473ancoms 469 . . . . . . . . . . . . . 14 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ))
75 crctcshwlkn0lem1 26605 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ) → ((𝑁𝑆) + 1) ≤ 𝑁)
7674, 75syl 17 . . . . . . . . . . . . 13 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁𝑆) + 1) ≤ 𝑁)
77763adant3 1079 . . . . . . . . . . . 12 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑁𝑆) + 1) ≤ 𝑁)
788, 77sylbi 207 . . . . . . . . . . 11 (𝑆 ∈ (1..^𝑁) → ((𝑁𝑆) + 1) ≤ 𝑁)
7971, 68, 783jca 1240 . . . . . . . . . 10 (𝑆 ∈ (1..^𝑁) → (((𝑁𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁𝑆) + 1) ≤ 𝑁))
807, 79syl 17 . . . . . . . . 9 (𝜑 → (((𝑁𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁𝑆) + 1) ≤ 𝑁))
81 eluz2 11653 . . . . . . . . 9 (𝑁 ∈ (ℤ‘((𝑁𝑆) + 1)) ↔ (((𝑁𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁𝑆) + 1) ≤ 𝑁))
8280, 81sylibr 224 . . . . . . . 8 (𝜑𝑁 ∈ (ℤ‘((𝑁𝑆) + 1)))
83 eluzfz1 12306 . . . . . . . 8 (𝑁 ∈ (ℤ‘((𝑁𝑆) + 1)) → ((𝑁𝑆) + 1) ∈ (((𝑁𝑆) + 1)...𝑁))
8482, 83syl 17 . . . . . . 7 (𝜑 → ((𝑁𝑆) + 1) ∈ (((𝑁𝑆) + 1)...𝑁))
857, 65crctcshwlkn0lem3 26607 . . . . . . 7 ((𝜑 ∧ ((𝑁𝑆) + 1) ∈ (((𝑁𝑆) + 1)...𝑁)) → (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘((((𝑁𝑆) + 1) + 𝑆) − 𝑁)))
8684, 85mpdan 701 . . . . . 6 (𝜑 → (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘((((𝑁𝑆) + 1) + 𝑆) − 𝑁)))
87 subcl 10240 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑁𝑆) ∈ ℂ)
8887ancoms 469 . . . . . . . . . . . . 13 ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑁𝑆) ∈ ℂ)
89 ax-1cn 9954 . . . . . . . . . . . . 13 1 ∈ ℂ
90 pncan2 10248 . . . . . . . . . . . . . 14 (((𝑁𝑆) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁𝑆) + 1) − (𝑁𝑆)) = 1)
9190eqcomd 2627 . . . . . . . . . . . . 13 (((𝑁𝑆) ∈ ℂ ∧ 1 ∈ ℂ) → 1 = (((𝑁𝑆) + 1) − (𝑁𝑆)))
9288, 89, 91sylancl 693 . . . . . . . . . . . 12 ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 1 = (((𝑁𝑆) + 1) − (𝑁𝑆)))
93 peano2cn 10168 . . . . . . . . . . . . . 14 ((𝑁𝑆) ∈ ℂ → ((𝑁𝑆) + 1) ∈ ℂ)
9488, 93syl 17 . . . . . . . . . . . . 13 ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁𝑆) + 1) ∈ ℂ)
95 simpr 477 . . . . . . . . . . . . 13 ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 𝑁 ∈ ℂ)
96 simpl 473 . . . . . . . . . . . . 13 ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 𝑆 ∈ ℂ)
9794, 95, 96subsub3d 10382 . . . . . . . . . . . 12 ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((𝑁𝑆) + 1) − (𝑁𝑆)) = ((((𝑁𝑆) + 1) + 𝑆) − 𝑁))
9892, 97eqtr2d 2656 . . . . . . . . . . 11 ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((((𝑁𝑆) + 1) + 𝑆) − 𝑁) = 1)
9925, 24, 98syl2an 494 . . . . . . . . . 10 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((𝑁𝑆) + 1) + 𝑆) − 𝑁) = 1)
100993adant3 1079 . . . . . . . . 9 ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((((𝑁𝑆) + 1) + 𝑆) − 𝑁) = 1)
1018, 100sylbi 207 . . . . . . . 8 (𝑆 ∈ (1..^𝑁) → ((((𝑁𝑆) + 1) + 𝑆) − 𝑁) = 1)
1027, 101syl 17 . . . . . . 7 (𝜑 → ((((𝑁𝑆) + 1) + 𝑆) − 𝑁) = 1)
103102fveq2d 6162 . . . . . 6 (𝜑 → (𝑃‘((((𝑁𝑆) + 1) + 𝑆) − 𝑁)) = (𝑃‘1))
10486, 103eqtrd 2655 . . . . 5 (𝜑 → (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘1))
105 crctcshwlkn0lem.h . . . . . . 7 𝐻 = (𝐹 cyclShift 𝑆)
106105fveq1i 6159 . . . . . 6 (𝐻‘(𝑁𝑆)) = ((𝐹 cyclShift 𝑆)‘(𝑁𝑆))
107 crctcshwlkn0lem.f . . . . . . . . 9 (𝜑𝐹 ∈ Word 𝐴)
108107adantr 481 . . . . . . . 8 ((𝜑𝑆 ∈ (1..^𝑁)) → 𝐹 ∈ Word 𝐴)
10969adantl 482 . . . . . . . 8 ((𝜑𝑆 ∈ (1..^𝑁)) → 𝑆 ∈ ℤ)
110 elfzofz 12442 . . . . . . . . . . 11 (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ (1...𝑁))
111 ubmelfzo 12489 . . . . . . . . . . 11 (𝑆 ∈ (1...𝑁) → (𝑁𝑆) ∈ (0..^𝑁))
112110, 111syl 17 . . . . . . . . . 10 (𝑆 ∈ (1..^𝑁) → (𝑁𝑆) ∈ (0..^𝑁))
113112adantl 482 . . . . . . . . 9 ((𝜑𝑆 ∈ (1..^𝑁)) → (𝑁𝑆) ∈ (0..^𝑁))
11431oveq2i 6626 . . . . . . . . 9 (0..^(#‘𝐹)) = (0..^𝑁)
115113, 114syl6eleqr 2709 . . . . . . . 8 ((𝜑𝑆 ∈ (1..^𝑁)) → (𝑁𝑆) ∈ (0..^(#‘𝐹)))
116 cshwidxmod 13502 . . . . . . . 8 ((𝐹 ∈ Word 𝐴𝑆 ∈ ℤ ∧ (𝑁𝑆) ∈ (0..^(#‘𝐹))) → ((𝐹 cyclShift 𝑆)‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹))))
117108, 109, 115, 116syl3anc 1323 . . . . . . 7 ((𝜑𝑆 ∈ (1..^𝑁)) → ((𝐹 cyclShift 𝑆)‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹))))
1187, 117mpdan 701 . . . . . 6 (𝜑 → ((𝐹 cyclShift 𝑆)‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹))))
119106, 118syl5eq 2667 . . . . 5 (𝜑 → (𝐻‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹))))
120 simp1 1059 . . . . . . 7 (((𝑄‘(𝑁𝑆)) = (𝑃‘((𝑁𝑆) + 𝑆)) ∧ (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) → (𝑄‘(𝑁𝑆)) = (𝑃‘((𝑁𝑆) + 𝑆)))
121 simp2 1060 . . . . . . 7 (((𝑄‘(𝑁𝑆)) = (𝑃‘((𝑁𝑆) + 𝑆)) ∧ (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) → (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘1))
122120, 121eqeq12d 2636 . . . . . 6 (((𝑄‘(𝑁𝑆)) = (𝑃‘((𝑁𝑆) + 𝑆)) ∧ (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) → ((𝑄‘(𝑁𝑆)) = (𝑄‘((𝑁𝑆) + 1)) ↔ (𝑃‘((𝑁𝑆) + 𝑆)) = (𝑃‘1)))
123 simp3 1061 . . . . . . . 8 (((𝑄‘(𝑁𝑆)) = (𝑃‘((𝑁𝑆) + 𝑆)) ∧ (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) → (𝐻‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹))))
124123fveq2d 6162 . . . . . . 7 (((𝑄‘(𝑁𝑆)) = (𝑃‘((𝑁𝑆) + 𝑆)) ∧ (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) → (𝐼‘(𝐻‘(𝑁𝑆))) = (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))))
125120sneqd 4167 . . . . . . 7 (((𝑄‘(𝑁𝑆)) = (𝑃‘((𝑁𝑆) + 𝑆)) ∧ (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) → {(𝑄‘(𝑁𝑆))} = {(𝑃‘((𝑁𝑆) + 𝑆))})
126124, 125eqeq12d 2636 . . . . . 6 (((𝑄‘(𝑁𝑆)) = (𝑃‘((𝑁𝑆) + 𝑆)) ∧ (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) → ((𝐼‘(𝐻‘(𝑁𝑆))) = {(𝑄‘(𝑁𝑆))} ↔ (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) = {(𝑃‘((𝑁𝑆) + 𝑆))}))
127120, 121preq12d 4253 . . . . . . 7 (((𝑄‘(𝑁𝑆)) = (𝑃‘((𝑁𝑆) + 𝑆)) ∧ (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) → {(𝑄‘(𝑁𝑆)), (𝑄‘((𝑁𝑆) + 1))} = {(𝑃‘((𝑁𝑆) + 𝑆)), (𝑃‘1)})
128127, 124sseq12d 3619 . . . . . 6 (((𝑄‘(𝑁𝑆)) = (𝑃‘((𝑁𝑆) + 𝑆)) ∧ (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) → ({(𝑄‘(𝑁𝑆)), (𝑄‘((𝑁𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁𝑆))) ↔ {(𝑃‘((𝑁𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹))))))
129122, 126, 128ifpbi123d 1026 . . . . 5 (((𝑄‘(𝑁𝑆)) = (𝑃‘((𝑁𝑆) + 𝑆)) ∧ (𝑄‘((𝑁𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁𝑆)) = (𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) → (if-((𝑄‘(𝑁𝑆)) = (𝑄‘((𝑁𝑆) + 1)), (𝐼‘(𝐻‘(𝑁𝑆))) = {(𝑄‘(𝑁𝑆))}, {(𝑄‘(𝑁𝑆)), (𝑄‘((𝑁𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁𝑆)))) ↔ if-((𝑃‘((𝑁𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) = {(𝑃‘((𝑁𝑆) + 𝑆))}, {(𝑃‘((𝑁𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))))))
13067, 104, 119, 129syl3anc 1323 . . . 4 (𝜑 → (if-((𝑄‘(𝑁𝑆)) = (𝑄‘((𝑁𝑆) + 1)), (𝐼‘(𝐻‘(𝑁𝑆))) = {(𝑄‘(𝑁𝑆))}, {(𝑄‘(𝑁𝑆)), (𝑄‘((𝑁𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁𝑆)))) ↔ if-((𝑃‘((𝑁𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))) = {(𝑃‘((𝑁𝑆) + 𝑆))}, {(𝑃‘((𝑁𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁𝑆) + 𝑆) mod (#‘𝐹)))))))
13157, 130mpbird 247 . . 3 (𝜑 → if-((𝑄‘(𝑁𝑆)) = (𝑄‘((𝑁𝑆) + 1)), (𝐼‘(𝐻‘(𝑁𝑆))) = {(𝑄‘(𝑁𝑆))}, {(𝑄‘(𝑁𝑆)), (𝑄‘((𝑁𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁𝑆)))))
132131adantr 481 . 2 ((𝜑𝐽 = (𝑁𝑆)) → if-((𝑄‘(𝑁𝑆)) = (𝑄‘((𝑁𝑆) + 1)), (𝐼‘(𝐻‘(𝑁𝑆))) = {(𝑄‘(𝑁𝑆))}, {(𝑄‘(𝑁𝑆)), (𝑄‘((𝑁𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁𝑆)))))
133 wkslem1 26407 . . 3 (𝐽 = (𝑁𝑆) → (if-((𝑄𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻𝐽)) = {(𝑄𝐽)}, {(𝑄𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻𝐽))) ↔ if-((𝑄‘(𝑁𝑆)) = (𝑄‘((𝑁𝑆) + 1)), (𝐼‘(𝐻‘(𝑁𝑆))) = {(𝑄‘(𝑁𝑆))}, {(𝑄‘(𝑁𝑆)), (𝑄‘((𝑁𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁𝑆))))))
134133adantl 482 . 2 ((𝜑𝐽 = (𝑁𝑆)) → (if-((𝑄𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻𝐽)) = {(𝑄𝐽)}, {(𝑄𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻𝐽))) ↔ if-((𝑄‘(𝑁𝑆)) = (𝑄‘((𝑁𝑆) + 1)), (𝐼‘(𝐻‘(𝑁𝑆))) = {(𝑄‘(𝑁𝑆))}, {(𝑄‘(𝑁𝑆)), (𝑄‘((𝑁𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁𝑆))))))
135132, 134mpbird 247 1 ((𝜑𝐽 = (𝑁𝑆)) → if-((𝑄𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻𝐽)) = {(𝑄𝐽)}, {(𝑄𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻𝐽))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  if-wif 1011   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987  ∀wral 2908   ⊆ wss 3560  ifcif 4064  {csn 4155  {cpr 4157   class class class wbr 4623   ↦ cmpt 4683  ‘cfv 5857  (class class class)co 6615  ℂcc 9894  ℝcr 9895  0cc0 9896  1c1 9897   + caddc 9899   < clt 10034   ≤ cle 10035   − cmin 10226  ℕcn 10980  ℕ0cn0 11252  ℤcz 11337  ℤ≥cuz 11647  ℝ+crp 11792  ...cfz 12284  ..^cfzo 12422   mod cmo 12624  #chash 13073  Word cword 13246   cyclShift ccsh 13487 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ifp 1012  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-oadd 7524  df-er 7702  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-sup 8308  df-inf 8309  df-card 8725  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-n0 11253  df-z 11338  df-uz 11648  df-rp 11793  df-fz 12285  df-fzo 12423  df-fl 12549  df-mod 12625  df-hash 13074  df-word 13254  df-concat 13256  df-substr 13258  df-csh 13488 This theorem is referenced by:  crctcshwlkn0lem7  26611
 Copyright terms: Public domain W3C validator