This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wlklenvm1

Description: The number of edges of a walk is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018) (Revised by AV, 2-Jan-2021)

Ref Expression
Assertion wlklenvm1 ⊢ F Walks ⁡ G P → F = P − 1

Proof

Step Hyp Ref Expression
1 wlklenvp1 ⊢ F Walks ⁡ G P → P = F + 1
2 oveq1 ⊢ P = F + 1 → P − 1 = F + 1 - 1
3 wlkcl ⊢ F Walks ⁡ G P → F ∈ ℕ 0
4 3 nn0cnd ⊢ F Walks ⁡ G P → F ∈ ℂ
5 pncan1 ⊢ F ∈ ℂ → F + 1 - 1 = F
6 4 5 syl ⊢ F Walks ⁡ G P → F + 1 - 1 = F
7 2 6 sylan9eqr ⊢ F Walks ⁡ G P ∧ P = F + 1 → P − 1 = F
8 7 eqcomd ⊢ F Walks ⁡ G P ∧ P = F + 1 → F = P − 1
9 1 8 mpdan ⊢ F Walks ⁡ G P → F = P − 1