pthdadjvtx

Description: The adjacent vertices of a path of length at least 2 are distinct. (Contributed by AV, 5-Feb-2021)

		Ref	Expression
	Assertion	pthdadjvtx	$⊢ (F Paths (G) P \land 1 < \|F\| \land I \in (0 ..^\|F\|)) \to P (I) \neq P (I + 1)$

Proof

Step	Hyp	Ref	Expression
1		elfzo0l	$⊢ I \in (0 ..^\|F\|) \to (I = 0 \lor I \in (1 ..^\|F\|))$
2		simpr	$⊢ (1 < \|F\| \land F Paths (G) P) \to F Paths (G) P$
3		pthiswlk	$⊢ F Paths (G) P \to F Walks (G) P$
4		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
5		1zzd	$⊢ (\|F\| \in ℕ_{0} \land 1 < \|F\|) \to 1 \in ℤ$
6		nn0z	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℤ$
7	6	adantr	$⊢ (\|F\| \in ℕ_{0} \land 1 < \|F\|) \to \|F\| \in ℤ$
8		simpr	$⊢ (\|F\| \in ℕ_{0} \land 1 < \|F\|) \to 1 < \|F\|$
9		fzolb	$⊢ 1 \in (1 ..^\|F\|) \leftrightarrow (1 \in ℤ \land \|F\| \in ℤ \land 1 < \|F\|)$
10	5 7 8 9	syl3anbrc	$⊢ (\|F\| \in ℕ_{0} \land 1 < \|F\|) \to 1 \in (1 ..^\|F\|)$
11		0elfz	$⊢ \|F\| \in ℕ_{0} \to 0 \in (0 \dots \|F\|)$
12	11	adantr	$⊢ (\|F\| \in ℕ_{0} \land 1 < \|F\|) \to 0 \in (0 \dots \|F\|)$
13		ax-1ne0	$⊢ 1 \neq 0$
14	13	a1i	$⊢ (\|F\| \in ℕ_{0} \land 1 < \|F\|) \to 1 \neq 0$
15	10 12 14	3jca	$⊢ (\|F\| \in ℕ_{0} \land 1 < \|F\|) \to (1 \in (1 ..^\|F\|) \land 0 \in (0 \dots \|F\|) \land 1 \neq 0)$
16	15	ex	$⊢ \|F\| \in ℕ_{0} \to (1 < \|F\| \to (1 \in (1 ..^\|F\|) \land 0 \in (0 \dots \|F\|) \land 1 \neq 0))$
17	3 4 16	3syl	$⊢ F Paths (G) P \to (1 < \|F\| \to (1 \in (1 ..^\|F\|) \land 0 \in (0 \dots \|F\|) \land 1 \neq 0))$
18	17	impcom	$⊢ (1 < \|F\| \land F Paths (G) P) \to (1 \in (1 ..^\|F\|) \land 0 \in (0 \dots \|F\|) \land 1 \neq 0)$
19		pthdivtx	$⊢ (F Paths (G) P \land (1 \in (1 ..^\|F\|) \land 0 \in (0 \dots \|F\|) \land 1 \neq 0)) \to P (1) \neq P (0)$
20	2 18 19	syl2anc	$⊢ (1 < \|F\| \land F Paths (G) P) \to P (1) \neq P (0)$
21	20	necomd	$⊢ (1 < \|F\| \land F Paths (G) P) \to P (0) \neq P (1)$
22	21	3adant1	$⊢ (I = 0 \land 1 < \|F\| \land F Paths (G) P) \to P (0) \neq P (1)$
23		fveq2	$⊢ I = 0 \to P (I) = P (0)$
24		fv0p1e1	$⊢ I = 0 \to P (I + 1) = P (1)$
25	23 24	neeq12d	$⊢ I = 0 \to (P (I) \neq P (I + 1) \leftrightarrow P (0) \neq P (1))$
26	25	3ad2ant1	$⊢ (I = 0 \land 1 < \|F\| \land F Paths (G) P) \to (P (I) \neq P (I + 1) \leftrightarrow P (0) \neq P (1))$
27	22 26	mpbird	$⊢ (I = 0 \land 1 < \|F\| \land F Paths (G) P) \to P (I) \neq P (I + 1)$
28	27	3exp	$⊢ I = 0 \to (1 < \|F\| \to (F Paths (G) P \to P (I) \neq P (I + 1)))$
29		simp3	$⊢ (I \in (1 ..^\|F\|) \land 1 < \|F\| \land F Paths (G) P) \to F Paths (G) P$
30		id	$⊢ I \in (1 ..^\|F\|) \to I \in (1 ..^\|F\|)$
31		fzo0ss1	$⊢ (1 ..^\|F\|) \subseteq (0 ..^\|F\|)$
32	31	sseli	$⊢ I \in (1 ..^\|F\|) \to I \in (0 ..^\|F\|)$
33		fzofzp1	$⊢ I \in (0 ..^\|F\|) \to I + 1 \in (0 \dots \|F\|)$
34	32 33	syl	$⊢ I \in (1 ..^\|F\|) \to I + 1 \in (0 \dots \|F\|)$
35		elfzoelz	$⊢ I \in (1 ..^\|F\|) \to I \in ℤ$
36	35	zcnd	$⊢ I \in (1 ..^\|F\|) \to I \in ℂ$
37		1cnd	$⊢ I \in (1 ..^\|F\|) \to 1 \in ℂ$
38	13	a1i	$⊢ I \in (1 ..^\|F\|) \to 1 \neq 0$
39	36 37 38	3jca	$⊢ I \in (1 ..^\|F\|) \to (I \in ℂ \land 1 \in ℂ \land 1 \neq 0)$
40		addn0nid	$⊢ (I \in ℂ \land 1 \in ℂ \land 1 \neq 0) \to I + 1 \neq I$
41	40	necomd	$⊢ (I \in ℂ \land 1 \in ℂ \land 1 \neq 0) \to I \neq I + 1$
42	39 41	syl	$⊢ I \in (1 ..^\|F\|) \to I \neq I + 1$
43	30 34 42	3jca	$⊢ I \in (1 ..^\|F\|) \to (I \in (1 ..^\|F\|) \land I + 1 \in (0 \dots \|F\|) \land I \neq I + 1)$
44	43	3ad2ant1	$⊢ (I \in (1 ..^\|F\|) \land 1 < \|F\| \land F Paths (G) P) \to (I \in (1 ..^\|F\|) \land I + 1 \in (0 \dots \|F\|) \land I \neq I + 1)$
45		pthdivtx	$⊢ (F Paths (G) P \land (I \in (1 ..^\|F\|) \land I + 1 \in (0 \dots \|F\|) \land I \neq I + 1)) \to P (I) \neq P (I + 1)$
46	29 44 45	syl2anc	$⊢ (I \in (1 ..^\|F\|) \land 1 < \|F\| \land F Paths (G) P) \to P (I) \neq P (I + 1)$
47	46	3exp	$⊢ I \in (1 ..^\|F\|) \to (1 < \|F\| \to (F Paths (G) P \to P (I) \neq P (I + 1)))$
48	28 47	jaoi	$⊢ (I = 0 \lor I \in (1 ..^\|F\|)) \to (1 < \|F\| \to (F Paths (G) P \to P (I) \neq P (I + 1)))$
49	1 48	syl	$⊢ I \in (0 ..^\|F\|) \to (1 < \|F\| \to (F Paths (G) P \to P (I) \neq P (I + 1)))$
50	49	3imp31	$⊢ (F Paths (G) P \land 1 < \|F\| \land I \in (0 ..^\|F\|)) \to P (I) \neq P (I + 1)$

Metamath Proof Explorer

Theorem pthdadjvtx

Proof