Metamath Proof Explorer

Theorem gpg3kgrtriex

Description: All generalized Petersen graphs G(N,K) with N = 3 x. K contain triangles. (Contributed by AV, 1-Oct-2025)

Ref Expression
Hypotheses gpg3kgrtriex.n 
|- N = ( 3 x. K )
gpg3kgrtriex.g 
|- G = ( N gPetersenGr K )
Assertion gpg3kgrtriex 
|- ( K e. NN -> E. t t e. ( GrTriangles ` G ) )

Proof

Step Hyp Ref Expression
1 gpg3kgrtriex.n 
 |-  N = ( 3 x. K )
2 gpg3kgrtriex.g 
 |-  G = ( N gPetersenGr K )
3 1elpr01 
 |-  1 e. { 0 , 1 }
4 3 a1i 
 |-  ( K e. NN -> 1 e. { 0 , 1 } )
5 3nn 
 |-  3 e. NN
6 5 a1i 
 |-  ( K e. NN -> 3 e. NN )
7 id 
 |-  ( K e. NN -> K e. NN )
8 6 7 nnmulcld 
 |-  ( K e. NN -> ( 3 x. K ) e. NN )
9 1 8 eqeltrid 
 |-  ( K e. NN -> N e. NN )
10 lbfzo0 
 |-  ( 0 e. ( 0 ..^ N ) <-> N e. NN )
11 9 10 sylibr 
 |-  ( K e. NN -> 0 e. ( 0 ..^ N ) )
12 4 11 opelxpd 
 |-  ( K e. NN -> <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
13 1 gpg3kgrtriexlem4 
 |-  ( K e. NN -> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
14 9 13 jca 
 |-  ( K e. NN -> ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) )
15 eqid 
 |-  ( 1 ..^ ( |^ ` ( N / 2 ) ) ) = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
16 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
17 15 16 gpgvtx 
 |-  ( ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) )
18 17 eleq2d 
 |-  ( ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( <. 1 , 0 >. e. ( Vtx ` ( N gPetersenGr K ) ) <-> <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
19 14 18 syl 
 |-  ( K e. NN -> ( <. 1 , 0 >. e. ( Vtx ` ( N gPetersenGr K ) ) <-> <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
20 12 19 mpbird 
 |-  ( K e. NN -> <. 1 , 0 >. e. ( Vtx ` ( N gPetersenGr K ) ) )
21 2 fveq2i 
 |-  ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) )
22 20 21 eleqtrrdi 
 |-  ( K e. NN -> <. 1 , 0 >. e. ( Vtx ` G ) )
23 oveq2 
 |-  ( a = <. 1 , 0 >. -> ( G NeighbVtx a ) = ( G NeighbVtx <. 1 , 0 >. ) )
24 biidd 
 |-  ( a = <. 1 , 0 >. -> ( ( b =/= c /\ { b , c } e. ( Edg ` G ) ) <-> ( b =/= c /\ { b , c } e. ( Edg ` G ) ) ) )
25 23 24 rexeqbidv 
 |-  ( a = <. 1 , 0 >. -> ( E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) <-> E. c e. ( G NeighbVtx <. 1 , 0 >. ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) ) )
26 23 25 rexeqbidv 
 |-  ( a = <. 1 , 0 >. -> ( E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) <-> E. b e. ( G NeighbVtx <. 1 , 0 >. ) E. c e. ( G NeighbVtx <. 1 , 0 >. ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) ) )
27 26 adantl 
 |-  ( ( K e. NN /\ a = <. 1 , 0 >. ) -> ( E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) <-> E. b e. ( G NeighbVtx <. 1 , 0 >. ) E. c e. ( G NeighbVtx <. 1 , 0 >. ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) ) )
28 1 gpg3kgrtriexlem3 
 |-  ( K e. NN -> N e. ( ZZ>= ` 3 ) )
29 eqid 
 |-  1 = 1
30 29 a1i 
 |-  ( K e. NN -> 1 = 1 )
31 30 olcd 
 |-  ( K e. NN -> ( 1 = 0 \/ 1 = 1 ) )
32 31 11 jca 
 |-  ( K e. NN -> ( ( 1 = 0 \/ 1 = 1 ) /\ 0 e. ( 0 ..^ N ) ) )
33 28 13 jca 
 |-  ( K e. NN -> ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) )
34 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
35 16 15 2 34 opgpgvtx 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( <. 1 , 0 >. e. ( Vtx ` G ) <-> ( ( 1 = 0 \/ 1 = 1 ) /\ 0 e. ( 0 ..^ N ) ) ) )
36 33 35 syl 
 |-  ( K e. NN -> ( <. 1 , 0 >. e. ( Vtx ` G ) <-> ( ( 1 = 0 \/ 1 = 1 ) /\ 0 e. ( 0 ..^ N ) ) ) )
37 32 36 mpbird 
 |-  ( K e. NN -> <. 1 , 0 >. e. ( Vtx ` G ) )
38 1ex 
 |-  1 e. _V
39 c0ex 
 |-  0 e. _V
40 38 39 op1st 
 |-  ( 1st ` <. 1 , 0 >. ) = 1
41 40 a1i 
 |-  ( K e. NN -> ( 1st ` <. 1 , 0 >. ) = 1 )
