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 -> ( # ` F ) e. NN0 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
2 1 eupthi 
 |-  ( F ( EulerPaths ` G ) P -> ( F ( Walks ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom ( iEdg ` G ) ) )
3 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
4 3 adantr 
 |-  ( ( F ( Walks ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom ( iEdg ` G ) ) -> ( # ` F ) e. NN0 )
5 2 4 syl 
 |-  ( F ( EulerPaths ` G ) P -> ( # ` F ) e. NN0 )