Theorem 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 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 ..^ ( |^ ` ( N / 2 ) ) )
	gpgnbgr.g	|- G = ( N gPetersenGr K )
	gpgnbgr.v	|- V = ( Vtx ` G )
	gpgnbgr.u	|- U = ( G NeighbVtx X )
Assertion	gpg3nbgrvtx0ALT	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( # ` U ) = 3 )

Proof

Step	Hyp	Ref	Expression
1		gpgnbgr.j	|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2		gpgnbgr.g	|- G = ( N gPetersenGr K )
3		gpgnbgr.v	|- V = ( Vtx ` G )
4		gpgnbgr.u	|- U = ( G NeighbVtx X )
5	1 2 3 4	gpgnbgrvtx0	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> U = { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } )
6	5	fveq2d	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( # ` U ) = ( # ` { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } ) )
7		0ne1	|- 0 =/= 1
8	7	a1i	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> 0 =/= 1 )
9	8	orcd	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( 0 =/= 1 \/ ( ( ( 2nd ` X ) + 1 ) mod N ) =/= ( 2nd ` X ) ) )
10		c0ex	|- 0 e. _V
11		ovex	|- ( ( ( 2nd ` X ) + 1 ) mod N ) e. _V
12	10 11	opthne	|- ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. =/= <. 1 , ( 2nd ` X ) >. <-> ( 0 =/= 1 \/ ( ( ( 2nd ` X ) + 1 ) mod N ) =/= ( 2nd ` X ) ) )
13	9 12	sylibr	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. =/= <. 1 , ( 2nd ` X ) >. )
14		ax-1ne0	|- 1 =/= 0
15	14	a1i	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> 1 =/= 0 )
16	15	orcd	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( 1 =/= 0 \/ ( 2nd ` X ) =/= ( ( ( 2nd ` X ) - 1 ) mod N ) ) )
17		1ex	|- 1 e. _V
18		fvex	|- ( 2nd ` X ) e. _V
19	17 18	opthne	|- ( <. 1 , ( 2nd ` X ) >. =/= <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. <-> ( 1 =/= 0 \/ ( 2nd ` X ) =/= ( ( ( 2nd ` X ) - 1 ) mod N ) ) )
20	16 19	sylibr	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> <. 1 , ( 2nd ` X ) >. =/= <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. )
21		simpll	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> N e. ( ZZ>= ` 3 ) )
22		2z	|- 2 e. ZZ
23	22	a1i	|- ( N e. ( ZZ>= ` 3 ) -> 2 e. ZZ )
24		eluzelre	|- ( N e. ( ZZ>= ` 3 ) -> N e. RR )
25	24	rehalfcld	|- ( N e. ( ZZ>= ` 3 ) -> ( N / 2 ) e. RR )
26	25	ceilcld	|- ( N e. ( ZZ>= ` 3 ) -> ( |^ ` ( N / 2 ) ) e. ZZ )
27		2ltceilhalf	|- ( N e. ( ZZ>= ` 3 ) -> 2 <_ ( |^ ` ( N / 2 ) ) )
28		eluz2	|- ( ( |^ ` ( N / 2 ) ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ( |^ ` ( N / 2 ) ) e. ZZ /\ 2 <_ ( |^ ` ( N / 2 ) ) ) )
29	23 26 27 28	syl3anbrc	|- ( N e. ( ZZ>= ` 3 ) -> ( |^ ` ( N / 2 ) ) e. ( ZZ>= ` 2 ) )
30	29	adantr	|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( |^ ` ( N / 2 ) ) e. ( ZZ>= ` 2 ) )
31	30	adantr	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( |^ ` ( N / 2 ) ) e. ( ZZ>= ` 2 ) )
32		fzo1lb	|- ( 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) <-> ( |^ ` ( N / 2 ) ) e. ( ZZ>= ` 2 ) )
33	31 32	sylibr	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
34		eqid	|- ( 0 ..^ N ) = ( 0 ..^ N )
35	34 1 2 3	gpgvtxel2	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> ( 2nd ` X ) e. ( 0 ..^ N ) )
36	35	adantrr	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( 2nd ` X ) e. ( 0 ..^ N ) )
37		gpg3nbgrvtxlem	|- ( ( N e. ( ZZ>= ` 3 ) /\ 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) /\ ( 2nd ` X ) e. ( 0 ..^ N ) ) -> ( ( ( 2nd ` X ) + 1 ) mod N ) =/= ( ( ( 2nd ` X ) - 1 ) mod N ) )
38	21 33 36 37	syl3anc	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( 2nd ` X ) + 1 ) mod N ) =/= ( ( ( 2nd ` X ) - 1 ) mod N ) )
39	38	necomd	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( 2nd ` X ) - 1 ) mod N ) =/= ( ( ( 2nd ` X ) + 1 ) mod N ) )
40	39	olcd	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( 0 =/= 0 \/ ( ( ( 2nd ` X ) - 1 ) mod N ) =/= ( ( ( 2nd ` X ) + 1 ) mod N ) ) )
41		ovex	|- ( ( ( 2nd ` X ) - 1 ) mod N ) e. _V
42	10 41	opthne	|- ( <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. =/= <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. <-> ( 0 =/= 0 \/ ( ( ( 2nd ` X ) - 1 ) mod N ) =/= ( ( ( 2nd ` X ) + 1 ) mod N ) ) )
43	40 42	sylibr	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. =/= <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. )
44	13 20 43	3jca	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. =/= <. 1 , ( 2nd ` X ) >. /\ <. 1 , ( 2nd ` X ) >. =/= <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. /\ <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. =/= <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. ) )
45		opex	|- <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. _V
46		opex	|- <. 1 , ( 2nd ` X ) >. e. _V
47		opex	|- <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. _V
48		hashtpg	|- ( ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. _V /\ <. 1 , ( 2nd ` X ) >. e. _V /\ <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. _V ) -> ( ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. =/= <. 1 , ( 2nd ` X ) >. /\ <. 1 , ( 2nd ` X ) >. =/= <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. /\ <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. =/= <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. ) <-> ( # ` { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } ) = 3 ) )
49	45 46 47 48	mp3an	|- ( ( <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. =/= <. 1 , ( 2nd ` X ) >. /\ <. 1 , ( 2nd ` X ) >. =/= <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. /\ <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. =/= <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. ) <-> ( # ` { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } ) = 3 )
50	44 49	sylib	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( # ` { <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. , <. 1 , ( 2nd ` X ) >. , <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. } ) = 3 )
51	6 50	eqtrd	|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( # ` U ) = 3 )