Metamath Proof Explorer

Theorem wwlksnextproplem3

Description: Lemma 3 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
wwlksnextprop.y ⊢Y=w∈NWWalksNG|w⁡0=P
Assertion wwlksnextproplem3 ⊢W∈X∧W⁡0=P∧N∈ℕ0→WprefixN+1∈Y

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x ⊢X=N+1WWalksNG
2 wwlksnextprop.e ⊢E=Edg⁡G
3 wwlksnextprop.y ⊢Y=w∈NWWalksNG|w⁡0=P
4 peano2nn0 ⊢N∈ℕ0→N+1∈ℕ0
5 iswwlksn ⊢N+1∈ℕ0→W∈N+1WWalksNG↔W∈WWalks⁡G∧W=N+1+1
6 4 5 syl ⊢N∈ℕ0→W∈N+1WWalksNG↔W∈WWalks⁡G∧W=N+1+1
7 eqid ⊢Vtx⁡G=Vtx⁡G
8 7 wwlkbp ⊢W∈WWalks⁡G→G∈V∧W∈WordVtx⁡G
9 lencl ⊢W∈WordVtx⁡G→W∈ℕ0
10 eqcom ⊢W=N+1+1↔N+1+1=W
11 nn0cn ⊢W∈ℕ0→W∈ℂ
12 11 adantr ⊢W∈ℕ0∧N∈ℕ0→W∈ℂ
13 1cnd ⊢W∈ℕ0∧N∈ℕ0→1∈ℂ
14 nn0cn ⊢N+1∈ℕ0→N+1∈ℂ
15 4 14 syl ⊢N∈ℕ0→N+1∈ℂ
16 15 adantl ⊢W∈ℕ0∧N∈ℕ0→N+1∈ℂ
17 subadd2 ⊢W∈ℂ∧1∈ℂ∧N+1∈ℂ→W−1=N+1↔N+1+1=W
18 17 bicomd ⊢W∈ℂ∧1∈ℂ∧N+1∈ℂ→N+1+1=W↔W−1=N+1
19 12 13 16 18 syl3anc ⊢W∈ℕ0∧N∈ℕ0→N+1+1=W↔W−1=N+1
20 10 19 bitrid ⊢W∈ℕ0∧N∈ℕ0→W=N+1+1↔W−1=N+1
21 eqcom ⊢W−1=N+1↔N+1=W−1
22 21 biimpi ⊢W−1=N+1→N+1=W−1
23 20 22 syl6bi ⊢W∈ℕ0∧N∈ℕ0→W=N+1+1→N+1=W−1
24 23 ex ⊢W∈ℕ0→N∈ℕ0→W=N+1+1→N+1=W−1
25 24 com23 ⊢W∈ℕ0→W=N+1+1→N∈ℕ0→N+1=W−1
26 9 25 syl ⊢W∈WordVtx⁡G→W=N+1+1→N∈ℕ0→N+1=W−1
27 8 26 simpl2im ⊢W∈WWalks⁡G→W=N+1+1→N∈ℕ0→N+1=W−1
28 27 imp31 ⊢W∈WWalks⁡G∧W=N+1+1∧N∈ℕ0→N+1=W−1
29 28 oveq2d ⊢W∈WWalks⁡G∧W=N+1+1∧N∈ℕ0→WprefixN+1=WprefixW−1
30 simpll ⊢W∈WWalks⁡G∧W=N+1+1∧N∈ℕ0→W∈WWalks⁡G
31 nn0ge0 ⊢N∈ℕ0→0≤N
32 2re ⊢2∈ℝ
33 32 a1i ⊢N∈ℕ0→2∈ℝ
34 nn0re ⊢N∈ℕ0→N∈ℝ
35 33 34 addge02d ⊢N∈ℕ0→0≤N↔2≤N+2
36 31 35 mpbid ⊢N∈ℕ0→2≤N+2
37 nn0cn ⊢N∈ℕ0→N∈ℂ
38 1cnd ⊢N∈ℕ0→1∈ℂ
39 37 38 38 addassd ⊢N∈ℕ0→N+1+1=N+1+1
40 1p1e2 ⊢1+1=2
41 40 a1i ⊢N∈ℕ0→1+1=2
42 41 oveq2d ⊢N∈ℕ0→N+1+1=N+2
43 39 42 eqtrd ⊢N∈ℕ0→N+1+1=N+2
44 36 43 breqtrrd ⊢N∈ℕ0→2≤N+1+1
45 44 adantl ⊢W∈WWalks⁡G∧W=N+1+1∧N∈ℕ0→2≤N+1+1
46 breq2 ⊢W=N+1+1→2≤W↔2≤N+1+1
47 46 ad2antlr ⊢W∈WWalks⁡G∧W=N+1+1∧N∈ℕ0→2≤W↔2≤N+1+1
48 45 47 mpbird ⊢W∈WWalks⁡G∧W=N+1+1∧N∈ℕ0→2≤W
49 wwlksm1edg ⊢W∈WWalks⁡G∧2≤W→WprefixW−1∈WWalks⁡G
50 30 48 49 syl2anc ⊢W∈WWalks⁡G∧W=N+1+1∧N∈ℕ0→WprefixW−1∈WWalks⁡G
51 29 50 eqeltrd ⊢W∈WWalks⁡G∧W=N+1+1∧N∈ℕ0→WprefixN+1∈WWalks⁡G
52 51 expcom ⊢N∈ℕ0→W∈WWalks⁡G∧W=N+1+1→WprefixN+1∈WWalks⁡G
53 6 52 sylbid ⊢N∈ℕ0→W∈N+1WWalksNG→WprefixN+1∈WWalks⁡G
54 53 com12 ⊢W∈N+1WWalksNG→N∈ℕ0→WprefixN+1∈WWalks⁡G
55 54 adantr ⊢W∈N+1WWalksNG∧W⁡0=P→N∈ℕ0→WprefixN+1∈WWalks⁡G
56 55 imp ⊢W∈N+1WWalksNG∧W⁡0=P∧N∈ℕ0→WprefixN+1∈WWalks⁡G
57 7 2 wwlknp ⊢W∈N+1WWalksNG→W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E
58 simpll ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→W∈WordVtx⁡G
59 peano2nn0 ⊢N+1∈ℕ0→N+1+1∈ℕ0
60 4 59 syl ⊢N∈ℕ0→N+1+1∈ℕ0
61 peano2re ⊢N∈ℝ→N+1∈ℝ
62 34 61 syl ⊢N∈ℕ0→N+1∈ℝ
63 62 lep1d ⊢N∈ℕ0→N+1≤N+1+1
64 elfz2nn0 ⊢N+1∈0…N+1+1↔N+1∈ℕ0∧N+1+1∈ℕ0∧N+1≤N+1+1
65 4 60 63 64 syl3anbrc ⊢N∈ℕ0→N+1∈0…N+1+1
66 65 adantl ⊢W=N+1+1∧N∈ℕ0→N+1∈0…N+1+1
67 oveq2 ⊢W=N+1+1→0…W=0…N+1+1
68 67 adantr ⊢W=N+1+1∧N∈ℕ0→0…W=0…N+1+1
69 66 68 eleqtrrd ⊢W=N+1+1∧N∈ℕ0→N+1∈0…W
70 69 adantll ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→N+1∈0…W
71 58 70 jca ⊢W∈WordVtx⁡G∧W=N+1+1∧N∈ℕ0→W∈WordVtx⁡G∧N+1∈0…W
72 71 ex ⊢W∈WordVtx⁡G∧W=N+1+1→N∈ℕ0→W∈WordVtx⁡G∧N+1∈0…W
73 72 3adant3 ⊢W∈WordVtx⁡G∧W=N+1+1∧∀i∈0..^N+1W⁡iW⁡i+1∈E→N∈ℕ0→W∈WordVtx⁡G∧N+1∈0…W
74 57 73 syl ⊢W∈N+1WWalksNG→N∈ℕ0→W∈WordVtx⁡G∧N+1∈0…W
75 74 adantr ⊢W∈N+1WWalksNG∧W⁡0=P→N∈ℕ0→W∈WordVtx⁡G∧N+1∈0…W
76 75 imp ⊢W∈N+1WWalksNG∧W⁡0=P∧N∈ℕ0→W∈WordVtx⁡G∧N+1∈0…W
77 pfxlen ⊢W∈WordVtx⁡G∧N+1∈0…W→WprefixN+1=N+1
78 76 77 syl ⊢W∈N+1WWalksNG∧W⁡0=P∧N∈ℕ0→WprefixN+1=N+1
79 56 78 jca ⊢W∈N+1WWalksNG∧W⁡0=P∧N∈ℕ0→WprefixN+1∈WWalks⁡G∧WprefixN+1=N+1
80 iswwlksn ⊢N∈ℕ0→WprefixN+1∈NWWalksNG↔WprefixN+1∈WWalks⁡G∧WprefixN+1=N+1
81 80 adantl ⊢W∈N+1WWalksNG∧W⁡0=P∧N∈ℕ0→WprefixN+1∈NWWalksNG↔WprefixN+1∈WWalks⁡G∧WprefixN+1=N+1
82 79 81 mpbird ⊢W∈N+1WWalksNG∧W⁡0=P∧N∈ℕ0→WprefixN+1∈NWWalksNG
83 82 exp31 ⊢W∈N+1WWalksNG→W⁡0=P→N∈ℕ0→WprefixN+1∈NWWalksNG
84 83 1 eleq2s ⊢W∈X→W⁡0=P→N∈ℕ0→WprefixN+1∈NWWalksNG
85 84 3imp ⊢W∈X∧W⁡0=P∧N∈ℕ0→WprefixN+1∈NWWalksNG
86 1 wwlksnextproplem1 ⊢W∈X∧N∈ℕ0→WprefixN+1⁡0=W⁡0
87 86 3adant2 ⊢W∈X∧W⁡0=P∧N∈ℕ0→WprefixN+1⁡0=W⁡0
88 simp2 ⊢W∈X∧W⁡0=P∧N∈ℕ0→W⁡0=P
89 87 88 eqtrd ⊢W∈X∧W⁡0=P∧N∈ℕ0→WprefixN+1⁡0=P
90 fveq1 ⊢w=WprefixN+1→w⁡0=WprefixN+1⁡0
91 90 eqeq1d ⊢w=WprefixN+1→w⁡0=P↔WprefixN+1⁡0=P
92 91 3 elrab2 ⊢WprefixN+1∈Y↔WprefixN+1∈NWWalksNG∧WprefixN+1⁡0=P
93 85 89 92 sylanbrc ⊢W∈X∧W⁡0=P∧N∈ℕ0→WprefixN+1∈Y