Metamath Proof Explorer

Theorem wwlksnextproplem2

Description: Lemma 2 for wwlksnextprop . (Contributed by Alexander van der Vekens, 1-Aug-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 29-Oct-2022)

Ref Expression
Hypotheses wwlksnextprop.x ⊢ X = N + 1 WWalksN G
wwlksnextprop.e ⊢ E = Edg ⁡ G
Assertion wwlksnextproplem2 ⊢ W ∈ X ∧ N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x ⊢ X = N + 1 WWalksN G
2 wwlksnextprop.e ⊢ E = Edg ⁡ G
3 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
4 3 2 wwlknp ⊢ W ∈ N + 1 WWalksN G → W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E
5 fzonn0p1 ⊢ N ∈ ℕ 0 → N ∈ 0 ..^ N + 1
6 5 adantl ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → N ∈ 0 ..^ N + 1
7 fveq2 ⊢ i = N → W ⁡ i = W ⁡ N
8 fvoveq1 ⊢ i = N → W ⁡ i + 1 = W ⁡ N + 1
9 7 8 preq12d ⊢ i = N → W ⁡ i W ⁡ i + 1 = W ⁡ N W ⁡ N + 1
10 9 eleq1d ⊢ i = N → W ⁡ i W ⁡ i + 1 ∈ E ↔ W ⁡ N W ⁡ N + 1 ∈ E
11 10 rspcv ⊢ N ∈ 0 ..^ N + 1 → ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → W ⁡ N W ⁡ N + 1 ∈ E
12 6 11 syl ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → W ⁡ N W ⁡ N + 1 ∈ E
13 12 imp ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → W ⁡ N W ⁡ N + 1 ∈ E
14 simpll ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W ∈ Word Vtx ⁡ G
15 1zzd ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → 1 ∈ ℤ
16 lencl ⊢ W ∈ Word Vtx ⁡ G → W ∈ ℕ 0
17 16 nn0zd ⊢ W ∈ Word Vtx ⁡ G → W ∈ ℤ
18 17 ad2antrr ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W ∈ ℤ
19 peano2nn0 ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ 0
20 19 nn0zd ⊢ N ∈ ℕ 0 → N + 1 ∈ ℤ
21 20 adantl ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → N + 1 ∈ ℤ
22 15 18 21 3jca ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → 1 ∈ ℤ ∧ W ∈ ℤ ∧ N + 1 ∈ ℤ
23 nn0ge0 ⊢ N ∈ ℕ 0 → 0 ≤ N
24 1red ⊢ N ∈ ℕ 0 → 1 ∈ ℝ
25 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
26 24 25 addge02d ⊢ N ∈ ℕ 0 → 0 ≤ N ↔ 1 ≤ N + 1
27 23 26 mpbid ⊢ N ∈ ℕ 0 → 1 ≤ N + 1
28 27 adantl ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → 1 ≤ N + 1
29 19 nn0red ⊢ N ∈ ℕ 0 → N + 1 ∈ ℝ
30 29 lep1d ⊢ N ∈ ℕ 0 → N + 1 ≤ N + 1 + 1
31 breq2 ⊢ W = N + 1 + 1 → N + 1 ≤ W ↔ N + 1 ≤ N + 1 + 1
32 30 31 syl5ibrcom ⊢ N ∈ ℕ 0 → W = N + 1 + 1 → N + 1 ≤ W
33 32 a1i ⊢ W ∈ ℕ 0 → N ∈ ℕ 0 → W = N + 1 + 1 → N + 1 ≤ W
34 33 com23 ⊢ W ∈ ℕ 0 → W = N + 1 + 1 → N ∈ ℕ 0 → N + 1 ≤ W
35 16 34 syl ⊢ W ∈ Word Vtx ⁡ G → W = N + 1 + 1 → N ∈ ℕ 0 → N + 1 ≤ W
36 35 imp31 ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → N + 1 ≤ W
37 28 36 jca ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → 1 ≤ N + 1 ∧ N + 1 ≤ W
38 elfz2 ⊢ N + 1 ∈ 1 … W ↔ 1 ∈ ℤ ∧ W ∈ ℤ ∧ N + 1 ∈ ℤ ∧ 1 ≤ N + 1 ∧ N + 1 ≤ W
39 22 37 38 sylanbrc ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → N + 1 ∈ 1 … W
40 pfxfvlsw ⊢ W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 1 … W → lastS ⁡ W prefix N + 1 = W ⁡ N + 1 - 1
41 14 39 40 syl2anc ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 = W ⁡ N + 1 - 1
42 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
43 1cnd ⊢ N ∈ ℕ 0 → 1 ∈ ℂ
44 42 43 pncand ⊢ N ∈ ℕ 0 → N + 1 - 1 = N
45 44 fveq2d ⊢ N ∈ ℕ 0 → W ⁡ N + 1 - 1 = W ⁡ N
46 45 adantl ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W ⁡ N + 1 - 1 = W ⁡ N
47 41 46 eqtrd ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 = W ⁡ N
48 lsw ⊢ W ∈ Word Vtx ⁡ G → lastS ⁡ W = W ⁡ W − 1
49 48 ad2antrr ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → lastS ⁡ W = W ⁡ W − 1
50 fvoveq1 ⊢ W = N + 1 + 1 → W ⁡ W − 1 = W ⁡ N + 1 + 1 - 1
51 50 adantl ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → W ⁡ W − 1 = W ⁡ N + 1 + 1 - 1
52 19 nn0cnd ⊢ N ∈ ℕ 0 → N + 1 ∈ ℂ
53 52 43 pncand ⊢ N ∈ ℕ 0 → N + 1 + 1 - 1 = N + 1
54 53 fveq2d ⊢ N ∈ ℕ 0 → W ⁡ N + 1 + 1 - 1 = W ⁡ N + 1
55 51 54 sylan9eq ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W ⁡ W − 1 = W ⁡ N + 1
56 49 55 eqtrd ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → lastS ⁡ W = W ⁡ N + 1
57 47 56 preq12d ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 lastS ⁡ W = W ⁡ N W ⁡ N + 1
58 57 eleq1d ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E ↔ W ⁡ N W ⁡ N + 1 ∈ E
59 58 adantr ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E ↔ W ⁡ N W ⁡ N + 1 ∈ E
60 13 59 mpbird ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E
61 60 exp31 ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → N ∈ ℕ 0 → ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E
62 61 com23 ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E
63 62 3impia ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 W ⁡ i W ⁡ i + 1 ∈ E → N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E
64 4 63 syl ⊢ W ∈ N + 1 WWalksN G → N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E
65 64 1 eleq2s ⊢ W ∈ X → N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E
66 65 imp ⊢ W ∈ X ∧ N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E