clwlknf1oclwwlknlem1

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

		Ref	Expression
	Assertion	clwlknf1oclwwlknlem1	$⊢ (C \in ClWalks (G) \land 1 \leq \|1^{st} (C)\|) \to \|2^{nd} (C) prefix (\|2^{nd} (C)\| - 1)\| = \|1^{st} (C)\|$

Proof

Step	Hyp	Ref	Expression
1		clwlkwlk	$⊢ C \in ClWalks (G) \to C \in Walks (G)$
2		wlkcpr	$⊢ C \in Walks (G) \leftrightarrow 1^{st} (C) Walks (G) 2^{nd} (C)$
3		eqid	$⊢ Vtx (G) = Vtx (G)$
4	3	wlkpwrd	$⊢ 1^{st} (C) Walks (G) 2^{nd} (C) \to 2^{nd} (C) \in Word Vtx (G)$
5		lencl	$⊢ 2^{nd} (C) \in Word Vtx (G) \to \|2^{nd} (C)\| \in ℕ_{0}$
6	4 5	syl	$⊢ 1^{st} (C) Walks (G) 2^{nd} (C) \to \|2^{nd} (C)\| \in ℕ_{0}$
7		wlklenvm1	$⊢ 1^{st} (C) Walks (G) 2^{nd} (C) \to \|1^{st} (C)\| = \|2^{nd} (C)\| - 1$
8	7	breq2d	$⊢ 1^{st} (C) Walks (G) 2^{nd} (C) \to (1 \leq \|1^{st} (C)\| \leftrightarrow 1 \leq \|2^{nd} (C)\| - 1)$
9		1red	$⊢ \|2^{nd} (C)\| \in ℕ_{0} \to 1 \in ℝ$
10		nn0re	$⊢ \|2^{nd} (C)\| \in ℕ_{0} \to \|2^{nd} (C)\| \in ℝ$
11	9 9 10	leaddsub2d	$⊢ \|2^{nd} (C)\| \in ℕ_{0} \to (1 + 1 \leq \|2^{nd} (C)\| \leftrightarrow 1 \leq \|2^{nd} (C)\| - 1)$
12		1p1e2	$⊢ 1 + 1 = 2$
13	12	breq1i	$⊢ 1 + 1 \leq \|2^{nd} (C)\| \leftrightarrow 2 \leq \|2^{nd} (C)\|$
14	13	biimpi	$⊢ 1 + 1 \leq \|2^{nd} (C)\| \to 2 \leq \|2^{nd} (C)\|$
15	11 14	syl6bir	$⊢ \|2^{nd} (C)\| \in ℕ_{0} \to (1 \leq \|2^{nd} (C)\| - 1 \to 2 \leq \|2^{nd} (C)\|)$
16	4 5 15	3syl	$⊢ 1^{st} (C) Walks (G) 2^{nd} (C) \to (1 \leq \|2^{nd} (C)\| - 1 \to 2 \leq \|2^{nd} (C)\|)$
17	8 16	sylbid	$⊢ 1^{st} (C) Walks (G) 2^{nd} (C) \to (1 \leq \|1^{st} (C)\| \to 2 \leq \|2^{nd} (C)\|)$
18	17	imp	$⊢ (1^{st} (C) Walks (G) 2^{nd} (C) \land 1 \leq \|1^{st} (C)\|) \to 2 \leq \|2^{nd} (C)\|$
19		ige2m1fz	$⊢ (\|2^{nd} (C)\| \in ℕ_{0} \land 2 \leq \|2^{nd} (C)\|) \to \|2^{nd} (C)\| - 1 \in (0 \dots \|2^{nd} (C)\|)$
20	6 18 19	syl2an2r	$⊢ (1^{st} (C) Walks (G) 2^{nd} (C) \land 1 \leq \|1^{st} (C)\|) \to \|2^{nd} (C)\| - 1 \in (0 \dots \|2^{nd} (C)\|)$
21		pfxlen	$⊢ (2^{nd} (C) \in Word Vtx (G) \land \|2^{nd} (C)\| - 1 \in (0 \dots \|2^{nd} (C)\|)) \to \|2^{nd} (C) prefix (\|2^{nd} (C)\| - 1)\| = \|2^{nd} (C)\| - 1$
22	4 20 21	syl2an2r	$⊢ (1^{st} (C) Walks (G) 2^{nd} (C) \land 1 \leq \|1^{st} (C)\|) \to \|2^{nd} (C) prefix (\|2^{nd} (C)\| - 1)\| = \|2^{nd} (C)\| - 1$
23	7	eqcomd	$⊢ 1^{st} (C) Walks (G) 2^{nd} (C) \to \|2^{nd} (C)\| - 1 = \|1^{st} (C)\|$
24	23	adantr	$⊢ (1^{st} (C) Walks (G) 2^{nd} (C) \land 1 \leq \|1^{st} (C)\|) \to \|2^{nd} (C)\| - 1 = \|1^{st} (C)\|$
25	22 24	eqtrd	$⊢ (1^{st} (C) Walks (G) 2^{nd} (C) \land 1 \leq \|1^{st} (C)\|) \to \|2^{nd} (C) prefix (\|2^{nd} (C)\| - 1)\| = \|1^{st} (C)\|$
26	25	ex	$⊢ 1^{st} (C) Walks (G) 2^{nd} (C) \to (1 \leq \|1^{st} (C)\| \to \|2^{nd} (C) prefix (\|2^{nd} (C)\| - 1)\| = \|1^{st} (C)\|)$
27	2 26	sylbi	$⊢ C \in Walks (G) \to (1 \leq \|1^{st} (C)\| \to \|2^{nd} (C) prefix (\|2^{nd} (C)\| - 1)\| = \|1^{st} (C)\|)$
28	1 27	syl	$⊢ C \in ClWalks (G) \to (1 \leq \|1^{st} (C)\| \to \|2^{nd} (C) prefix (\|2^{nd} (C)\| - 1)\| = \|1^{st} (C)\|)$
29	28	imp	$⊢ (C \in ClWalks (G) \land 1 \leq \|1^{st} (C)\|) \to \|2^{nd} (C) prefix (\|2^{nd} (C)\| - 1)\| = \|1^{st} (C)\|$

Metamath Proof Explorer

Theorem clwlknf1oclwwlknlem1

Proof