gpg3nbgrvtx0ALT

Description: In a generalized Petersen graph G , every outside vertex has exactly three (different) neighbors. (Contributed by AV, 30-Aug-2025)

The proof of gpg3nbgrvtx0 can be shortened using modmknepk , 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		eqid	$⊢ (0 ..^N) = (0 ..^N)$
23	22 1 2 3	gpgvtxel2	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land X \in V) \to 2^{nd} (X) \in (0 ..^N)$
24	23	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)$
25		2z	$⊢ 2 \in ℤ$
26	25	a1i	$⊢ N \in ℤ_{\geq 3} \to 2 \in ℤ$
27		eluzelre	$⊢ N \in ℤ_{\geq 3} \to N \in ℝ$
28	27	rehalfcld	$⊢ N \in ℤ_{\geq 3} \to \frac{N}{2} \in ℝ$
29	28	ceilcld	$⊢ N \in ℤ_{\geq 3} \to ⌈\frac{N}{2}⌉ \in ℤ$
30		2ltceilhalf	$⊢ N \in ℤ_{\geq 3} \to 2 \leq ⌈\frac{N}{2}⌉$
31		eluz2	$⊢ ⌈\frac{N}{2}⌉ \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land ⌈\frac{N}{2}⌉ \in ℤ \land 2 \leq ⌈\frac{N}{2}⌉)$
32	26 29 30 31	syl3anbrc	$⊢ N \in ℤ_{\geq 3} \to ⌈\frac{N}{2}⌉ \in ℤ_{\geq 2}$
33		fzo1lb	$⊢ 1 \in (1 ..^⌈\frac{N}{2}⌉) \leftrightarrow ⌈\frac{N}{2}⌉ \in ℤ_{\geq 2}$
34	32 33	sylibr	$⊢ N \in ℤ_{\geq 3} \to 1 \in (1 ..^⌈\frac{N}{2}⌉)$
35	34	ad2antrr	$⊢ ((N \in ℤ_{\geq 3} \land K \in J) \land (X \in V \land 1^{st} (X) = 0)) \to 1 \in (1 ..^⌈\frac{N}{2}⌉)$
36		eqid	$⊢ (1 ..^⌈\frac{N}{2}⌉) = (1 ..^⌈\frac{N}{2}⌉)$
37	36 22	modmknepk	$⊢ (N \in ℤ_{\geq 3} \land 2^{nd} (X) \in (0 ..^N) \land 1 \in (1 ..^⌈\frac{N}{2}⌉)) \to (2^{nd} (X) - 1) \mod N \neq (2^{nd} (X) + 1) \mod N$
38	21 24 35 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	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)$
40		ovex	$⊢ (2^{nd} (X) - 1) \mod N \in V$
41	10 40	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)$
42	39 41	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⟩$
43	13 20 42	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⟩)$
44		opex	$⊢ ⟨0, (2^{nd} (X) + 1) \mod N⟩ \in V$
45		opex	$⊢ ⟨1, 2^{nd} (X)⟩ \in V$
46		opex	$⊢ ⟨0, (2^{nd} (X) - 1) \mod N⟩ \in V$
47		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)$
48	44 45 46 47	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$
49	43 48	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$
50	6 49	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