gpg3nbgrvtx0ALT

Description: In a generalized Petersen graph G , every vertex of the first kind has exactly three (different) neighbors. (Contributed by AV, 30-Aug-2025) The proof of gpg3nbgrvtx0 can be shortened using lemma gpg3nbgrvtxlem , but then theorem 2ltceilhalf is required which is based on an "example" ex-ceil . If these theorems were moved to main, the "example" should also be moved up to become a full-fledged theorem. (Proof shortened by AV, 4-Sep-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	gpgnbgr.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
	gpgnbgr.g	No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
	gpgnbgr.v	$⊢ V = Vtx (G)$
	gpgnbgr.u	$⊢ U = G NeighbVtx X$
Assertion	gpg3nbgrvtx0ALT	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \|U\| = 3$

Proof

Step	Hyp	Ref	Expression
1		gpgnbgr.j	$⊢ J = (1 ..^⌈\frac{N}{2}⌉)$
2		gpgnbgr.g	Could not format G = ( N gPetersenGr K ) : No typesetting found for \|- G = ( N gPetersenGr K ) with typecode \|-
3		gpgnbgr.v	$⊢ V = Vtx (G)$
4		gpgnbgr.u	$⊢ U = G NeighbVtx X$
5	1 2 3 4	gpgnbgrvtx0	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to U = \{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}$
6	5	fveq2d	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \|U\| = \|\{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}\|$
7		0ne1	$⊢ 0 \neq 1$
8	7	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 0 \neq 1$
9	8	orcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (0 \neq 1 \lor (2^{nd} (X) + 1) \mod N \neq 2^{nd} (X))$
10		c0ex	$⊢ 0 \in V$
11		ovex	$⊢ (2^{nd} (X) + 1) \mod N \in V$
12	10 11	opthne	$⊢ ⟨0, (2^{nd} (X) + 1) \mod N⟩ \neq ⟨1, 2^{nd} (X)⟩ \leftrightarrow (0 \neq 1 \lor (2^{nd} (X) + 1) \mod N \neq 2^{nd} (X))$
13	9 12	sylibr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ⟨0, (2^{nd} (X) + 1) \mod N⟩ \neq ⟨1, 2^{nd} (X)⟩$
14		ax-1ne0	$⊢ 1 \neq 0$
15	14	a1i	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 1 \neq 0$
16	15	orcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (1 \neq 0 \lor 2^{nd} (X) \neq (2^{nd} (X) - 1) \mod N)$
17		1ex	$⊢ 1 \in V$
18		fvex	$⊢ 2^{nd} (X) \in V$
19	17 18	opthne	$⊢ ⟨1, 2^{nd} (X)⟩ \neq ⟨0, (2^{nd} (X) - 1) \mod N⟩ \leftrightarrow (1 \neq 0 \lor 2^{nd} (X) \neq (2^{nd} (X) - 1) \mod N)$
20	16 19	sylibr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ⟨1, 2^{nd} (X)⟩ \neq ⟨0, (2^{nd} (X) - 1) \mod N⟩$
21		simpll	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to N \in ℤ_{\geq 3}$
22		2z	$⊢ 2 \in ℤ$
23	22	a1i	$⊢ N \in ℤ_{\geq 3} \to 2 \in ℤ$
24		eluzelre	$⊢ N \in ℤ_{\geq 3} \to N \in ℝ$
25	24	rehalfcld	$⊢ N \in ℤ_{\geq 3} \to \frac{N}{2} \in ℝ$
26	25	ceilcld	$⊢ N \in ℤ_{\geq 3} \to ⌈\frac{N}{2}⌉ \in ℤ$
27		2ltceilhalf	$⊢ N \in ℤ_{\geq 3} \to 2 \leq ⌈\frac{N}{2}⌉$
28		eluz2	$⊢ ⌈\frac{N}{2}⌉ \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land ⌈\frac{N}{2}⌉ \in ℤ \land 2 \leq ⌈\frac{N}{2}⌉)$
29	23 26 27 28	syl3anbrc	$⊢ N \in ℤ_{\geq 3} \to ⌈\frac{N}{2}⌉ \in ℤ_{\geq 2}$
30	29	adantr	$⊢ (N \in ℤ_{\geq 3} \land K \in J) \to ⌈\frac{N}{2}⌉ \in ℤ_{\geq 2}$
31	30	adantr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ⌈\frac{N}{2}⌉ \in ℤ_{\geq 2}$
32		fzo1lb	$⊢ 1 \in (1 ..^⌈\frac{N}{2}⌉) \leftrightarrow ⌈\frac{N}{2}⌉ \in ℤ_{\geq 2}$
33	31 32	sylibr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 1 \in (1 ..^⌈\frac{N}{2}⌉)$
34		eqid	$⊢ (0 ..^N) = (0 ..^N)$
35	34 1 2 3	gpgvtxel2	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to 2^{nd} (X) \in (0 ..^N)$
36	35	adantrr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 2^{nd} (X) \in (0 ..^N)$
37		gpg3nbgrvtxlem	$⊢ (N \in ℤ_{\geq 3} \land 1 \in (1 ..^⌈\frac{N}{2}⌉) \land 2^{nd} (X) \in (0 ..^N)) \to (2^{nd} (X) + 1) \mod N \neq (2^{nd} (X) - 1) \mod N$
38	21 33 36 37	syl3anc	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (2^{nd} (X) + 1) \mod N \neq (2^{nd} (X) - 1) \mod N$
39	38	necomd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (2^{nd} (X) - 1) \mod N \neq (2^{nd} (X) + 1) \mod N$
40	39	olcd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (0 \neq 0 \lor (2^{nd} (X) - 1) \mod N \neq (2^{nd} (X) + 1) \mod N)$
41		ovex	$⊢ (2^{nd} (X) - 1) \mod N \in V$
42	10 41	opthne	$⊢ ⟨0, (2^{nd} (X) - 1) \mod N⟩ \neq ⟨0, (2^{nd} (X) + 1) \mod N⟩ \leftrightarrow (0 \neq 0 \lor (2^{nd} (X) - 1) \mod N \neq (2^{nd} (X) + 1) \mod N)$
43	40 42	sylibr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to ⟨0, (2^{nd} (X) - 1) \mod N⟩ \neq ⟨0, (2^{nd} (X) + 1) \mod N⟩$
44	13 20 43	3jca	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to (⟨0, (2^{nd} (X) + 1) \mod N⟩ \neq ⟨1, 2^{nd} (X)⟩ \land ⟨1, 2^{nd} (X)⟩ \neq ⟨0, (2^{nd} (X) - 1) \mod N⟩ \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \neq ⟨0, (2^{nd} (X) + 1) \mod N⟩)$
45		opex	$⊢ ⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V$
46		opex	$⊢ ⟨1, 2^{nd} (X)⟩ \in V$
47		opex	$⊢ ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V$
48		hashtpg	$⊢ (⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V \land ⟨1, 2^{nd} (X)⟩ \in V \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V) \to ((⟨0, (2^{nd} (X) + 1) \mod N⟩ \neq ⟨1, 2^{nd} (X)⟩ \land ⟨1, 2^{nd} (X)⟩ \neq ⟨0, (2^{nd} (X) - 1) \mod N⟩ \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \neq ⟨0, (2^{nd} (X) + 1) \mod N⟩) \leftrightarrow \|\{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}\| = 3)$
49	45 46 47 48	mp3an	$⊢ (⟨0, (2^{nd} (X) + 1) \mod N⟩ \neq ⟨1, 2^{nd} (X)⟩ \land ⟨1, 2^{nd} (X)⟩ \neq ⟨0, (2^{nd} (X) - 1) \mod N⟩ \land ⟨0, (2^{nd} (X) - 1) \mod N⟩ \neq ⟨0, (2^{nd} (X) + 1) \mod N⟩) \leftrightarrow \|\{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}\| = 3$
50	44 49	sylib	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \|\{⟨0, (2^{nd} (X) + 1) \mod N⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod N⟩\}\| = 3$
51	6 50	eqtrd	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to \|U\| = 3$

Metamath Proof Explorer

Theorem gpg3nbgrvtx0ALT

Proof