Metamath Proof Explorer

Theorem clwwnrepclwwn

Description: If the initial vertex of a closed walk occurs another time in the walk, the walk starts with a closed walk. Notice that 3 <_ N is required, because for N = 2 , ( w prefix ( N - 2 ) ) = ( w prefix 0 ) = (/) , but (/) (and anything else) is not a representation of an empty closed walk as word, see clwwlkn0 . (Contributed by Alexander van der Vekens, 15-Sep-2018) (Revised by AV, 28-May-2021) (Revised by AV, 30-Oct-2022)

Ref Expression
Assertion clwwnrepclwwn ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ N ClWWalksN G ∧ W ⁡ N − 2 = W ⁡ 0 → W prefix N − 2 ∈ N − 2 ClWWalksN G

Proof

Step Hyp Ref Expression
1 uz3m2nn ⊢ N ∈ ℤ ≥ 3 → N − 2 ∈ ℕ
2 eluzelz ⊢ N ∈ ℤ ≥ 3 → N ∈ ℤ
3 2eluzge1 ⊢ 2 ∈ ℤ ≥ 1
4 subeluzsub ⊢ N ∈ ℤ ∧ 2 ∈ ℤ ≥ 1 → N − 1 ∈ ℤ ≥ N − 2
5 2 3 4 sylancl ⊢ N ∈ ℤ ≥ 3 → N − 1 ∈ ℤ ≥ N − 2
6 1 5 jca ⊢ N ∈ ℤ ≥ 3 → N − 2 ∈ ℕ ∧ N − 1 ∈ ℤ ≥ N − 2
7 6 3ad2ant1 ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ N ClWWalksN G ∧ W ⁡ N − 2 = W ⁡ 0 → N − 2 ∈ ℕ ∧ N − 1 ∈ ℤ ≥ N − 2
8 clwwlknwwlksn ⊢ W ∈ N ClWWalksN G → W ∈ N − 1 WWalksN G
9 8 3ad2ant2 ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ N ClWWalksN G ∧ W ⁡ N − 2 = W ⁡ 0 → W ∈ N − 1 WWalksN G
10 simp3 ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ N ClWWalksN G ∧ W ⁡ N − 2 = W ⁡ 0 → W ⁡ N − 2 = W ⁡ 0
11 clwwlkinwwlk ⊢ N − 2 ∈ ℕ ∧ N − 1 ∈ ℤ ≥ N − 2 ∧ W ∈ N − 1 WWalksN G ∧ W ⁡ N − 2 = W ⁡ 0 → W prefix N − 2 ∈ N − 2 ClWWalksN G
12 7 9 10 11 syl3anc ⊢ N ∈ ℤ ≥ 3 ∧ W ∈ N ClWWalksN G ∧ W ⁡ N − 2 = W ⁡ 0 → W prefix N − 2 ∈ N − 2 ClWWalksN G