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	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑁 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		n0i	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ¬ ( 𝑁 ClWWalksN 𝐺 ) = ∅ )
2		df-nel	⊢ ( 𝑁 ∉ ℕ ↔ ¬ 𝑁 ∈ ℕ )
3	2	biimpri	⊢ ( ¬ 𝑁 ∈ ℕ → 𝑁 ∉ ℕ )
4	3	olcd	⊢ ( ¬ 𝑁 ∈ ℕ → ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ ) )
5		clwwlkneq0	⊢ ( ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ ) → ( 𝑁 ClWWalksN 𝐺 ) = ∅ )
6	4 5	syl	⊢ ( ¬ 𝑁 ∈ ℕ → ( 𝑁 ClWWalksN 𝐺 ) = ∅ )
7	1 6	nsyl2	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑁 ∈ ℕ )