Metamath Proof Explorer

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 
|- 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 )