# Metamath Proof Explorer

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

Ref Expression
Assertion pthdadjvtx ${⊢}\left({F}\mathrm{Paths}\left({G}\right){P}\wedge 1<\left|{F}\right|\wedge {I}\in \left(0..^\left|{F}\right|\right)\right)\to {P}\left({I}\right)\ne {P}\left({I}+1\right)$

### Proof

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