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

Proof

Step	Hyp	Ref	Expression
1		n0i	$$⊢W\in \left(N\mathrm{ClWWalksN}G\right)\to \neg N\mathrm{ClWWalksN}G=\varnothing$$
2		df-nel	$$⊢N\notin \mathbb{N}\leftrightarrow \neg N\in \mathbb{N}$$
3	2	biimpri	$$⊢\neg N\in \mathbb{N}\to N\notin \mathbb{N}$$
4	3	olcd	$$⊢\neg N\in \mathbb{N}\to \left(G\notin \mathrm{V}\vee N\notin \mathbb{N}\right)$$
5		clwwlkneq0	$$⊢\left(G\notin \mathrm{V}\vee N\notin \mathbb{N}\right)\to N\mathrm{ClWWalksN}G=\varnothing$$
6	4 5	syl	$$⊢\neg N\in \mathbb{N}\to N\mathrm{ClWWalksN}G=\varnothing$$
7	1 6	nsyl2	$$⊢W\in \left(N\mathrm{ClWWalksN}G\right)\to N\in \mathbb{N}$$