Description: The N -th edge in an eulerian path is the edge having P ( N ) and P ( N + 1 ) as endpoints . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 18-Feb-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | eupths.i | |
|
Assertion | eupthseg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eupths.i | |
|
2 | 1 | eupthi | |
3 | 2 | simpld | |
4 | 1 | wlkvtxeledg | |
5 | fveq2 | |
|
6 | fvoveq1 | |
|
7 | 5 6 | preq12d | |
8 | 2fveq3 | |
|
9 | 7 8 | sseq12d | |
10 | 9 | rspccv | |
11 | 3 4 10 | 3syl | |
12 | 11 | imp | |