Metamath Proof Explorer

Theorem gpg3nbgrvtx0

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

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 gpg3nbgrvtx0 
|- ( ( ( 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 simpl 
 |-  ( ( X e. V /\ ( 1st ` X ) = 0 ) -> X e. V )
22 21 anim2i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) )
23 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
24 23 1 2 3 gpgvtxel2 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ X e. V ) -> ( 2nd ` X ) e. ( 0 ..^ N ) )
25 elfzoelz 
 |-  ( ( 2nd ` X ) e. ( 0 ..^ N ) -> ( 2nd ` X ) e. ZZ )
26 22 24 25 3syl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( 2nd ` X ) e. ZZ )
27 26 zcnd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( 2nd ` X ) e. CC )
28 1cnd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> 1 e. CC )
29 2cnd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> 2 e. CC )
30 27 28 29 subadd23d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( 2nd ` X ) - 1 ) + 2 ) = ( ( 2nd ` X ) + ( 2 - 1 ) ) )
31 2m1e1 
 |-  ( 2 - 1 ) = 1
32 31 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( 2 - 1 ) = 1 )
33 32 oveq2d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( 2nd ` X ) + ( 2 - 1 ) ) = ( ( 2nd ` X ) + 1 ) )
34 30 33 eqtrd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( 2nd ` X ) - 1 ) + 2 ) = ( ( 2nd ` X ) + 1 ) )
35 34 eqcomd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( 2nd ` X ) + 1 ) = ( ( ( 2nd ` X ) - 1 ) + 2 ) )
36 35 oveq1d 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( 2nd ` X ) + 1 ) mod N ) = ( ( ( ( 2nd ` X ) - 1 ) + 2 ) mod N ) )
37 1zzd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> 1 e. ZZ )
38 26 37 zsubcld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( 2nd ` X ) - 1 ) e. ZZ )
39 38 zred 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( 2nd ` X ) - 1 ) e. RR )
40 2re 
 |-  2 e. RR
41 40 a1i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> 2 e. RR )
42 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
43 42 nnrpd 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. RR+ )
44 43 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> N e. RR+ )
45 modaddabs 
 |-  ( ( ( ( 2nd ` X ) - 1 ) e. RR /\ 2 e. RR /\ N e. RR+ ) -> ( ( ( ( ( 2nd ` X ) - 1 ) mod N ) + ( 2 mod N ) ) mod N ) = ( ( ( ( 2nd ` X ) - 1 ) + 2 ) mod N ) )
46 39 41 44 45 syl3anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( ( ( 2nd ` X ) - 1 ) mod N ) + ( 2 mod N ) ) mod N ) = ( ( ( ( 2nd ` X ) - 1 ) + 2 ) mod N ) )
47 46 eqcomd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( ( 2nd ` X ) - 1 ) + 2 ) mod N ) = ( ( ( ( ( 2nd ` X ) - 1 ) mod N ) + ( 2 mod N ) ) mod N ) )
48 36 47 eqtrd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( 2nd ` X ) + 1 ) mod N ) = ( ( ( ( ( 2nd ` X ) - 1 ) mod N ) + ( 2 mod N ) ) mod N ) )
49 42 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> N e. NN )
50 38 49 zmodcld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( 2nd ` X ) - 1 ) mod N ) e. NN0 )
51 modlt 
 |-  ( ( ( ( 2nd ` X ) - 1 ) e. RR /\ N e. RR+ ) -> ( ( ( 2nd ` X ) - 1 ) mod N ) < N )
52 39 44 51 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( 2nd ` X ) - 1 ) mod N ) < N )
53 50 52 jca 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( ( 2nd ` X ) - 1 ) mod N ) e. NN0 /\ ( ( ( 2nd ` X ) - 1 ) mod N ) < N ) )
54 2nn0 
 |-  2 e. NN0
55 54 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 e. NN0 )
56 eluz2 
 |-  ( N e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) )
57 40 a1i 
 |-  ( ( N e. ZZ /\ 3 <_ N ) -> 2 e. RR )
58 3re 
 |-  3 e. RR
59 58 a1i 
 |-  ( ( N e. ZZ /\ 3 <_ N ) -> 3 e. RR )
60 zre 
 |-  ( N e. ZZ -> N e. RR )
61 60 adantr 
 |-  ( ( N e. ZZ /\ 3 <_ N ) -> N e. RR )
62 2lt3 
 |-  2 < 3
63 62 a1i 
 |-  ( ( N e. ZZ /\ 3 <_ N ) -> 2 < 3 )
64 simpr 
 |-  ( ( N e. ZZ /\ 3 <_ N ) -> 3 <_ N )
65 57 59 61 63 64 ltletrd 
 |-  ( ( N e. ZZ /\ 3 <_ N ) -> 2 < N )
66 65 3adant1 
 |-  ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 2 < N )
67 56 66 sylbi 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 < N )
68 elfzo0 
 |-  ( 2 e. ( 0 ..^ N ) <-> ( 2 e. NN0 /\ N e. NN /\ 2 < N ) )
69 55 42 67 68 syl3anbrc 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 e. ( 0 ..^ N ) )
70 zmodidfzoimp 
 |-  ( 2 e. ( 0 ..^ N ) -> ( 2 mod N ) = 2 )
71 69 70 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 2 mod N ) = 2 )
72 2nn 
 |-  2 e. NN
73 71 72 eqeltrdi 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 2 mod N ) e. NN )
74 40 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 e. RR )
75 modlt 
 |-  ( ( 2 e. RR /\ N e. RR+ ) -> ( 2 mod N ) < N )
76 74 43 75 syl2anc 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 2 mod N ) < N )
77 73 76 jca 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( 2 mod N ) e. NN /\ ( 2 mod N ) < N ) )
78 77 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( 2 mod N ) e. NN /\ ( 2 mod N ) < N ) )
79 addmodne 
 |-  ( ( N e. NN /\ ( ( ( ( 2nd ` X ) - 1 ) mod N ) e. NN0 /\ ( ( ( 2nd ` X ) - 1 ) mod N ) < N ) /\ ( ( 2 mod N ) e. NN /\ ( 2 mod N ) < N ) ) -> ( ( ( ( ( 2nd ` X ) - 1 ) mod N ) + ( 2 mod N ) ) mod N ) =/= ( ( ( 2nd ` X ) - 1 ) mod N ) )
80 49 53 78 79 syl3anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( ( ( 2nd ` X ) - 1 ) mod N ) + ( 2 mod N ) ) mod N ) =/= ( ( ( 2nd ` X ) - 1 ) mod N ) )
81 48 80 eqnetrd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( 2nd ` X ) + 1 ) mod N ) =/= ( ( ( 2nd ` X ) - 1 ) mod N ) )
82 81 necomd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( ( ( 2nd ` X ) - 1 ) mod N ) =/= ( ( ( 2nd ` X ) + 1 ) mod N ) )
83 82 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 ) ) )
84 ovex 
 |-  ( ( ( 2nd ` X ) - 1 ) mod N ) e. _V
85 10 84 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 ) ) )
86 83 85 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 ) >. )
87 13 20 86 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 ) >. ) )
88 opex 
 |-  <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. e. _V
89 opex 
 |-  <. 1 , ( 2nd ` X ) >. e. _V
90 opex 
 |-  <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. e. _V
91 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 ) )
92 88 89 90 91 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 )
93 87 92 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 )
94 6 93 eqtrd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. V /\ ( 1st ` X ) = 0 ) ) -> ( # ` U ) = 3 )