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

Metamath Proof Explorer

Theorem eupthcl

Description: An Eulerian path has length # ( F ) , which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 18-Feb-2021)

		Ref	Expression
	Assertion	eupthcl	$⊢ F EulerPaths (G) P \to \|F\| \in ℕ_{0}$

Step	Hyp	Ref	Expression
1		eqid	$⊢ iEdg (G) = iEdg (G)$
2	1	eupthi	$⊢ F EulerPaths (G) P \to (F Walks (G) P \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom iEdg (G))$
3		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
4	3	adantr	$⊢ (F Walks (G) P \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom iEdg (G)) \to \|F\| \in ℕ_{0}$
5	2 4	syl	$⊢ F EulerPaths (G) P \to \|F\| \in ℕ_{0}$