Metamath Proof Explorer

Theorem dlwwlknondlwlknonf1olem1

Description: Lemma 1 for dlwwlknondlwlknonf1o . (Contributed by AV, 29-May-2022) (Revised by AV, 1-Nov-2022)

Ref Expression
Assertion dlwwlknondlwlknonf1olem1 ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → 2 nd ⁡ c prefix 1 st ⁡ c ⁡ N − 2 = 2 nd ⁡ c ⁡ N − 2

Proof

Step Hyp Ref Expression
1 clwlkwlk ⊢ c ∈ ClWalks ⁡ G → c ∈ Walks ⁡ G
2 wlkcpr ⊢ c ∈ Walks ⁡ G ↔ 1 st ⁡ c Walks ⁡ G 2 nd ⁡ c
3 1 2 sylib ⊢ c ∈ ClWalks ⁡ G → 1 st ⁡ c Walks ⁡ G 2 nd ⁡ c
4 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
5 4 wlkpwrd ⊢ 1 st ⁡ c Walks ⁡ G 2 nd ⁡ c → 2 nd ⁡ c ∈ Word Vtx ⁡ G
6 3 5 syl ⊢ c ∈ ClWalks ⁡ G → 2 nd ⁡ c ∈ Word Vtx ⁡ G
7 6 3ad2ant2 ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → 2 nd ⁡ c ∈ Word Vtx ⁡ G
8 eluzge2nn0 ⊢ N ∈ ℤ ≥ 2 → N ∈ ℕ 0
9 8 3ad2ant3 ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → N ∈ ℕ 0
10 eleq1 ⊢ 1 st ⁡ c = N → 1 st ⁡ c ∈ ℕ 0 ↔ N ∈ ℕ 0
11 10 3ad2ant1 ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → 1 st ⁡ c ∈ ℕ 0 ↔ N ∈ ℕ 0
12 9 11 mpbird ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → 1 st ⁡ c ∈ ℕ 0
13 nn0fz0 ⊢ 1 st ⁡ c ∈ ℕ 0 ↔ 1 st ⁡ c ∈ 0 … 1 st ⁡ c
14 12 13 sylib ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → 1 st ⁡ c ∈ 0 … 1 st ⁡ c
15 fzelp1 ⊢ 1 st ⁡ c ∈ 0 … 1 st ⁡ c → 1 st ⁡ c ∈ 0 … 1 st ⁡ c + 1
16 14 15 syl ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → 1 st ⁡ c ∈ 0 … 1 st ⁡ c + 1
17 wlklenvp1 ⊢ 1 st ⁡ c Walks ⁡ G 2 nd ⁡ c → 2 nd ⁡ c = 1 st ⁡ c + 1
18 17 eqcomd ⊢ 1 st ⁡ c Walks ⁡ G 2 nd ⁡ c → 1 st ⁡ c + 1 = 2 nd ⁡ c
19 3 18 syl ⊢ c ∈ ClWalks ⁡ G → 1 st ⁡ c + 1 = 2 nd ⁡ c
20 19 oveq2d ⊢ c ∈ ClWalks ⁡ G → 0 … 1 st ⁡ c + 1 = 0 … 2 nd ⁡ c
21 20 eleq2d ⊢ c ∈ ClWalks ⁡ G → 1 st ⁡ c ∈ 0 … 1 st ⁡ c + 1 ↔ 1 st ⁡ c ∈ 0 … 2 nd ⁡ c
22 21 3ad2ant2 ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → 1 st ⁡ c ∈ 0 … 1 st ⁡ c + 1 ↔ 1 st ⁡ c ∈ 0 … 2 nd ⁡ c
23 16 22 mpbid ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → 1 st ⁡ c ∈ 0 … 2 nd ⁡ c
24 2nn ⊢ 2 ∈ ℕ
25 24 a1i ⊢ N ∈ ℤ ≥ 2 → 2 ∈ ℕ
26 eluz2nn ⊢ N ∈ ℤ ≥ 2 → N ∈ ℕ
27 eluzle ⊢ N ∈ ℤ ≥ 2 → 2 ≤ N
28 elfz1b ⊢ 2 ∈ 1 … N ↔ 2 ∈ ℕ ∧ N ∈ ℕ ∧ 2 ≤ N
29 25 26 27 28 syl3anbrc ⊢ N ∈ ℤ ≥ 2 → 2 ∈ 1 … N
30 ubmelfzo ⊢ 2 ∈ 1 … N → N − 2 ∈ 0 ..^ N
31 29 30 syl ⊢ N ∈ ℤ ≥ 2 → N − 2 ∈ 0 ..^ N
32 31 3ad2ant3 ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → N − 2 ∈ 0 ..^ N
33 oveq2 ⊢ 1 st ⁡ c = N → 0 ..^ 1 st ⁡ c = 0 ..^ N
34 33 eleq2d ⊢ 1 st ⁡ c = N → N − 2 ∈ 0 ..^ 1 st ⁡ c ↔ N − 2 ∈ 0 ..^ N
35 34 3ad2ant1 ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → N − 2 ∈ 0 ..^ 1 st ⁡ c ↔ N − 2 ∈ 0 ..^ N
36 32 35 mpbird ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → N − 2 ∈ 0 ..^ 1 st ⁡ c
37 pfxfv ⊢ 2 nd ⁡ c ∈ Word Vtx ⁡ G ∧ 1 st ⁡ c ∈ 0 … 2 nd ⁡ c ∧ N − 2 ∈ 0 ..^ 1 st ⁡ c → 2 nd ⁡ c prefix 1 st ⁡ c ⁡ N − 2 = 2 nd ⁡ c ⁡ N − 2
38 7 23 36 37 syl3anc ⊢ 1 st ⁡ c = N ∧ c ∈ ClWalks ⁡ G ∧ N ∈ ℤ ≥ 2 → 2 nd ⁡ c prefix 1 st ⁡ c ⁡ N − 2 = 2 nd ⁡ c ⁡ N − 2