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