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

Metamath Proof Explorer

Theorem wlkcl

Description: A walk has length # ( F ) , which is an integer. Formerly proven for an Eulerian path, see eupthcl . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 18-Feb-2021)

Ref Expression
Assertion wlkcl ⊢ F Walks ⁡ G P → F ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
2 1 wlkf ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ iEdg ⁡ G
3 lencl ⊢ F ∈ Word dom ⁡ iEdg ⁡ G → F ∈ ℕ 0
4 2 3 syl ⊢ F Walks ⁡ G P → F ∈ ℕ 0