Metamath Proof Explorer

Theorem clwlknf1oclwwlknlem1

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

Ref Expression
Assertion clwlknf1oclwwlknlem1 ⊢C∈ClWalks⁡G∧1≤1st⁡C→2nd⁡Cprefix2nd⁡C−1=1st⁡C

Proof

Step Hyp Ref Expression
1 clwlkwlk ⊢C∈ClWalks⁡G→C∈Walks⁡G
2 wlkcpr ⊢C∈Walks⁡G↔1st⁡CWalks⁡G2nd⁡C
3 eqid ⊢Vtx⁡G=Vtx⁡G
4 3 wlkpwrd ⊢1st⁡CWalks⁡G2nd⁡C→2nd⁡C∈WordVtx⁡G
5 lencl ⊢2nd⁡C∈WordVtx⁡G→2nd⁡C∈ℕ0
6 4 5 syl ⊢1st⁡CWalks⁡G2nd⁡C→2nd⁡C∈ℕ0
7 wlklenvm1 ⊢1st⁡CWalks⁡G2nd⁡C→1st⁡C=2nd⁡C−1
8 7 breq2d ⊢1st⁡CWalks⁡G2nd⁡C→1≤1st⁡C↔1≤2nd⁡C−1
9 1red ⊢2nd⁡C∈ℕ0→1∈ℝ
10 nn0re ⊢2nd⁡C∈ℕ0→2nd⁡C∈ℝ
11 9 9 10 leaddsub2d ⊢2nd⁡C∈ℕ0→1+1≤2nd⁡C↔1≤2nd⁡C−1
12 1p1e2 ⊢1+1=2
13 12 breq1i ⊢1+1≤2nd⁡C↔2≤2nd⁡C
14 13 biimpi ⊢1+1≤2nd⁡C→2≤2nd⁡C
15 11 14 syl6bir ⊢2nd⁡C∈ℕ0→1≤2nd⁡C−1→2≤2nd⁡C
16 4 5 15 3syl ⊢1st⁡CWalks⁡G2nd⁡C→1≤2nd⁡C−1→2≤2nd⁡C
17 8 16 sylbid ⊢1st⁡CWalks⁡G2nd⁡C→1≤1st⁡C→2≤2nd⁡C
18 17 imp ⊢1st⁡CWalks⁡G2nd⁡C∧1≤1st⁡C→2≤2nd⁡C
19 ige2m1fz ⊢2nd⁡C∈ℕ0∧2≤2nd⁡C→2nd⁡C−1∈0…2nd⁡C
20 6 18 19 syl2an2r ⊢1st⁡CWalks⁡G2nd⁡C∧1≤1st⁡C→2nd⁡C−1∈0…2nd⁡C
21 pfxlen ⊢2nd⁡C∈WordVtx⁡G∧2nd⁡C−1∈0…2nd⁡C→2nd⁡Cprefix2nd⁡C−1=2nd⁡C−1
22 4 20 21 syl2an2r ⊢1st⁡CWalks⁡G2nd⁡C∧1≤1st⁡C→2nd⁡Cprefix2nd⁡C−1=2nd⁡C−1
23 7 eqcomd ⊢1st⁡CWalks⁡G2nd⁡C→2nd⁡C−1=1st⁡C
24 23 adantr ⊢1st⁡CWalks⁡G2nd⁡C∧1≤1st⁡C→2nd⁡C−1=1st⁡C
25 22 24 eqtrd ⊢1st⁡CWalks⁡G2nd⁡C∧1≤1st⁡C→2nd⁡Cprefix2nd⁡C−1=1st⁡C
26 25 ex ⊢1st⁡CWalks⁡G2nd⁡C→1≤1st⁡C→2nd⁡Cprefix2nd⁡C−1=1st⁡C
27 2 26 sylbi ⊢C∈Walks⁡G→1≤1st⁡C→2nd⁡Cprefix2nd⁡C−1=1st⁡C
28 1 27 syl ⊢C∈ClWalks⁡G→1≤1st⁡C→2nd⁡Cprefix2nd⁡C−1=1st⁡C
29 28 imp ⊢C∈ClWalks⁡G∧1≤1st⁡C→2nd⁡Cprefix2nd⁡C−1=1st⁡C