Theorem gpgedgvtx1lem

Description: Lemma for gpgedgvtx1 . (Contributed by AV, 1-Sep-2025) (Proof shortened by AV, 8-Sep-2025)

	Ref	Expression
Hypotheses	ceilhalfelfzo1.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
	gpgedgvtx1lem.i	$$⊢I=\left(0..^N\right)$$
Assertion	gpgedgvtx1lem	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X\in J\right)\to X\in I$$

Proof

Step	Hyp	Ref	Expression
1		ceilhalfelfzo1.j	$$⊢J=\left(1..^⌈\frac{N}{2}⌉\right)$$
2		gpgedgvtx1lem.i	$$⊢I=\left(0..^N\right)$$
3		fzo0ss1	$$⊢\left(1..^N\right)\subseteq \left(0..^N\right)$$
4	3	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(1..^N\right)\subseteq \left(0..^N\right)$$
5	4 2	sseqtrrdi	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(1..^N\right)\subseteq I$$
6	5	adantr	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X\in J\right)\to \left(1..^N\right)\subseteq I$$
7		eluzge3nn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{N}$$
8	1	ceilhalfelfzo1	$$⊢N\in \mathbb{N}\to \left(X\in J\to X\in \left(1..^N\right)\right)$$
9	7 8	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(X\in J\to X\in \left(1..^N\right)\right)$$
10	9	imp	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X\in J\right)\to X\in \left(1..^N\right)$$
11	6 10	sseldd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge X\in J\right)\to X\in I$$