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 1ex 
 |-  1 e. _V
4 3 prid2 
 |-  1 e. { 0 , 1 }
5 4 a1i 
 |-  ( K e. NN -> 1 e. { 0 , 1 } )
6 3nn 
 |-  3 e. NN
7 6 a1i 
 |-  ( K e. NN -> 3 e. NN )
8 id 
 |-  ( K e. NN -> K e. NN )
9 7 8 nnmulcld 
 |-  ( K e. NN -> ( 3 x. K ) e. NN )
10 1 9 eqeltrid 
 |-  ( K e. NN -> N e. NN )
11 lbfzo0 
 |-  ( 0 e. ( 0 ..^ N ) <-> N e. NN )
12 10 11 sylibr 
 |-  ( K e. NN -> 0 e. ( 0 ..^ N ) )
13 5 12 opelxpd 
 |-  ( K e. NN -> <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
14 1 gpg3kgrtriexlem4 
 |-  ( K e. NN -> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
15 10 14 jca 
 |-  ( K e. NN -> ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) )
16 eqid 
 |-  ( 1 ..^ ( |^ ` ( N / 2 ) ) ) = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
17 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
18 16 17 gpgvtx 
 |-  ( ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( Vtx ` ( N gPetersenGr K ) ) = ( { 0 , 1 } X. ( 0 ..^ N ) ) )
19 18 eleq2d 
 |-  ( ( N e. NN /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( <. 1 , 0 >. e. ( Vtx ` ( N gPetersenGr K ) ) <-> <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
20 15 19 syl 
 |-  ( K e. NN -> ( <. 1 , 0 >. e. ( Vtx ` ( N gPetersenGr K ) ) <-> <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
21 13 20 mpbird 
 |-  ( K e. NN -> <. 1 , 0 >. e. ( Vtx ` ( N gPetersenGr K ) ) )
22 2 fveq2i 
 |-  ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) )
23 21 22 eleqtrrdi 
 |-  ( K e. NN -> <. 1 , 0 >. e. ( Vtx ` G ) )
24 oveq2 
 |-  ( a = <. 1 , 0 >. -> ( G NeighbVtx a ) = ( G NeighbVtx <. 1 , 0 >. ) )
25 biidd 
 |-  ( a = <. 1 , 0 >. -> ( ( b =/= c /\ { b , c } e. ( Edg ` G ) ) <-> ( b =/= c /\ { b , c } e. ( Edg ` G ) ) ) )
26 24 25 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 ) ) ) )
27 24 26 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 ) ) ) )
28 27 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 ) ) ) )
29 1 gpg3kgrtriexlem3 
 |-  ( K e. NN -> N e. ( ZZ>= ` 3 ) )
30 eqid 
 |-  1 = 1
31 30 a1i 
 |-  ( K e. NN -> 1 = 1 )
32 31 olcd 
 |-  ( K e. NN -> ( 1 = 0 \/ 1 = 1 ) )
33 32 12 jca 
 |-  ( K e. NN -> ( ( 1 = 0 \/ 1 = 1 ) /\ 0 e. ( 0 ..^ N ) ) )
34 29 14 jca 
 |-  ( K e. NN -> ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) )
35 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
36 17 16 2 35 opgpgvtx 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( <. 1 , 0 >. e. ( Vtx ` G ) <-> ( ( 1 = 0 \/ 1 = 1 ) /\ 0 e. ( 0 ..^ N ) ) ) )
37 34 36 syl 
 |-  ( K e. NN -> ( <. 1 , 0 >. e. ( Vtx ` G ) <-> ( ( 1 = 0 \/ 1 = 1 ) /\ 0 e. ( 0 ..^ N ) ) ) )
38 33 37 mpbird 
 |-  ( K e. NN -> <. 1 , 0 >. e. ( Vtx ` G ) )
39 c0ex 
 |-  0 e. _V
40 3 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 16 2 35 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 29 14 38 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 3 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 3 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 23 28 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 35 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 34 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 ) )