42 eqid 
 |-  ( G NeighbVtx <. 1 , 0 >. ) = ( G NeighbVtx <. 1 , 0 >. )
43 15 2 34 42 gpgnbgrvtx1 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) /\ ( <. 1 , 0 >. e. ( Vtx ` G ) /\ ( 1st ` <. 1 , 0 >. ) = 1 ) ) -> ( G NeighbVtx <. 1 , 0 >. ) = { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } )
44 28 13 37 41 43 syl22anc 
 |-  ( K e. NN -> ( G NeighbVtx <. 1 , 0 >. ) = { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } )
45 neeq1 
 |-  ( b = <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. -> ( b =/= c <-> <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. =/= c ) )
46 preq1 
 |-  ( b = <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. -> { b , c } = { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , c } )
47 46 eleq1d 
 |-  ( b = <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. -> ( { b , c } e. ( Edg ` G ) <-> { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , c } e. ( Edg ` G ) ) )
48 45 47 anbi12d 
 |-  ( b = <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. -> ( ( b =/= c /\ { b , c } e. ( Edg ` G ) ) <-> ( <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. =/= c /\ { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , c } e. ( Edg ` G ) ) ) )
49 neeq2 
 |-  ( c = <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. -> ( <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. =/= c <-> <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. =/= <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. ) )
50 preq2 
 |-  ( c = <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. -> { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , c } = { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } )
51 50 eleq1d 
 |-  ( c = <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. -> ( { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , c } e. ( Edg ` G ) <-> { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } e. ( Edg ` G ) ) )
52 49 51 anbi12d 
 |-  ( c = <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. -> ( ( <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. =/= c /\ { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , c } e. ( Edg ` G ) ) <-> ( <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. =/= <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. /\ { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } e. ( Edg ` G ) ) ) )
53 opex 
 |-  <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. e. _V
54 53 tpid1 
 |-  <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. e. { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. }
55 eleq2 
 |-  ( ( G NeighbVtx <. 1 , 0 >. ) = { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } -> ( <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. e. ( G NeighbVtx <. 1 , 0 >. ) <-> <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. e. { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } ) )
56 55 adantl 
 |-  ( ( K e. NN /\ ( G NeighbVtx <. 1 , 0 >. ) = { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } ) -> ( <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. e. ( G NeighbVtx <. 1 , 0 >. ) <-> <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. e. { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } ) )
57 54 56 mpbiri 
 |-  ( ( K e. NN /\ ( G NeighbVtx <. 1 , 0 >. ) = { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } ) -> <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. e. ( G NeighbVtx <. 1 , 0 >. ) )
58 opex 
 |-  <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. e. _V
59 58 tpid3 
 |-  <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. e. { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. }
60 eleq2 
 |-  ( ( G NeighbVtx <. 1 , 0 >. ) = { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } -> ( <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. e. ( G NeighbVtx <. 1 , 0 >. ) <-> <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. e. { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } ) )
61 60 adantl 
 |-  ( ( K e. NN /\ ( G NeighbVtx <. 1 , 0 >. ) = { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } ) -> ( <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. e. ( G NeighbVtx <. 1 , 0 >. ) <-> <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. e. { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } ) )
62 59 61 mpbiri 
 |-  ( ( K e. NN /\ ( G NeighbVtx <. 1 , 0 >. ) = { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } ) -> <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. e. ( G NeighbVtx <. 1 , 0 >. ) )
63 1 gpg3kgrtriexlem5 
 |-  ( K e. NN -> ( K mod N ) =/= ( -u K mod N ) )
64 38 39 op2nd 
 |-  ( 2nd ` <. 1 , 0 >. ) = 0
65 64 oveq1i 
 |-  ( ( 2nd ` <. 1 , 0 >. ) + K ) = ( 0 + K )
66 nncn 
 |-  ( K e. NN -> K e. CC )
67 66 addlidd 
 |-  ( K e. NN -> ( 0 + K ) = K )
