Metamath Proof Explorer


Theorem clwwlknnn

Description: The length of a closed walk of a fixed length as word is a positive integer. (Contributed by AV, 22-Mar-2022)

Ref Expression
Assertion clwwlknnn W N ClWWalksN G N

Proof

Step Hyp Ref Expression
1 n0i W N ClWWalksN G ¬ N ClWWalksN G =
2 df-nel N ¬ N
3 2 biimpri ¬ N N
4 3 olcd ¬ N G V N
5 clwwlkneq0 G V N N ClWWalksN G =
6 4 5 syl ¬ N N ClWWalksN G =
7 1 6 nsyl2 W N ClWWalksN G N