Theorem eucrct2eupth1

Description: Removing one edge ( I( FN ) ) from a nonempty graph G with an Eulerian circuit <. F , P >. results in a graph S with an Eulerian path <. H , Q >. . This is the special case of eucrct2eupth (with J = ( N - 1 ) ) where the last segment/edge of the circuit is removed. (Contributed by AV, 11-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

	Ref	Expression
Hypotheses	eucrct2eupth1.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	eucrct2eupth1.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	eucrct2eupth1.d	$$⊢\phi \to F\mathrm{EulerPaths}\left(G\right)P$$
	eucrct2eupth1.c	$$⊢\phi \to F\mathrm{Circuits}\left(G\right)P$$
	eucrct2eupth1.s	$$⊢\mathrm{Vtx}\left(S\right)=V$$
	eucrct2eupth1.g	$$⊢\phi \to 0<\left|F\right|$$
	eucrct2eupth1.n	$$⊢\phi \to N=\left|F\right|-1$$
	eucrct2eupth1.e	$$⊢\phi \to \mathrm{iEdg}\left(S\right)={I\upharpoonright }_{F\left[\left(0..^N\right)\right]}$$
	eucrct2eupth1.h	$$⊢H=F\mathrm{prefix}N$$
	eucrct2eupth1.q	$$⊢Q={P\upharpoonright }_{\left(0\dots N\right)}$$
Assertion	eucrct2eupth1	$$⊢\phi \to H\mathrm{EulerPaths}\left(S\right)Q$$

Proof

Step	Hyp	Ref	Expression
1		eucrct2eupth1.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		eucrct2eupth1.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		eucrct2eupth1.d	$$⊢\phi \to F\mathrm{EulerPaths}\left(G\right)P$$
4		eucrct2eupth1.c	$$⊢\phi \to F\mathrm{Circuits}\left(G\right)P$$
5		eucrct2eupth1.s	$$⊢\mathrm{Vtx}\left(S\right)=V$$
6		eucrct2eupth1.g	$$⊢\phi \to 0<\left|F\right|$$
7		eucrct2eupth1.n	$$⊢\phi \to N=\left|F\right|-1$$
8		eucrct2eupth1.e	$$⊢\phi \to \mathrm{iEdg}\left(S\right)={I\upharpoonright }_{F\left[\left(0..^N\right)\right]}$$
9		eucrct2eupth1.h	$$⊢H=F\mathrm{prefix}N$$
10		eucrct2eupth1.q	$$⊢Q={P\upharpoonright }_{\left(0\dots N\right)}$$
11		eupthiswlk	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$
12		wlkcl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|\in {\mathbb{N}}_0$$
13		nn0z	$$⊢\left|F\right|\in {\mathbb{N}}_0\to \left|F\right|\in \mathbb{Z}$$
14	13	anim1i	$$⊢\left(\left|F\right|\in {\mathbb{N}}_0\wedge 0<\left|F\right|\right)\to \left(\left|F\right|\in \mathbb{Z}\wedge 0<\left|F\right|\right)$$
15		elnnz	$$⊢\left|F\right|\in \mathbb{N}\leftrightarrow \left(\left|F\right|\in \mathbb{Z}\wedge 0<\left|F\right|\right)$$
16	14 15	sylibr	$$⊢\left(\left|F\right|\in {\mathbb{N}}_0\wedge 0<\left|F\right|\right)\to \left|F\right|\in \mathbb{N}$$
17	16	ex	$$⊢\left|F\right|\in {\mathbb{N}}_0\to \left(0<\left|F\right|\to \left|F\right|\in \mathbb{N}\right)$$
18	3 11 12 17	4syl	$$⊢\phi \to \left(0<\left|F\right|\to \left|F\right|\in \mathbb{N}\right)$$
19	6 18	mpd	$$⊢\phi \to \left|F\right|\in \mathbb{N}$$
20		fzo0end	$$⊢\left|F\right|\in \mathbb{N}\to \left|F\right|-1\in \left(0..^\left|F\right|\right)$$
21	19 20	syl	$$⊢\phi \to \left|F\right|-1\in \left(0..^\left|F\right|\right)$$
22	7 21	eqeltrd	$$⊢\phi \to N\in \left(0..^\left|F\right|\right)$$
23	1 2 3 22 8 9 10 5	eupthres	$$⊢\phi \to H\mathrm{EulerPaths}\left(S\right)Q$$