Description: Lemma for crctcsh . (Contributed by AV, 10-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | crctcsh.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
crctcsh.i | ⊢ 𝐼 = ( iEdg ‘ 𝐺 ) | ||
crctcsh.d | ⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) | ||
crctcsh.n | ⊢ 𝑁 = ( ♯ ‘ 𝐹 ) | ||
Assertion | crctcshlem1 | ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crctcsh.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
2 | crctcsh.i | ⊢ 𝐼 = ( iEdg ‘ 𝐺 ) | |
3 | crctcsh.d | ⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) | |
4 | crctcsh.n | ⊢ 𝑁 = ( ♯ ‘ 𝐹 ) | |
5 | crctiswlk | ⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) | |
6 | wlkcl | ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) | |
7 | 4 6 | eqeltrid | ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑁 ∈ ℕ0 ) |
8 | 3 5 7 | 3syl | ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |