Theorem pglem

Description: Lemma for theorems about Petersen graphs. (Contributed by AV, 10-Nov-2025)

	Ref	Expression
Assertion	pglem	$$⊢2\in \left(1..^⌈\frac{5}{2}⌉\right)$$

Proof

Step	Hyp	Ref	Expression
1		2ex	$$⊢2\in \mathrm{V}$$
2	1	prid2	$$⊢2\in \left\{1,2\right\}$$
3		fzo13pr	$$⊢\left(1..^3\right)=\left\{1,2\right\}$$
4	2 3	eleqtrri	$$⊢2\in \left(1..^3\right)$$
5		ceil5half3	$$⊢⌈\frac{5}{2}⌉=3$$
6	5	oveq2i	$$⊢\left(1..^⌈\frac{5}{2}⌉\right)=\left(1..^3\right)$$
7	4 6	eleqtrri	$$⊢2\in \left(1..^⌈\frac{5}{2}⌉\right)$$