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 = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
	gpgedgvtx1lem.i	|- I = ( 0 ..^ N )
Assertion	gpgedgvtx1lem	|- ( ( N e. ( ZZ>= ` 3 ) /\ X e. J ) -> X e. I )

Proof

Step	Hyp	Ref	Expression
1		ceilhalfelfzo1.j	|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2		gpgedgvtx1lem.i	|- I = ( 0 ..^ N )
3		fzo0ss1	|- ( 1 ..^ N ) C_ ( 0 ..^ N )
4	3	a1i	|- ( N e. ( ZZ>= ` 3 ) -> ( 1 ..^ N ) C_ ( 0 ..^ N ) )
5	4 2	sseqtrrdi	|- ( N e. ( ZZ>= ` 3 ) -> ( 1 ..^ N ) C_ I )
6	5	adantr	|- ( ( N e. ( ZZ>= ` 3 ) /\ X e. J ) -> ( 1 ..^ N ) C_ I )
7		eluzge3nn	|- ( N e. ( ZZ>= ` 3 ) -> N e. NN )
8	1	ceilhalfelfzo1	|- ( N e. NN -> ( X e. J -> X e. ( 1 ..^ N ) ) )
9	7 8	syl	|- ( N e. ( ZZ>= ` 3 ) -> ( X e. J -> X e. ( 1 ..^ N ) ) )
10	9	imp	|- ( ( N e. ( ZZ>= ` 3 ) /\ X e. J ) -> X e. ( 1 ..^ N ) )
11	6 10	sseldd	|- ( ( N e. ( ZZ>= ` 3 ) /\ X e. J ) -> X e. I )