Metamath Proof Explorer


Theorem crctcshlem1

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 )

Proof

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 )