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