Theorem gpgedgvtx1lem

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

	Ref	Expression
Hypotheses	ceilhalfelfzo1.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	gpgedgvtx1lem.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion	gpgedgvtx1lem	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ 𝐽 ) → 𝑋 ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		ceilhalfelfzo1.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2		gpgedgvtx1lem.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
3		fzo0ss1	⊢ ( 1 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 )
4	3	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 1 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) )
5	4 2	sseqtrrdi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 1 ..^ 𝑁 ) ⊆ 𝐼 )
6	5	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ 𝐽 ) → ( 1 ..^ 𝑁 ) ⊆ 𝐼 )
7		eluzge3nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
8	1	ceilhalfelfzo1	⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ 𝐽 → 𝑋 ∈ ( 1 ..^ 𝑁 ) ) )
9	7 8	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑋 ∈ 𝐽 → 𝑋 ∈ ( 1 ..^ 𝑁 ) ) )
10	9	imp	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ 𝐽 ) → 𝑋 ∈ ( 1 ..^ 𝑁 ) )
11	6 10	sseldd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑋 ∈ 𝐽 ) → 𝑋 ∈ 𝐼 )