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+1WWalksNG
wwlksnextprop.e ⊢E=Edg⁡G
Assertion wwlksnextproplem2 ⊢W∈X∧N∈ℕ0→lastS⁡WprefixN+1lastS⁡W∈E

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x ⊢X=N+1WWalksNG
2 wwlksnextprop.e ⊢E=Edg⁡G
3 eqid ⊢Vtx⁡G=Vtx⁡G
4 3 2 wwlknp ⊢W∈N+1WWalksNG→W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E
5 fzonn0p1 ⊢N∈ℕ0→N∈0..^N+1
6 5 adantl ⊢W∈WordVtx⁡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⁡iW⁡i+1=W⁡NW⁡N+1
10 9 eleq1d ⊢i=N→W⁡iW⁡i+1∈E↔W⁡NW⁡N+1∈E
11 10 rspcv ⊢N∈0..^N+1→∀i∈0..^N+1W⁡iW⁡i+1∈E→W⁡NW⁡N+1∈E
12 6 11 syl ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→∀i∈0..^N+1W⁡iW⁡i+1∈E→W⁡NW⁡N+1∈E
13 12 imp ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧∀i∈0..^N+1W⁡iW⁡i+1∈E→W⁡NW⁡N+1∈E
14 simpll ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→W∈WordVtx⁡G
15 1zzd ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→1∈ℤ
16 lencl ⊢W∈WordVtx⁡G→W∈ℕ0
17 16 nn0zd ⊢W∈WordVtx⁡G→W∈ℤ
18 17 ad2antrr ⊢W∈WordVtx⁡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∈WordVtx⁡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∈WordVtx⁡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∈WordVtx⁡G→W=N+1+1→N∈ℕ0→N+1≤W
35 34 imp31 ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1≤W
36 15 18 21 27 35 elfzd ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1∈1…W
37 pfxfvlsw ⊢W∈WordVtx⁡G∧N+1∈1…W→lastS⁡WprefixN+1=W⁡N+1-1
38 14 36 37 syl2anc ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→lastS⁡WprefixN+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∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→W⁡N+1-1=W⁡N
44 38 43 eqtrd ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→lastS⁡WprefixN+1=W⁡N
45 lsw ⊢W∈WordVtx⁡G→lastS⁡W=W⁡W−1
46 45 ad2antrr ⊢W∈WordVtx⁡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∈WordVtx⁡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∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→W⁡W−1=W⁡N+1
53 46 52 eqtrd ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→lastS⁡W=W⁡N+1
54 44 53 preq12d ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→lastS⁡WprefixN+1lastS⁡W=W⁡NW⁡N+1
55 54 eleq1d ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→lastS⁡WprefixN+1lastS⁡W∈E↔W⁡NW⁡N+1∈E
56 55 adantr ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧∀i∈0..^N+1W⁡iW⁡i+1∈E→lastS⁡WprefixN+1lastS⁡W∈E↔W⁡NW⁡N+1∈E
57 13 56 mpbird ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0∧∀i∈0..^N+1W⁡iW⁡i+1∈E→lastS⁡WprefixN+1lastS⁡W∈E
58 57 exp31 ⊢W∈WordVtx⁡G∧W=N+1+1→N∈ℕ0→∀i∈0..^N+1W⁡iW⁡i+1∈E→lastS⁡WprefixN+1lastS⁡W∈E
59 58 com23 ⊢W∈WordVtx⁡G∧W=N+1+1→∀i∈0..^N+1W⁡iW⁡i+1∈E→N∈ℕ0→lastS⁡WprefixN+1lastS⁡W∈E
60 59 3impia ⊢W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→N∈ℕ0→lastS⁡WprefixN+1lastS⁡W∈E
61 4 60 syl ⊢W∈N+1WWalksNG→N∈ℕ0→lastS⁡WprefixN+1lastS⁡W∈E
62 61 1 eleq2s ⊢W∈X→N∈ℕ0→lastS⁡WprefixN+1lastS⁡W∈E
63 62 imp ⊢W∈X∧N∈ℕ0→lastS⁡WprefixN+1lastS⁡W∈E