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 
|- ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ I e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` I ) =/= ( P ` ( I + 1 ) ) )

Proof

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