Metamath Proof Explorer

Theorem 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 ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ ( 𝐼 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 elfzo0l ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
2 simpr ⊢ ( ( 1 < ( ♯ ‘ 𝐹 ) ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
3 pthiswlk ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
4 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
5 1zzd ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝐹 ) ) → 1 ∈ ℤ )
6 nn0z ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℤ )
7 6 adantr ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ℤ )
8 simpr ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝐹 ) ) → 1 < ( ♯ ‘ 𝐹 ) )
9 fzolb ⊢ ( 1 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( 1 ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℤ ∧ 1 < ( ♯ ‘ 𝐹 ) ) )
10 5 7 8 9 syl3anbrc ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝐹 ) ) → 1 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
11 0elfz ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
12 11 adantr ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝐹 ) ) → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
13 ax-1ne0 ⊢ 1 ≠ 0
14 13 a1i ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝐹 ) ) → 1 ≠ 0 )
15 10 12 14 3jca ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 1 < ( ♯ ‘ 𝐹 ) ) → ( 1 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 1 ≠ 0 ) )
16 15 ex ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 1 < ( ♯ ‘ 𝐹 ) → ( 1 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 1 ≠ 0 ) ) )
17 3 4 16 3syl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 1 < ( ♯ ‘ 𝐹 ) → ( 1 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 1 ≠ 0 ) ) )
18 17 impcom ⊢ ( ( 1 < ( ♯ ‘ 𝐹 ) ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 1 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 1 ≠ 0 ) )
19 pthdivtx ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 1 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 1 ≠ 0 ) ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 0 ) )
20 2 18 19 syl2anc ⊢ ( ( 1 < ( ♯ ‘ 𝐹 ) ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 0 ) )
21 20 necomd ⊢ ( ( 1 < ( ♯ ‘ 𝐹 ) ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) )
22 21 3adant1 ⊢ ( ( 𝐼 = 0 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) )
23 fveq2 ⊢ ( 𝐼 = 0 → ( 𝑃 ‘ 𝐼 ) = ( 𝑃 ‘ 0 ) )
24 fv0p1e1 ⊢ ( 𝐼 = 0 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) = ( 𝑃 ‘ 1 ) )
25 23 24 neeq12d ⊢ ( 𝐼 = 0 → ( ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
26 25 3ad2ant1 ⊢ ( ( 𝐼 = 0 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
27 22 26 mpbird ⊢ ( ( 𝐼 = 0 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ ( 𝐼 + 1 ) ) )
28 27 3exp ⊢ ( 𝐼 = 0 → ( 1 < ( ♯ ‘ 𝐹 ) → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
29 simp3 ⊢ ( ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
30 id ⊢ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
31 fzo0ss1 ⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
32 31 sseli ⊢ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
33 fzofzp1 ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
34 32 33 syl ⊢ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
35 elfzoelz ⊢ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝐼 ∈ ℤ )
36 35 zcnd ⊢ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝐼 ∈ ℂ )
37 1cnd ⊢ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 1 ∈ ℂ )
38 13 a1i ⊢ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 1 ≠ 0 )
39 36 37 38 3jca ⊢ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ) )
40 addn0nid ⊢ ( ( 𝐼 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ) → ( 𝐼 + 1 ) ≠ 𝐼 )
41 40 necomd ⊢ ( ( 𝐼 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ) → 𝐼 ≠ ( 𝐼 + 1 ) )
42 39 41 syl ⊢ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝐼 ≠ ( 𝐼 + 1 ) )
43 30 34 42 3jca ⊢ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( 𝐼 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ≠ ( 𝐼 + 1 ) ) )
44 43 3ad2ant1 ⊢ ( ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( 𝐼 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ≠ ( 𝐼 + 1 ) ) )
45 pthdivtx ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( 𝐼 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝐼 ≠ ( 𝐼 + 1 ) ) ) → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ ( 𝐼 + 1 ) ) )
46 29 44 45 syl2anc ⊢ ( ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ ( 𝐼 + 1 ) ) )
47 46 3exp ⊢ ( 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 1 < ( ♯ ‘ 𝐹 ) → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
48 28 47 jaoi ⊢ ( ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 1 < ( ♯ ‘ 𝐹 ) → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
49 1 48 syl ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 1 < ( ♯ ‘ 𝐹 ) → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) )
50 49 3imp31 ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 𝐼 ) ≠ ( 𝑃 ‘ ( 𝐼 + 1 ) ) )