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 K
gpg3kgrtriex.g No typesetting found for |- G = ( N gPetersenGr K ) with typecode |-
Assertion gpg3kgrtriex Could not format assertion : No typesetting found for |- ( K e. NN -> E. t t e. ( GrTriangles ` G ) ) with typecode |-

Proof

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