Step | Hyp | Ref
| Expression |
1 | | 1e2m1 11013 |
. . . . . . . . . . 11
⊢ 1 = (2
− 1) |
2 | 1 | oveq2i 6560 |
. . . . . . . . . 10
⊢ (𝑁 − 1) = (𝑁 − (2 − 1)) |
3 | | eluzelcn 11575 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℂ) |
4 | | 2cnd 10970 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈ ℂ) |
5 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ ℂ) |
6 | 3, 4, 5 | subsubd 10299 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − (2 − 1)) = ((𝑁 − 2) +
1)) |
7 | 2, 6 | syl5req 2657 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 − 2) + 1) = (𝑁 − 1)) |
8 | 7 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑊‘((𝑁 − 2) + 1)) = (𝑊‘(𝑁 − 1))) |
9 | 8 | preq2d 4219 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → {(𝑊‘(𝑁 − 2)), (𝑊‘((𝑁 − 2) + 1))} = {(𝑊‘(𝑁 − 2)), (𝑊‘(𝑁 − 1))}) |
10 | 9 | adantl 481 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2)) → {(𝑊‘(𝑁 − 2)), (𝑊‘((𝑁 − 2) + 1))} = {(𝑊‘(𝑁 − 2)), (𝑊‘(𝑁 − 1))}) |
11 | 10 | adantr 480 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑊 ∈ (𝑁 ClWWalkSN 𝐺)) → {(𝑊‘(𝑁 − 2)), (𝑊‘((𝑁 − 2) + 1))} = {(𝑊‘(𝑁 − 2)), (𝑊‘(𝑁 − 1))}) |
12 | | ige2m2fzo 12398 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈ (0..^(𝑁 − 1))) |
13 | 12 | adantl 481 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2)) → (𝑁 − 2) ∈ (0..^(𝑁 − 1))) |
14 | | eqid 2610 |
. . . . . . . 8
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
15 | | eqid 2610 |
. . . . . . . 8
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
16 | 14, 15 | clwwlknp 41195 |
. . . . . . 7
⊢ (𝑊 ∈ (𝑁 ClWWalkSN 𝐺) → ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))) |
17 | 16 | simp2d 1067 |
. . . . . 6
⊢ (𝑊 ∈ (𝑁 ClWWalkSN 𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
18 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑖 = (𝑁 − 2) → (𝑊‘𝑖) = (𝑊‘(𝑁 − 2))) |
19 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑁 − 2) → (𝑖 + 1) = ((𝑁 − 2) + 1)) |
20 | 19 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑖 = (𝑁 − 2) → (𝑊‘(𝑖 + 1)) = (𝑊‘((𝑁 − 2) + 1))) |
21 | 18, 20 | preq12d 4220 |
. . . . . . . 8
⊢ (𝑖 = (𝑁 − 2) → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘(𝑁 − 2)), (𝑊‘((𝑁 − 2) + 1))}) |
22 | 21 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑖 = (𝑁 − 2) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 2)), (𝑊‘((𝑁 − 2) + 1))} ∈ (Edg‘𝐺))) |
23 | 22 | rspcva 3280 |
. . . . . 6
⊢ (((𝑁 − 2) ∈ (0..^(𝑁 − 1)) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → {(𝑊‘(𝑁 − 2)), (𝑊‘((𝑁 − 2) + 1))} ∈ (Edg‘𝐺)) |
24 | 13, 17, 23 | syl2an 493 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑊 ∈ (𝑁 ClWWalkSN 𝐺)) → {(𝑊‘(𝑁 − 2)), (𝑊‘((𝑁 − 2) + 1))} ∈ (Edg‘𝐺)) |
25 | 11, 24 | eqeltrrd 2689 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑊 ∈ (𝑁 ClWWalkSN 𝐺)) → {(𝑊‘(𝑁 − 2)), (𝑊‘(𝑁 − 1))} ∈ (Edg‘𝐺)) |
26 | 25 | 3adant3 1074 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑊 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → {(𝑊‘(𝑁 − 2)), (𝑊‘(𝑁 − 1))} ∈ (Edg‘𝐺)) |
27 | | preq2 4213 |
. . . . . . 7
⊢ ((𝑊‘0) = (𝑊‘(𝑁 − 2)) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘(𝑁 − 2))}) |
28 | 27 | eqcoms 2618 |
. . . . . 6
⊢ ((𝑊‘(𝑁 − 2)) = (𝑊‘0) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘(𝑁 − 2))}) |
29 | | prcom 4211 |
. . . . . 6
⊢ {(𝑊‘(𝑁 − 1)), (𝑊‘(𝑁 − 2))} = {(𝑊‘(𝑁 − 2)), (𝑊‘(𝑁 − 1))} |
30 | 28, 29 | syl6eq 2660 |
. . . . 5
⊢ ((𝑊‘(𝑁 − 2)) = (𝑊‘0) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} = {(𝑊‘(𝑁 − 2)), (𝑊‘(𝑁 − 1))}) |
31 | 30 | eleq1d 2672 |
. . . 4
⊢ ((𝑊‘(𝑁 − 2)) = (𝑊‘0) → ({(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 2)), (𝑊‘(𝑁 − 1))} ∈ (Edg‘𝐺))) |
32 | 31 | 3ad2ant3 1077 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑊 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → ({(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 2)), (𝑊‘(𝑁 − 1))} ∈ (Edg‘𝐺))) |
33 | 26, 32 | mpbird 246 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑊 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺)) |
34 | 15 | nbusgreledg 40575 |
. . . 4
⊢ (𝐺 ∈ USGraph → ((𝑊‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx (𝑊‘0)) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺))) |
35 | 34 | adantr 480 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2)) → ((𝑊‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx (𝑊‘0)) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺))) |
36 | 35 | 3ad2ant1 1075 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑊 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → ((𝑊‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx (𝑊‘0)) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺))) |
37 | 33, 36 | mpbird 246 |
1
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑊 ∈ (𝑁 ClWWalkSN 𝐺) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → (𝑊‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx (𝑊‘0))) |