Step | Hyp | Ref
| Expression |
1 | | eqid 2772 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | | wwlksnextprop.e |
. . . . 5
⊢ 𝐸 = (Edg‘𝐺) |
3 | 1, 2 | wwlknp 27319 |
. . . 4
⊢ (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) |
4 | | fzonn0p1 12922 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0..^(𝑁 + 1))) |
5 | 4 | adantl 474 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ (0..^(𝑁 + 1))) |
6 | | fveq2 6493 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑁 → (𝑊‘𝑖) = (𝑊‘𝑁)) |
7 | | fvoveq1 6993 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑁 → (𝑊‘(𝑖 + 1)) = (𝑊‘(𝑁 + 1))) |
8 | 6, 7 | preq12d 4545 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑁 → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))}) |
9 | 8 | eleq1d 2844 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑁 → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
10 | 9 | rspcv 3525 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (0..^(𝑁 + 1)) → (∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
11 | 5, 10 | syl 17 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) →
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
12 | 11 | imp 398 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) ∧
∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸) |
13 | | simpll 754 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 𝑊 ∈ Word (Vtx‘𝐺)) |
14 | | 1zzd 11819 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 1 ∈
ℤ) |
15 | | lencl 13684 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (♯‘𝑊) ∈
ℕ0) |
16 | 15 | nn0zd 11891 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (♯‘𝑊) ∈
ℤ) |
17 | 16 | ad2antrr 713 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) →
(♯‘𝑊) ∈
ℤ) |
18 | | peano2nn0 11742 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
19 | 18 | nn0zd 11891 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℤ) |
20 | 19 | adantl 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ∈
ℤ) |
21 | 14, 17, 20 | 3jca 1108 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (1
∈ ℤ ∧ (♯‘𝑊) ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ)) |
22 | | nn0ge0 11727 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
23 | | 1red 10432 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℝ) |
24 | | nn0re 11710 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
25 | 23, 24 | addge02d 11022 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ (0 ≤ 𝑁 ↔ 1
≤ (𝑁 +
1))) |
26 | 22, 25 | mpbid 224 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 1 ≤ (𝑁 +
1)) |
27 | 26 | adantl 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → 1 ≤
(𝑁 + 1)) |
28 | 18 | nn0red 11761 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) |
29 | 28 | lep1d 11364 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) |
30 | | breq2 4927 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑊) =
((𝑁 + 1) + 1) →
((𝑁 + 1) ≤
(♯‘𝑊) ↔
(𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
31 | 29, 30 | syl5ibrcom 239 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ ((♯‘𝑊) =
((𝑁 + 1) + 1) → (𝑁 + 1) ≤ (♯‘𝑊))) |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑊)
∈ ℕ0 → (𝑁 ∈ ℕ0 →
((♯‘𝑊) =
((𝑁 + 1) + 1) → (𝑁 + 1) ≤ (♯‘𝑊)))) |
33 | 32 | com23 86 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑊)
∈ ℕ0 → ((♯‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑁 + 1) ≤ (♯‘𝑊)))) |
34 | 15, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑁 + 1) ≤ (♯‘𝑊)))) |
35 | 34 | imp31 410 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ≤ (♯‘𝑊)) |
36 | 27, 35 | jca 504 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (1 ≤
(𝑁 + 1) ∧ (𝑁 + 1) ≤ (♯‘𝑊))) |
37 | | elfz2 12708 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 + 1) ∈
(1...(♯‘𝑊))
↔ ((1 ∈ ℤ ∧ (♯‘𝑊) ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) ∧ (1 ≤ (𝑁 + 1) ∧ (𝑁 + 1) ≤ (♯‘𝑊)))) |
38 | 21, 36, 37 | sylanbrc 575 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ∈
(1...(♯‘𝑊))) |
39 | | pfxfvlsw 13867 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(♯‘𝑊))) → (lastS‘(𝑊 prefix (𝑁 + 1))) = (𝑊‘((𝑁 + 1) − 1))) |
40 | 13, 38, 39 | syl2anc 576 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) →
(lastS‘(𝑊 prefix
(𝑁 + 1))) = (𝑊‘((𝑁 + 1) − 1))) |
41 | | nn0cn 11711 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
42 | | 1cnd 10426 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
43 | 41, 42 | pncand 10791 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
44 | 43 | fveq2d 6497 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑊‘((𝑁 + 1) − 1)) = (𝑊‘𝑁)) |
45 | 44 | adantl 474 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑊‘((𝑁 + 1) − 1)) = (𝑊‘𝑁)) |
46 | 40, 45 | eqtrd 2808 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) →
(lastS‘(𝑊 prefix
(𝑁 + 1))) = (𝑊‘𝑁)) |
47 | | lsw 13717 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1))) |
48 | 47 | ad2antrr 713 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) →
(lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1))) |
49 | | fvoveq1 6993 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑊) =
((𝑁 + 1) + 1) → (𝑊‘((♯‘𝑊) − 1)) = (𝑊‘(((𝑁 + 1) + 1) − 1))) |
50 | 49 | adantl 474 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊‘((♯‘𝑊) − 1)) = (𝑊‘(((𝑁 + 1) + 1) − 1))) |
51 | 18 | nn0cnd 11762 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
52 | 51, 42 | pncand 10791 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) + 1)
− 1) = (𝑁 +
1)) |
53 | 52 | fveq2d 6497 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑊‘(((𝑁 + 1) + 1) − 1)) = (𝑊‘(𝑁 + 1))) |
54 | 50, 53 | sylan9eq 2828 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) → (𝑊‘((♯‘𝑊) − 1)) = (𝑊‘(𝑁 + 1))) |
55 | 48, 54 | eqtrd 2808 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) →
(lastS‘𝑊) = (𝑊‘(𝑁 + 1))) |
56 | 46, 55 | preq12d 4545 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) →
{(lastS‘(𝑊 prefix
(𝑁 + 1))),
(lastS‘𝑊)} = {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))}) |
57 | 56 | eleq1d 2844 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) →
({(lastS‘(𝑊 prefix
(𝑁 + 1))),
(lastS‘𝑊)} ∈
𝐸 ↔ {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
58 | 57 | adantr 473 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) ∧
∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ({(lastS‘(𝑊 prefix (𝑁 + 1))), (lastS‘𝑊)} ∈ 𝐸 ↔ {(𝑊‘𝑁), (𝑊‘(𝑁 + 1))} ∈ 𝐸)) |
59 | 12, 58 | mpbird 249 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0) ∧
∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → {(lastS‘(𝑊 prefix (𝑁 + 1))), (lastS‘𝑊)} ∈ 𝐸) |
60 | 59 | exp31 412 |
. . . . . 6
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 →
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → {(lastS‘(𝑊 prefix (𝑁 + 1))), (lastS‘𝑊)} ∈ 𝐸))) |
61 | 60 | com23 86 |
. . . . 5
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → (𝑁 ∈ ℕ0 →
{(lastS‘(𝑊 prefix
(𝑁 + 1))),
(lastS‘𝑊)} ∈
𝐸))) |
62 | 61 | 3impia 1097 |
. . . 4
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1) ∧ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (𝑁 ∈ ℕ0 →
{(lastS‘(𝑊 prefix
(𝑁 + 1))),
(lastS‘𝑊)} ∈
𝐸)) |
63 | 3, 62 | syl 17 |
. . 3
⊢ (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) → (𝑁 ∈ ℕ0 →
{(lastS‘(𝑊 prefix
(𝑁 + 1))),
(lastS‘𝑊)} ∈
𝐸)) |
64 | | wwlksnextprop.x |
. . 3
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) |
65 | 63, 64 | eleq2s 2878 |
. 2
⊢ (𝑊 ∈ 𝑋 → (𝑁 ∈ ℕ0 →
{(lastS‘(𝑊 prefix
(𝑁 + 1))),
(lastS‘𝑊)} ∈
𝐸)) |
66 | 65 | imp 398 |
1
⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) →
{(lastS‘(𝑊 prefix
(𝑁 + 1))),
(lastS‘𝑊)} ∈
𝐸) |