Theorem crctcshlem1

Description: Lemma for crctcsh . (Contributed by AV, 10-Mar-2021)

	Ref	Expression
Hypotheses	crctcsh.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	crctcsh.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	crctcsh.d	$$⊢\phi \to F\mathrm{Circuits}\left(G\right)P$$
	crctcsh.n	$$⊢N=\left|F\right|$$
Assertion	crctcshlem1	$$⊢\phi \to N\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		crctcsh.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		crctcsh.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		crctcsh.d	$$⊢\phi \to F\mathrm{Circuits}\left(G\right)P$$
4		crctcsh.n	$$⊢N=\left|F\right|$$
5		crctiswlk	$$⊢F\mathrm{Circuits}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$
6		wlkcl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|\in {\mathbb{N}}_0$$
7	4 6	eqeltrid	$$⊢F\mathrm{Walks}\left(G\right)P\to N\in {\mathbb{N}}_0$$
8	3 5 7	3syl	$$⊢\phi \to N\in {\mathbb{N}}_0$$