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\mathrm{EulerPaths}\left(G\right)P\to \left|F\right|\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{iEdg}\left(G\right)=\mathrm{iEdg}\left(G\right)$$
2	1	eupthi	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to \left(F\mathrm{Walks}\left(G\right)P\wedge F:\left(0..^\left|F\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(G\right)\right)$$
3		wlkcl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|\in {\mathbb{N}}_0$$
4	3	adantr	$$⊢\left(F\mathrm{Walks}\left(G\right)P\wedge F:\left(0..^\left|F\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(G\right)\right)\to \left|F\right|\in {\mathbb{N}}_0$$
5	2 4	syl	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to \left|F\right|\in {\mathbb{N}}_0$$