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

Theorem extwwlkfablem2 26605
 Description: Lemma 2 for extwwlkfab 26617. (Contributed by Alexander van der Vekens, 15-Sep-2018.)
Hypothesis
Ref Expression
numclwwlk.c 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))
Assertion
Ref Expression
extwwlkfablem2 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ (𝐶‘(𝑁 − 2)))
Distinct variable groups:   𝑛,𝐸   𝑛,𝑁   𝑛,𝑉
Allowed substitution hints:   𝐶(𝑤,𝑛)   𝐸(𝑤)   𝑁(𝑤)   𝑉(𝑤)   𝑋(𝑤,𝑛)

Proof of Theorem extwwlkfablem2
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 usgrav 25867 . . . . . . . . . . 11 (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V))
2 uzuzle23 11605 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ (ℤ‘2))
3 eluzge2nn0 11603 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘2) → 𝑁 ∈ ℕ0)
42, 3syl 17 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℕ0)
51, 4anim12i 588 . . . . . . . . . 10 ((𝑉 USGrph 𝐸𝑁 ∈ (ℤ‘3)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0))
6 df-3an 1033 . . . . . . . . . 10 ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0) ↔ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0))
75, 6sylibr 223 . . . . . . . . 9 ((𝑉 USGrph 𝐸𝑁 ∈ (ℤ‘3)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0))
8 isclwwlkn 26297 . . . . . . . . 9 ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁)))
97, 8syl 17 . . . . . . . 8 ((𝑉 USGrph 𝐸𝑁 ∈ (ℤ‘3)) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁)))
1093adant2 1073 . . . . . . 7 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁)))
11 isclwwlk 26296 . . . . . . . . . 10 ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑤 ∈ (𝑉 ClWWalks 𝐸) ↔ (𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸)))
1211anbi1d 737 . . . . . . . . 9 ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁) ↔ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)))
131, 12syl 17 . . . . . . . 8 (𝑉 USGrph 𝐸 → ((𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁) ↔ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)))
14133ad2ant1 1075 . . . . . . 7 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → ((𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁) ↔ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)))
1510, 14bitrd 267 . . . . . 6 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)))
16 swrdcl 13271 . . . . . . . . . . . 12 (𝑤 ∈ Word 𝑉 → (𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉)
17163ad2ant1 1075 . . . . . . . . . . 11 ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) → (𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉)
1817adantr 480 . . . . . . . . . 10 (((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁) → (𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉)
1918ad2antlr 759 . . . . . . . . 9 (((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉)
20 oveq1 6556 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝑤) = 𝑁 → ((#‘𝑤) − 1) = (𝑁 − 1))
2120adantr 480 . . . . . . . . . . . . . . . . . . 19 (((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3)) → ((#‘𝑤) − 1) = (𝑁 − 1))
22 1le3 11121 . . . . . . . . . . . . . . . . . . . . . 22 1 ≤ 3
23 1red 9934 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘3) → 1 ∈ ℝ)
24 3re 10971 . . . . . . . . . . . . . . . . . . . . . . . 24 3 ∈ ℝ
2524a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘3) → 3 ∈ ℝ)
26 eluzelre 11574 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℝ)
2723, 25, 26lesub2d 10514 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (ℤ‘3) → (1 ≤ 3 ↔ (𝑁 − 3) ≤ (𝑁 − 1)))
2822, 27mpbii 222 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (ℤ‘3) → (𝑁 − 3) ≤ (𝑁 − 1))
29 eluzelz 11573 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℤ)
30 eluzel2 11568 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘3) → 3 ∈ ℤ)
3129, 30zsubcld 11363 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (ℤ‘3) → (𝑁 − 3) ∈ ℤ)
32 peano2zm 11297 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
3329, 32syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (ℤ‘3) → (𝑁 − 1) ∈ ℤ)
34 eluz 11577 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 − 3) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 3)) ↔ (𝑁 − 3) ≤ (𝑁 − 1)))
3531, 33, 34syl2anc 691 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 3)) ↔ (𝑁 − 3) ≤ (𝑁 − 1)))
3628, 35mpbird 246 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (ℤ‘3) → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 3)))
3736adantl 481 . . . . . . . . . . . . . . . . . . 19 (((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3)) → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 3)))
3821, 37eqeltrd 2688 . . . . . . . . . . . . . . . . . 18 (((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3)) → ((#‘𝑤) − 1) ∈ (ℤ‘(𝑁 − 3)))
39 fzoss2 12365 . . . . . . . . . . . . . . . . . 18 (((#‘𝑤) − 1) ∈ (ℤ‘(𝑁 − 3)) → (0..^(𝑁 − 3)) ⊆ (0..^((#‘𝑤) − 1)))
40 ssralv 3629 . . . . . . . . . . . . . . . . . 18 ((0..^(𝑁 − 3)) ⊆ (0..^((#‘𝑤) − 1)) → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑁 − 3)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))
4138, 39, 403syl 18 . . . . . . . . . . . . . . . . 17 (((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3)) → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑁 − 3)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))
4241adantl 481 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑁 − 3)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))
43 simpll 786 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → 𝑤 ∈ Word 𝑉)
44 1eluzge0 11608 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ (ℤ‘0)
45 fzss1 12251 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ (ℤ‘0) → (1...𝑁) ⊆ (0...𝑁))
4644, 45mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘3) → (1...𝑁) ⊆ (0...𝑁))
47 ige3m2fz 12236 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ (1...𝑁))
4846, 47sseldd 3569 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ (0...𝑁))
4948adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3)) → (𝑁 − 2) ∈ (0...𝑁))
50 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((#‘𝑤) = 𝑁 → (0...(#‘𝑤)) = (0...𝑁))
5150eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . . . 24 ((#‘𝑤) = 𝑁 → ((𝑁 − 2) ∈ (0...(#‘𝑤)) ↔ (𝑁 − 2) ∈ (0...𝑁)))
5251adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3)) → ((𝑁 − 2) ∈ (0...(#‘𝑤)) ↔ (𝑁 − 2) ∈ (0...𝑁)))
5349, 52mpbird 246 . . . . . . . . . . . . . . . . . . . . . 22 (((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3)) → (𝑁 − 2) ∈ (0...(#‘𝑤)))
5453ad2antlr 759 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑁 − 2) ∈ (0...(#‘𝑤)))
55 2re 10967 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 ∈ ℝ
56 2lt3 11072 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 < 3
5755, 24, 56ltleii 10039 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ≤ 3
5855a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → 2 ∈ ℝ)
5958, 25, 26lesub2d 10514 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘3) → (2 ≤ 3 ↔ (𝑁 − 3) ≤ (𝑁 − 2)))
6057, 59mpbii 222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ (ℤ‘3) → (𝑁 − 3) ≤ (𝑁 − 2))
61 2z 11286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℤ
6261a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → 2 ∈ ℤ)
6329, 62zsubcld 11363 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ ℤ)
64 eluz 11577 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 − 3) ∈ ℤ ∧ (𝑁 − 2) ∈ ℤ) → ((𝑁 − 2) ∈ (ℤ‘(𝑁 − 3)) ↔ (𝑁 − 3) ≤ (𝑁 − 2)))
6531, 63, 64syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) ∈ (ℤ‘(𝑁 − 3)) ↔ (𝑁 − 3) ≤ (𝑁 − 2)))
6660, 65mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ (ℤ‘(𝑁 − 3)))
67 fzoss2 12365 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 − 2) ∈ (ℤ‘(𝑁 − 3)) → (0..^(𝑁 − 3)) ⊆ (0..^(𝑁 − 2)))
6866, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘3) → (0..^(𝑁 − 3)) ⊆ (0..^(𝑁 − 2)))
6968sseld 3567 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘3) → (𝑖 ∈ (0..^(𝑁 − 3)) → 𝑖 ∈ (0..^(𝑁 − 2))))
7069ad2antll 761 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) → (𝑖 ∈ (0..^(𝑁 − 3)) → 𝑖 ∈ (0..^(𝑁 − 2))))
7170imp 444 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → 𝑖 ∈ (0..^(𝑁 − 2)))
72 swrd0fv 13291 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (0...(#‘𝑤)) ∧ 𝑖 ∈ (0..^(𝑁 − 2))) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖) = (𝑤𝑖))
7343, 54, 71, 72syl3anc 1318 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖) = (𝑤𝑖))
7473eqcomd 2616 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑤𝑖) = ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖))
75 elfzonn0 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^(𝑁 − 3)) → 𝑖 ∈ ℕ0)
7675adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ (ℤ‘3) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → 𝑖 ∈ ℕ0)
77 peano2nn0 11210 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
7876, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ (ℤ‘3) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑖 + 1) ∈ ℕ0)
79 uz3m2nn 11607 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ ℕ)
8079adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ (ℤ‘3) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑁 − 2) ∈ ℕ)
81 elfzo0 12376 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^(𝑁 − 3)) ↔ (𝑖 ∈ ℕ0 ∧ (𝑁 − 3) ∈ ℕ ∧ 𝑖 < (𝑁 − 3)))
82 nn0cn 11179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑖 ∈ ℕ0𝑖 ∈ ℂ)
83 ax-1cn 9873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 1 ∈ ℂ
8482, 83jctir 559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑖 ∈ ℕ0 → (𝑖 ∈ ℂ ∧ 1 ∈ ℂ))
8584adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑖 ∈ ℕ0𝑁 ∈ (ℤ‘3)) → (𝑖 ∈ ℂ ∧ 1 ∈ ℂ))
86 pncan 10166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑖 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑖 + 1) − 1) = 𝑖)
8785, 86syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑖 ∈ ℕ0𝑁 ∈ (ℤ‘3)) → ((𝑖 + 1) − 1) = 𝑖)
8887eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑖 ∈ ℕ0𝑁 ∈ (ℤ‘3)) → 𝑖 = ((𝑖 + 1) − 1))
89 eluzelcn 11575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℂ)
9089adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑖 ∈ ℕ0𝑁 ∈ (ℤ‘3)) → 𝑁 ∈ ℂ)
91 2cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑖 ∈ ℕ0𝑁 ∈ (ℤ‘3)) → 2 ∈ ℂ)
92 1cnd 9935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑖 ∈ ℕ0𝑁 ∈ (ℤ‘3)) → 1 ∈ ℂ)
9390, 91, 92subsub4d 10302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑖 ∈ ℕ0𝑁 ∈ (ℤ‘3)) → ((𝑁 − 2) − 1) = (𝑁 − (2 + 1)))
94 df-3 10957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3 = (2 + 1)
9594oveq2i 6560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑁 − 3) = (𝑁 − (2 + 1))
9693, 95syl6reqr 2663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑖 ∈ ℕ0𝑁 ∈ (ℤ‘3)) → (𝑁 − 3) = ((𝑁 − 2) − 1))
9788, 96breq12d 4596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ ℕ0𝑁 ∈ (ℤ‘3)) → (𝑖 < (𝑁 − 3) ↔ ((𝑖 + 1) − 1) < ((𝑁 − 2) − 1)))
9897biimpd 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℕ0𝑁 ∈ (ℤ‘3)) → (𝑖 < (𝑁 − 3) → ((𝑖 + 1) − 1) < ((𝑁 − 2) − 1)))
9998impancom 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑖 ∈ ℕ0𝑖 < (𝑁 − 3)) → (𝑁 ∈ (ℤ‘3) → ((𝑖 + 1) − 1) < ((𝑁 − 2) − 1)))
100993adant2 1073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑖 ∈ ℕ0 ∧ (𝑁 − 3) ∈ ℕ ∧ 𝑖 < (𝑁 − 3)) → (𝑁 ∈ (ℤ‘3) → ((𝑖 + 1) − 1) < ((𝑁 − 2) − 1)))
101100imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑖 ∈ ℕ0 ∧ (𝑁 − 3) ∈ ℕ ∧ 𝑖 < (𝑁 − 3)) ∧ 𝑁 ∈ (ℤ‘3)) → ((𝑖 + 1) − 1) < ((𝑁 − 2) − 1))
102 nn0re 11178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ℕ0𝑖 ∈ ℝ)
103 peano2re 10088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ℝ → (𝑖 + 1) ∈ ℝ)
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℝ)
1051043ad2ant1 1075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑖 ∈ ℕ0 ∧ (𝑁 − 3) ∈ ℕ ∧ 𝑖 < (𝑁 − 3)) → (𝑖 + 1) ∈ ℝ)
106105adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑖 ∈ ℕ0 ∧ (𝑁 − 3) ∈ ℕ ∧ 𝑖 < (𝑁 − 3)) ∧ 𝑁 ∈ (ℤ‘3)) → (𝑖 + 1) ∈ ℝ)
10726, 58resubcld 10337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ ℝ)
108107adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑖 ∈ ℕ0 ∧ (𝑁 − 3) ∈ ℕ ∧ 𝑖 < (𝑁 − 3)) ∧ 𝑁 ∈ (ℤ‘3)) → (𝑁 − 2) ∈ ℝ)
109 1red 9934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑖 ∈ ℕ0 ∧ (𝑁 − 3) ∈ ℕ ∧ 𝑖 < (𝑁 − 3)) ∧ 𝑁 ∈ (ℤ‘3)) → 1 ∈ ℝ)
110106, 108, 109ltsub1d 10515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑖 ∈ ℕ0 ∧ (𝑁 − 3) ∈ ℕ ∧ 𝑖 < (𝑁 − 3)) ∧ 𝑁 ∈ (ℤ‘3)) → ((𝑖 + 1) < (𝑁 − 2) ↔ ((𝑖 + 1) − 1) < ((𝑁 − 2) − 1)))
111101, 110mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑖 ∈ ℕ0 ∧ (𝑁 − 3) ∈ ℕ ∧ 𝑖 < (𝑁 − 3)) ∧ 𝑁 ∈ (ℤ‘3)) → (𝑖 + 1) < (𝑁 − 2))
112111ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑖 ∈ ℕ0 ∧ (𝑁 − 3) ∈ ℕ ∧ 𝑖 < (𝑁 − 3)) → (𝑁 ∈ (ℤ‘3) → (𝑖 + 1) < (𝑁 − 2)))
11381, 112sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^(𝑁 − 3)) → (𝑁 ∈ (ℤ‘3) → (𝑖 + 1) < (𝑁 − 2)))
114113impcom 445 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ (ℤ‘3) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑖 + 1) < (𝑁 − 2))
115 elfzo0 12376 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 + 1) ∈ (0..^(𝑁 − 2)) ↔ ((𝑖 + 1) ∈ ℕ0 ∧ (𝑁 − 2) ∈ ℕ ∧ (𝑖 + 1) < (𝑁 − 2)))
11678, 80, 114, 115syl3anbrc 1239 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ (ℤ‘3) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑖 + 1) ∈ (0..^(𝑁 − 2)))
117116ex 449 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘3) → (𝑖 ∈ (0..^(𝑁 − 3)) → (𝑖 + 1) ∈ (0..^(𝑁 − 2))))
118117ad2antll 761 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) → (𝑖 ∈ (0..^(𝑁 − 3)) → (𝑖 + 1) ∈ (0..^(𝑁 − 2))))
119118imp 444 . . . . . . . . . . . . . . . . . . . . 21 (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑖 + 1) ∈ (0..^(𝑁 − 2)))
120 swrd0fv 13291 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (0...(#‘𝑤)) ∧ (𝑖 + 1) ∈ (0..^(𝑁 − 2))) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1)) = (𝑤‘(𝑖 + 1)))
12143, 54, 119, 120syl3anc 1318 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1)) = (𝑤‘(𝑖 + 1)))
122121eqcomd 2616 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → (𝑤‘(𝑖 + 1)) = ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1)))
12374, 122preq12d 4220 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → {(𝑤𝑖), (𝑤‘(𝑖 + 1))} = {((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))})
124123eleq1d 2672 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) ∧ 𝑖 ∈ (0..^(𝑁 − 3))) → ({(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
125124ralbidva 2968 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) → (∀𝑖 ∈ (0..^(𝑁 − 3)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 − 3)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
12642, 125sylibd 228 . . . . . . . . . . . . . . 15 ((𝑤 ∈ Word 𝑉 ∧ ((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3))) → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(𝑁 − 3)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
127126impancom 455 . . . . . . . . . . . . . 14 ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) → (((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3)) → ∀𝑖 ∈ (0..^(𝑁 − 3)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
1281273adant3 1074 . . . . . . . . . . . . 13 ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) → (((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3)) → ∀𝑖 ∈ (0..^(𝑁 − 3)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
129128expdimp 452 . . . . . . . . . . . 12 (((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ (ℤ‘3) → ∀𝑖 ∈ (0..^(𝑁 − 3)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
130129impcom 445 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → ∀𝑖 ∈ (0..^(𝑁 − 3)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸)
131130adantr 480 . . . . . . . . . 10 (((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ∀𝑖 ∈ (0..^(𝑁 − 3)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸)
132 simprl1 1099 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → 𝑤 ∈ Word 𝑉)
133 simprr 792 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → (#‘𝑤) = 𝑁)
1342adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → 𝑁 ∈ (ℤ‘2))
135132, 133, 1343jca 1235 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘2)))
136135adantr 480 . . . . . . . . . . . . . . 15 (((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘2)))
137 extwwlkfablem2lem 26602 . . . . . . . . . . . . . . 15 ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘2)) → (#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) = (𝑁 − 2))
138136, 137syl 17 . . . . . . . . . . . . . 14 (((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) = (𝑁 − 2))
139138oveq1d 6564 . . . . . . . . . . . . 13 (((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1) = ((𝑁 − 2) − 1))
140139oveq2d 6565 . . . . . . . . . . . 12 (((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)) = (0..^((𝑁 − 2) − 1)))
141 2cnd 10970 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘3) → 2 ∈ ℂ)
142 1cnd 9935 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘3) → 1 ∈ ℂ)
14389, 141, 142subsub4d 10302 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) − 1) = (𝑁 − (2 + 1)))
144 2p1e3 11028 . . . . . . . . . . . . . . . . 17 (2 + 1) = 3
145144a1i 11 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘3) → (2 + 1) = 3)
146145oveq2d 6565 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘3) → (𝑁 − (2 + 1)) = (𝑁 − 3))
147143, 146eqtrd 2644 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) − 1) = (𝑁 − 3))
148147ad2antrr 758 . . . . . . . . . . . . 13 (((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑁 − 2) − 1) = (𝑁 − 3))
149148oveq2d 6565 . . . . . . . . . . . 12 (((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (0..^((𝑁 − 2) − 1)) = (0..^(𝑁 − 3)))
150140, 149eqtrd 2644 . . . . . . . . . . 11 (((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)) = (0..^(𝑁 − 3)))
151150raleqdv 3121 . . . . . . . . . 10 (((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 − 3)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸))
152131, 151mpbird 246 . . . . . . . . 9 (((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸)
15320oveq2d 6565 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝑤) = 𝑁 → (0..^((#‘𝑤) − 1)) = (0..^(𝑁 − 1)))
154153raleqdv 3121 . . . . . . . . . . . . . . . . . . 19 ((#‘𝑤) = 𝑁 → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸))
155 simplr 788 . . . . . . . . . . . . . . . . . . . . . . 23 (((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → 𝑤 ∈ Word 𝑉)
156 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝑤) = 𝑁 → (1...(#‘𝑤)) = (1...𝑁))
157156eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((#‘𝑤) = 𝑁 → ((𝑁 − 2) ∈ (1...(#‘𝑤)) ↔ (𝑁 − 2) ∈ (1...𝑁)))
15847, 157syl5ibr 235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((#‘𝑤) = 𝑁 → (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ (1...(#‘𝑤))))
159158ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ (1...(#‘𝑤))))
160159com12 32 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘3) → ((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → (𝑁 − 2) ∈ (1...(#‘𝑤))))
161160adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → (𝑁 − 2) ∈ (1...(#‘𝑤))))
162161impcom 445 . . . . . . . . . . . . . . . . . . . . . . 23 (((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑁 − 2) ∈ (1...(#‘𝑤)))
163 swrd0fvlsw 13295 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))) → ( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) = (𝑤‘((𝑁 − 2) − 1)))
164155, 162, 163syl2anc 691 . . . . . . . . . . . . . . . . . . . . . 22 (((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) = (𝑤‘((𝑁 − 2) − 1)))
16547adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3)) → (𝑁 − 2) ∈ (1...𝑁))
166156adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3)) → (1...(#‘𝑤)) = (1...𝑁))
167165, 166eleqtrrd 2691 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘3)) → (𝑁 − 2) ∈ (1...(#‘𝑤)))
168167ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((#‘𝑤) = 𝑁 → (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ (1...(#‘𝑤))))
169168ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ (1...(#‘𝑤))))
170169com12 32 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘3) → ((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → (𝑁 − 2) ∈ (1...(#‘𝑤))))
171170adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → (𝑁 − 2) ∈ (1...(#‘𝑤))))
172171impcom 445 . . . . . . . . . . . . . . . . . . . . . . 23 (((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑁 − 2) ∈ (1...(#‘𝑤)))
173 swrd0fv0 13292 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 ∈ Word 𝑉 ∧ (𝑁 − 2) ∈ (1...(#‘𝑤))) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0) = (𝑤‘0))
174155, 172, 173syl2anc 691 . . . . . . . . . . . . . . . . . . . . . 22 (((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0) = (𝑤‘0))
175164, 174preq12d 4220 . . . . . . . . . . . . . . . . . . . . 21 (((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} = {(𝑤‘((𝑁 − 2) − 1)), (𝑤‘0)})
176 cnm2m1cnm3 11162 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℂ → ((𝑁 − 2) − 1) = (𝑁 − 3))
17789, 176syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 2) − 1) = (𝑁 − 3))
178177fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘3) → (𝑤‘((𝑁 − 2) − 1)) = (𝑤‘(𝑁 − 3)))
179178ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . 23 (((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘((𝑁 − 2) − 1)) = (𝑤‘(𝑁 − 3)))
180 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑤‘0) = (𝑤‘(𝑁 − 2)) → (𝑤‘0) = (𝑤‘(𝑁 − 2)))
181180eqcoms 2618 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑤‘(𝑁 − 2)) = (𝑤‘0) → (𝑤‘0) = (𝑤‘(𝑁 − 2)))
182181ad2antll 761 . . . . . . . . . . . . . . . . . . . . . . 23 (((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤‘0) = (𝑤‘(𝑁 − 2)))
183179, 182preq12d 4220 . . . . . . . . . . . . . . . . . . . . . 22 (((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {(𝑤‘((𝑁 − 2) − 1)), (𝑤‘0)} = {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))})
184 eluzfz2b 12221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑁 ∈ (ℤ‘3) ↔ 𝑁 ∈ (3...𝑁))
185 fzval3 12404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑁 ∈ ℤ → (3...𝑁) = (3..^(𝑁 + 1)))
18629, 185syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 ∈ (ℤ‘3) → (3...𝑁) = (3..^(𝑁 + 1)))
187186eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 ∈ (ℤ‘3) → (𝑁 ∈ (3...𝑁) ↔ 𝑁 ∈ (3..^(𝑁 + 1))))
188 peano2z 11295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
189 zadd2cl 11366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑁 ∈ ℤ → (𝑁 + 2) ∈ ℤ)
190 1le2 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 1 ≤ 2
191 1red 9934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑁 ∈ ℤ → 1 ∈ ℝ)
19255a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑁 ∈ ℤ → 2 ∈ ℝ)
193 zre 11258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
194191, 192, 193leadd2d 10501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑁 ∈ ℤ → (1 ≤ 2 ↔ (𝑁 + 1) ≤ (𝑁 + 2)))
195190, 194mpbii 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑁 ∈ ℤ → (𝑁 + 1) ≤ (𝑁 + 2))
196188, 189, 1953jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑁 ∈ ℤ → ((𝑁 + 1) ∈ ℤ ∧ (𝑁 + 2) ∈ ℤ ∧ (𝑁 + 1) ≤ (𝑁 + 2)))
19729, 196syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑁 ∈ (ℤ‘3) → ((𝑁 + 1) ∈ ℤ ∧ (𝑁 + 2) ∈ ℤ ∧ (𝑁 + 1) ≤ (𝑁 + 2)))
198 eluz2 11569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑁 + 2) ∈ (ℤ‘(𝑁 + 1)) ↔ ((𝑁 + 1) ∈ ℤ ∧ (𝑁 + 2) ∈ ℤ ∧ (𝑁 + 1) ≤ (𝑁 + 2)))
199197, 198sylibr 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑁 ∈ (ℤ‘3) → (𝑁 + 2) ∈ (ℤ‘(𝑁 + 1)))
200 fzoss2 12365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑁 + 2) ∈ (ℤ‘(𝑁 + 1)) → (3..^(𝑁 + 1)) ⊆ (3..^(𝑁 + 2)))
201199, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 ∈ (ℤ‘3) → (3..^(𝑁 + 1)) ⊆ (3..^(𝑁 + 2)))
202201sseld 3567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 ∈ (ℤ‘3) → (𝑁 ∈ (3..^(𝑁 + 1)) → 𝑁 ∈ (3..^(𝑁 + 2))))
203187, 202sylbid 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑁 ∈ (ℤ‘3) → (𝑁 ∈ (3...𝑁) → 𝑁 ∈ (3..^(𝑁 + 2))))
204184, 203syl5bi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑁 ∈ (ℤ‘3) → (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ (3..^(𝑁 + 2))))
205204pm2.43i 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ (3..^(𝑁 + 2)))
206 3cn 10972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3 ∈ ℂ
207206a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 ∈ (ℤ‘3) → 3 ∈ ℂ)
208207, 89, 142addsub12d 10294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑁 ∈ (ℤ‘3) → (3 + (𝑁 − 1)) = (𝑁 + (3 − 1)))
209 3m1e2 11014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (3 − 1) = 2
210209oveq2i 6560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑁 + (3 − 1)) = (𝑁 + 2)
211208, 210syl6eq 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑁 ∈ (ℤ‘3) → (3 + (𝑁 − 1)) = (𝑁 + 2))
212211oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ (ℤ‘3) → (3..^(3 + (𝑁 − 1))) = (3..^(𝑁 + 2)))
213205, 212eleqtrrd 2691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ (3..^(3 + (𝑁 − 1))))
214213, 33jca 553 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → (𝑁 ∈ (3..^(3 + (𝑁 − 1))) ∧ (𝑁 − 1) ∈ ℤ))
215 fzosubel3 12396 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 ∈ (3..^(3 + (𝑁 − 1))) ∧ (𝑁 − 1) ∈ ℤ) → (𝑁 − 3) ∈ (0..^(𝑁 − 1)))
216 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 = (𝑁 − 3) → (𝑤𝑖) = (𝑤‘(𝑁 − 3)))
217 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 = (𝑁 − 3) → (𝑖 + 1) = ((𝑁 − 3) + 1))
218217fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 = (𝑁 − 3) → (𝑤‘(𝑖 + 1)) = (𝑤‘((𝑁 − 3) + 1)))
219216, 218preq12d 4220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 = (𝑁 − 3) → {(𝑤𝑖), (𝑤‘(𝑖 + 1))} = {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))})
220219eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = (𝑁 − 3) → ({(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ ran 𝐸))
221220rspcv 3278 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 − 3) ∈ (0..^(𝑁 − 1)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ ran 𝐸))
222214, 215, 2213syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘3) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ ran 𝐸))
22389, 207, 142subsubd 10299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑁 ∈ (ℤ‘3) → (𝑁 − (3 − 1)) = ((𝑁 − 3) + 1))
224209a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑁 ∈ (ℤ‘3) → (3 − 1) = 2)
225224oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑁 ∈ (ℤ‘3) → (𝑁 − (3 − 1)) = (𝑁 − 2))
226223, 225eqtr3d 2646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ (ℤ‘3) → ((𝑁 − 3) + 1) = (𝑁 − 2))
227226fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ (ℤ‘3) → (𝑤‘((𝑁 − 3) + 1)) = (𝑤‘(𝑁 − 2)))
228227preq2d 4219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ (ℤ‘3) → {(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} = {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))})
229228eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘3) → ({(𝑤‘(𝑁 − 3)), (𝑤‘((𝑁 − 3) + 1))} ∈ ran 𝐸 ↔ {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))} ∈ ran 𝐸))
230222, 229sylibd 228 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ (ℤ‘3) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))} ∈ ran 𝐸))
231230adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))} ∈ ran 𝐸))
232231com12 32 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → ((𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))} ∈ ran 𝐸))
233232ad2antlr 759 . . . . . . . . . . . . . . . . . . . . . . 23 ((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) → ((𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))} ∈ ran 𝐸))
234233imp 444 . . . . . . . . . . . . . . . . . . . . . 22 (((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {(𝑤‘(𝑁 − 3)), (𝑤‘(𝑁 − 2))} ∈ ran 𝐸)
235183, 234eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . 21 (((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {(𝑤‘((𝑁 − 2) − 1)), (𝑤‘0)} ∈ ran 𝐸)
236175, 235eqeltrd 2688 . . . . . . . . . . . . . . . . . . . 20 (((((#‘𝑤) = 𝑁 ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) ∧ 𝑤 ∈ Word 𝑉) ∧ (𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸)
237236exp41 636 . . . . . . . . . . . . . . . . . . 19 ((#‘𝑤) = 𝑁 → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → (𝑤 ∈ Word 𝑉 → ((𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸))))
238154, 237sylbid 229 . . . . . . . . . . . . . . . . . 18 ((#‘𝑤) = 𝑁 → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → (𝑤 ∈ Word 𝑉 → ((𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸))))
239238com13 86 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ Word 𝑉 → (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 → ((#‘𝑤) = 𝑁 → ((𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸))))
240239imp 444 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) → ((#‘𝑤) = 𝑁 → ((𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸)))
2412403adant3 1074 . . . . . . . . . . . . . . 15 ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) → ((#‘𝑤) = 𝑁 → ((𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸)))
242241imp 444 . . . . . . . . . . . . . 14 (((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁) → ((𝑁 ∈ (ℤ‘3) ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸))
243242expd 451 . . . . . . . . . . . . 13 (((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ (ℤ‘3) → ((𝑤‘(𝑁 − 2)) = (𝑤‘0) → {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸)))
244243impcom 445 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → ((𝑤‘(𝑁 − 2)) = (𝑤‘0) → {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸))
245244com12 32 . . . . . . . . . . 11 ((𝑤‘(𝑁 − 2)) = (𝑤‘0) → ((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸))
246245adantl 481 . . . . . . . . . 10 (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) → {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸))
247246impcom 445 . . . . . . . . 9 (((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸)
24819, 152, 2473jca 1235 . . . . . . . 8 (((𝑁 ∈ (ℤ‘3) ∧ ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸))
249248exp31 628 . . . . . . 7 (𝑁 ∈ (ℤ‘3) → (((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸))))
2502493ad2ant3 1077 . . . . . 6 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸) ∧ (#‘𝑤) = 𝑁) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸))))
25115, 250sylbid 229 . . . . 5 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸))))
252251imp31 447 . . . 4 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸))
253 clwwlknprop 26300 . . . . . . . . . 10 (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧ (#‘𝑤) = 𝑁)))
254 simpl2 1058 . . . . . . . . . . . 12 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧ (#‘𝑤) = 𝑁)) ∧ 𝑁 ∈ (ℤ‘3)) → 𝑤 ∈ Word 𝑉)
255 simpl3r 1110 . . . . . . . . . . . 12 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧ (#‘𝑤) = 𝑁)) ∧ 𝑁 ∈ (ℤ‘3)) → (#‘𝑤) = 𝑁)
2562adantl 481 . . . . . . . . . . . 12 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧ (#‘𝑤) = 𝑁)) ∧ 𝑁 ∈ (ℤ‘3)) → 𝑁 ∈ (ℤ‘2))
257254, 255, 2563jca 1235 . . . . . . . . . . 11 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧ (#‘𝑤) = 𝑁)) ∧ 𝑁 ∈ (ℤ‘3)) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘2)))
258257ex 449 . . . . . . . . . 10 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧ (#‘𝑤) = 𝑁)) → (𝑁 ∈ (ℤ‘3) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘2))))
259253, 258syl 17 . . . . . . . . 9 (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑁 ∈ (ℤ‘3) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘2))))
260259com12 32 . . . . . . . 8 (𝑁 ∈ (ℤ‘3) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘2))))
2612603ad2ant3 1077 . . . . . . 7 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘2))))
262261imp 444 . . . . . 6 (((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘2)))
263262adantr 480 . . . . 5 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 𝑁𝑁 ∈ (ℤ‘2)))
264263, 137syl 17 . . . 4 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) = (𝑁 − 2))
265252, 264jca 553 . . 3 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) = (𝑁 − 2)))
266 uznn0sub 11595 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘2) → (𝑁 − 2) ∈ ℕ0)
2672, 266syl 17 . . . . . . . . 9 (𝑁 ∈ (ℤ‘3) → (𝑁 − 2) ∈ ℕ0)
2681, 267anim12i 588 . . . . . . . 8 ((𝑉 USGrph 𝐸𝑁 ∈ (ℤ‘3)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 − 2) ∈ ℕ0))
269 df-3an 1033 . . . . . . . 8 ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑁 − 2) ∈ ℕ0) ↔ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 − 2) ∈ ℕ0))
270268, 269sylibr 223 . . . . . . 7 ((𝑉 USGrph 𝐸𝑁 ∈ (ℤ‘3)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑁 − 2) ∈ ℕ0))
271 isclwwlkn 26297 . . . . . . 7 ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑁 − 2) ∈ ℕ0) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2)) ↔ ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) = (𝑁 − 2))))
272270, 271syl 17 . . . . . 6 ((𝑉 USGrph 𝐸𝑁 ∈ (ℤ‘3)) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2)) ↔ ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) = (𝑁 − 2))))
273 isclwwlk 26296 . . . . . . . . 9 ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸)))
2741, 273syl 17 . . . . . . . 8 (𝑉 USGrph 𝐸 → ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸)))
275274adantr 480 . . . . . . 7 ((𝑉 USGrph 𝐸𝑁 ∈ (ℤ‘3)) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸)))
276275anbi1d 737 . . . . . 6 ((𝑉 USGrph 𝐸𝑁 ∈ (ℤ‘3)) → (((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) = (𝑁 − 2)) ↔ (((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) = (𝑁 − 2))))
277272, 276bitrd 267 . . . . 5 ((𝑉 USGrph 𝐸𝑁 ∈ (ℤ‘3)) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2)) ↔ (((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) = (𝑁 − 2))))
2782773adant2 1073 . . . 4 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2)) ↔ (((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) = (𝑁 − 2))))
279278ad2antrr 758 . . 3 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → ((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2)) ↔ (((𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) − 1)){((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘𝑖), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)), ((𝑤 substr ⟨0, (𝑁 − 2)⟩)‘0)} ∈ ran 𝐸) ∧ (#‘(𝑤 substr ⟨0, (𝑁 − 2)⟩)) = (𝑁 − 2))))
280265, 279mpbird 246 . 2 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2)))
2812673ad2ant3 1077 . . . 4 ((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) → (𝑁 − 2) ∈ ℕ0)
282281ad2antrr 758 . . 3 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑁 − 2) ∈ ℕ0)
283 numclwwlk.c . . . 4 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))
284283numclwwlkfvc 26604 . . 3 ((𝑁 − 2) ∈ ℕ0 → (𝐶‘(𝑁 − 2)) = ((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2)))
285282, 284syl 17 . 2 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝐶‘(𝑁 − 2)) = ((𝑉 ClWWalksN 𝐸)‘(𝑁 − 2)))
286280, 285eleqtrrd 2691 1 ((((𝑉 USGrph 𝐸𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) → (𝑤 substr ⟨0, (𝑁 − 2)⟩) ∈ (𝐶‘(𝑁 − 2)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173   ⊆ wss 3540  {cpr 4127  ⟨cop 4131   class class class wbr 4583   ↦ cmpt 4643  ran crn 5039  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  2c2 10947  3c3 10948  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  ...cfz 12197  ..^cfzo 12334  #chash 12979  Word cword 13146   lastS clsw 13147   substr csubstr 13150   USGrph cusg 25859   ClWWalks cclwwlk 26276   ClWWalksN cclwwlkn 26277 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-hash 12980  df-word 13154  df-lsw 13155  df-substr 13158  df-usgra 25862  df-clwwlk 26279  df-clwwlkn 26280 This theorem is referenced by:  extwwlkfab  26617
 Copyright terms: Public domain W3C validator