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 e. ( N ClWWalksN G ) -> N e. NN )

Proof

Step	Hyp	Ref	Expression
1		n0i	|- ( W e. ( N ClWWalksN G ) -> -. ( N ClWWalksN G ) = (/) )
2		df-nel	|- ( N e/ NN <-> -. N e. NN )
3	2	biimpri	|- ( -. N e. NN -> N e/ NN )
4	3	olcd	|- ( -. N e. NN -> ( G e/ _V \/ N e/ NN ) )
5		clwwlkneq0	|- ( ( G e/ _V \/ N e/ NN ) -> ( N ClWWalksN G ) = (/) )
6	4 5	syl	|- ( -. N e. NN -> ( N ClWWalksN G ) = (/) )
7	1 6	nsyl2	|- ( W e. ( N ClWWalksN G ) -> N e. NN )