Theorem 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	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	gpgnbgr.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
	gpgnbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	gpgnbgr.u	⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
Assertion	gpg3nbgrvtx0ALT	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ 𝑈 ) = 3 )

Proof

Step	Hyp	Ref	Expression
1		gpgnbgr.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2		gpgnbgr.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
3		gpgnbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4		gpgnbgr.u	⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
5	1 2 3 4	gpgnbgrvtx0	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → 𝑈 = { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } )
6	5	fveq2d	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) )
7		0ne1	⊢ 0 ≠ 1
8	7	a1i	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → 0 ≠ 1 )
9	8	orcd	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( 0 ≠ 1 ∨ ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ≠ ( 2nd ‘ 𝑋 ) ) )
10		c0ex	⊢ 0 ∈ V
11		ovex	⊢ ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ∈ V
12	10 11	opthne	⊢ ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ↔ ( 0 ≠ 1 ∨ ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ≠ ( 2nd ‘ 𝑋 ) ) )
13	9 12	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ )
14		ax-1ne0	⊢ 1 ≠ 0
15	14	a1i	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → 1 ≠ 0 )
16	15	orcd	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( 1 ≠ 0 ∨ ( 2nd ‘ 𝑋 ) ≠ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ) )
17		1ex	⊢ 1 ∈ V
18		fvex	⊢ ( 2nd ‘ 𝑋 ) ∈ V
19	17 18	opthne	⊢ ( ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ↔ ( 1 ≠ 0 ∨ ( 2nd ‘ 𝑋 ) ≠ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ) )
20	16 19	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ )
21		simpll	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
22		2z	⊢ 2 ∈ ℤ
23	22	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℤ )
24		eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℝ )
25	24	rehalfcld	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 / 2 ) ∈ ℝ )
26	25	ceilcld	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
27		2ltceilhalf	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
28		eluz2	⊢ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ∧ 2 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
29	23 26 27 28	syl3anbrc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ( ℤ≥ ‘ 2 ) )
30	29	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ( ℤ≥ ‘ 2 ) )
31	30	adantr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ( ℤ≥ ‘ 2 ) )
32		fzo1lb	⊢ ( 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ↔ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ( ℤ≥ ‘ 2 ) )
33	31 32	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
34		eqid	⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
35	34 1 2 3	gpgvtxel2	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) )
36	35	adantrr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) )
37		gpg3nbgrvtxlem	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ∧ ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) )
38	21 33 36 37	syl3anc	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) )
39	38	necomd	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) )
40	39	olcd	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( 0 ≠ 0 ∨ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ) )
41		ovex	⊢ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ∈ V
42	10 41	opthne	⊢ ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ↔ ( 0 ≠ 0 ∨ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ) )
43	40 42	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ )
44	13 20 43	3jca	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∧ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ) )
45		opex	⊢ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ V
46		opex	⊢ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∈ V
47		opex	⊢ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ V
48		hashtpg	⊢ ( ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ V ∧ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∈ V ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ V ) → ( ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∧ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ) ↔ ( ♯ ‘ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) = 3 ) )
49	45 46 47 48	mp3an	⊢ ( ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∧ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ) ↔ ( ♯ ‘ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) = 3 )
50	44 49	sylib	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) = 3 )
51	6 50	eqtrd	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ 𝑈 ) = 3 )