68 65 67 eqtrid 
 |-  ( K e. NN -> ( ( 2nd ` <. 1 , 0 >. ) + K ) = K )
69 68 oveq1d 
 |-  ( K e. NN -> ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) = ( K mod N ) )
70 64 oveq1i 
 |-  ( ( 2nd ` <. 1 , 0 >. ) - K ) = ( 0 - K )
71 70 a1i 
 |-  ( K e. NN -> ( ( 2nd ` <. 1 , 0 >. ) - K ) = ( 0 - K ) )
72 df-neg 
 |-  -u K = ( 0 - K )
73 71 72 eqtr4di 
 |-  ( K e. NN -> ( ( 2nd ` <. 1 , 0 >. ) - K ) = -u K )
74 73 oveq1d 
 |-  ( K e. NN -> ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) = ( -u K mod N ) )
75 63 69 74 3netr4d 
 |-  ( K e. NN -> ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) =/= ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) )
76 75 olcd 
 |-  ( K e. NN -> ( 1 =/= 1 \/ ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) =/= ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) ) )
77 ovex 
 |-  ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) e. _V
78 38 77 opthne 
 |-  ( <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. =/= <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. <-> ( 1 =/= 1 \/ ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) =/= ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) ) )
79 76 78 sylibr 
 |-  ( K e. NN -> <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. =/= <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. )
80 64 a1i 
 |-  ( K e. NN -> ( 2nd ` <. 1 , 0 >. ) = 0 )
81 80 oveq1d 
 |-  ( K e. NN -> ( ( 2nd ` <. 1 , 0 >. ) + K ) = ( 0 + K ) )
82 81 67 eqtrd 
 |-  ( K e. NN -> ( ( 2nd ` <. 1 , 0 >. ) + K ) = K )
83 82 oveq1d 
 |-  ( K e. NN -> ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) = ( K mod N ) )
84 83 opeq2d 
 |-  ( K e. NN -> <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. = <. 1 , ( K mod N ) >. )
85 80 oveq1d 
 |-  ( K e. NN -> ( ( 2nd ` <. 1 , 0 >. ) - K ) = ( 0 - K ) )
86 85 72 eqtr4di 
 |-  ( K e. NN -> ( ( 2nd ` <. 1 , 0 >. ) - K ) = -u K )
87 86 oveq1d 
 |-  ( K e. NN -> ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) = ( -u K mod N ) )
88 87 opeq2d 
 |-  ( K e. NN -> <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. = <. 1 , ( -u K mod N ) >. )
89 84 88 preq12d 
 |-  ( K e. NN -> { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } = { <. 1 , ( K mod N ) >. , <. 1 , ( -u K mod N ) >. } )
90 eqid 
 |-  { <. 1 , ( K mod N ) >. , <. 1 , ( -u K mod N ) >. } = { <. 1 , ( K mod N ) >. , <. 1 , ( -u K mod N ) >. }
91 1 2 90 gpg3kgrtriexlem6 
 |-  ( K e. NN -> { <. 1 , ( K mod N ) >. , <. 1 , ( -u K mod N ) >. } e. ( Edg ` G ) )
92 89 91 eqeltrd 
 |-  ( K e. NN -> { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } e. ( Edg ` G ) )
93 79 92 jca 
 |-  ( K e. NN -> ( <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. =/= <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. /\ { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } e. ( Edg ` G ) ) )
94 93 adantr 
 |-  ( ( K e. NN /\ ( G NeighbVtx <. 1 , 0 >. ) = { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } ) -> ( <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. =/= <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. /\ { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } e. ( Edg ` G ) ) )
95 48 52 57 62 94 2rspcedvdw 
 |-  ( ( K e. NN /\ ( G NeighbVtx <. 1 , 0 >. ) = { <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) + K ) mod N ) >. , <. 0 , ( 2nd ` <. 1 , 0 >. ) >. , <. 1 , ( ( ( 2nd ` <. 1 , 0 >. ) - K ) mod N ) >. } ) -> E. b e. ( G NeighbVtx <. 1 , 0 >. ) E. c e. ( G NeighbVtx <. 1 , 0 >. ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) )
96 44 95 mpdan 
 |-  ( K e. NN -> E. b e. ( G NeighbVtx <. 1 , 0 >. ) E. c e. ( G NeighbVtx <. 1 , 0 >. ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) )
97 22 27 96 rspcedvd 
 |-  ( K e. NN -> E. a e. ( Vtx ` G ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) )
98 gpgusgra 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph )
99 2 98 eqeltrid 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> G e. USGraph )
100 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
101 eqid 
 |-  ( G NeighbVtx a ) = ( G NeighbVtx a )
102 34 100 101 usgrgrtrirex 
 |-  ( G e. USGraph -> ( E. t t e. ( GrTriangles ` G ) <-> E. a e. ( Vtx ` G ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) ) )
103 33 99 102 3syl 
 |-  ( K e. NN -> ( E. t t e. ( GrTriangles ` G ) <-> E. a e. ( Vtx ` G ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( Edg ` G ) ) ) )
104 97 103 mpbird 
 |-  ( K e. NN -> E. t t e. ( GrTriangles ` G ) )