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 nn0ge0 ⊢ N ∈ ℕ 0 → 0 ≤ N
23 1red ⊢ N ∈ ℕ 0 → 1 ∈ ℝ
24 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
25 23 24 addge02d ⊢ N ∈ ℕ 0 → 0 ≤ N ↔ 1 ≤ N + 1
26 22 25 mpbid ⊢ N ∈ ℕ 0 → 1 ≤ N + 1
27 26 adantl ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → 1 ≤ N + 1
28 19 nn0red ⊢ N ∈ ℕ 0 → N + 1 ∈ ℝ
29 28 lep1d ⊢ N ∈ ℕ 0 → N + 1 ≤ N + 1 + 1
30 breq2 ⊢ W = N + 1 + 1 → N + 1 ≤ W ↔ N + 1 ≤ N + 1 + 1
31 29 30 syl5ibrcom ⊢ N ∈ ℕ 0 → W = N + 1 + 1 → N + 1 ≤ W
32 31 a1i ⊢ W ∈ ℕ 0 → N ∈ ℕ 0 → W = N + 1 + 1 → N + 1 ≤ W
33 32 com23 ⊢ W ∈ ℕ 0 → W = N + 1 + 1 → N ∈ ℕ 0 → N + 1 ≤ W
34 16 33 syl ⊢ W ∈ Word Vtx ⁡ G → W = N + 1 + 1 → N ∈ ℕ 0 → N + 1 ≤ W
35 34 imp31 ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → N + 1 ≤ W
36 15 18 21 27 35 elfzd ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → N + 1 ∈ 1 … W
37 pfxfvlsw ⊢ W ∈ Word Vtx ⁡ G ∧ N + 1 ∈ 1 … W → lastS ⁡ W prefix N + 1 = W ⁡ N + 1 - 1
38 14 36 37 syl2anc ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 = W ⁡ N + 1 - 1
39 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
40 1cnd ⊢ N ∈ ℕ 0 → 1 ∈ ℂ
41 39 40 pncand ⊢ N ∈ ℕ 0 → N + 1 - 1 = N
42 41 fveq2d ⊢ N ∈ ℕ 0 → W ⁡ N + 1 - 1 = W ⁡ N
43 42 adantl ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W ⁡ N + 1 - 1 = W ⁡ N
44 38 43 eqtrd ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 = W ⁡ N
45 lsw ⊢ W ∈ Word Vtx ⁡ G → lastS ⁡ W = W ⁡ W − 1
46 45 ad2antrr ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → lastS ⁡ W = W ⁡ W − 1
47 fvoveq1 ⊢ W = N + 1 + 1 → W ⁡ W − 1 = W ⁡ N + 1 + 1 - 1
48 47 adantl ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 → W ⁡ W − 1 = W ⁡ N + 1 + 1 - 1
49 19 nn0cnd ⊢ N ∈ ℕ 0 → N + 1 ∈ ℂ
50 49 40 pncand ⊢ N ∈ ℕ 0 → N + 1 + 1 - 1 = N + 1
51 50 fveq2d ⊢ N ∈ ℕ 0 → W ⁡ N + 1 + 1 - 1 = W ⁡ N + 1
52 48 51 sylan9eq ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → W ⁡ W − 1 = W ⁡ N + 1
53 46 52 eqtrd ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → lastS ⁡ W = W ⁡ N + 1
54 44 53 preq12d ⊢ W ∈ Word Vtx ⁡ G ∧ W = N + 1 + 1 ∧ N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 lastS ⁡ W = W ⁡ N W ⁡ N + 1
55 54 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
56 55 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
57 13 56 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
58 57 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
59 58 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
60 59 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
61 4 60 syl ⊢ W ∈ N + 1 WWalksN G → N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E
62 61 1 eleq2s ⊢ W ∈ X → N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E
63 62 imp ⊢ W ∈ X ∧ N ∈ ℕ 0 → lastS ⁡ W prefix N + 1 lastS ⁡ W ∈ E