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\mathrm{Walks}\left(G\right)P\to \left|F\right|=\left|P\right|-1$$

Proof

Step	Hyp	Ref	Expression
1		wlklenvp1	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|P\right|=\left|F\right|+1$$
2		oveq1	$$⊢\left|P\right|=\left|F\right|+1\to \left|P\right|-1=\left|F\right|+1-1$$
3		wlkcl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|\in {\mathbb{N}}_0$$
4	3	nn0cnd	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|\in ℂ$$
5		pncan1	$$⊢\left|F\right|\in ℂ\to \left|F\right|+1-1=\left|F\right|$$
6	4 5	syl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|+1-1=\left|F\right|$$
7	2 6	sylan9eqr	$$⊢\left(F\mathrm{Walks}\left(G\right)P\wedge \left|P\right|=\left|F\right|+1\right)\to \left|P\right|-1=\left|F\right|$$
8	7	eqcomd	$$⊢\left(F\mathrm{Walks}\left(G\right)P\wedge \left|P\right|=\left|F\right|+1\right)\to \left|F\right|=\left|P\right|-1$$
9	1 8	mpdan	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|=\left|P\right|-1$$