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 ⊢ 𝑁 = ( 3 · 𝐾 )
gpg3kgrtriex.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
Assertion gpg3kgrtriex ( 𝐾 ∈ ℕ → ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 gpg3kgrtriex.n ⊢ 𝑁 = ( 3 · 𝐾 )
2 gpg3kgrtriex.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
3 1ex ⊢ 1 ∈ V
4 3 prid2 ⊢ 1 ∈ { 0 , 1 }
5 4 a1i ⊢ ( 𝐾 ∈ ℕ → 1 ∈ { 0 , 1 } )
6 3nn ⊢ 3 ∈ ℕ
7 6 a1i ⊢ ( 𝐾 ∈ ℕ → 3 ∈ ℕ )
8 id ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ )
9 7 8 nnmulcld ⊢ ( 𝐾 ∈ ℕ → ( 3 · 𝐾 ) ∈ ℕ )
10 1 9 eqeltrid ⊢ ( 𝐾 ∈ ℕ → 𝑁 ∈ ℕ )
11 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ℕ )
12 10 11 sylibr ⊢ ( 𝐾 ∈ ℕ → 0 ∈ ( 0 ..^ 𝑁 ) )
13 5 12 opelxpd ⊢ ( 𝐾 ∈ ℕ → ⟨ 1 , 0 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
14 1 gpg3kgrtriexlem4 ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
15 10 14 jca ⊢ ( 𝐾 ∈ ℕ → ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) )
16 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
17 eqid ⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
18 16 17 gpgvtx ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
19 18 eleq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( ⟨ 1 , 0 ⟩ ∈ ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) ↔ ⟨ 1 , 0 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
20 15 19 syl ⊢ ( 𝐾 ∈ ℕ → ( ⟨ 1 , 0 ⟩ ∈ ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) ↔ ⟨ 1 , 0 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
21 13 20 mpbird ⊢ ( 𝐾 ∈ ℕ → ⟨ 1 , 0 ⟩ ∈ ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) )
22 2 fveq2i ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) )
23 21 22 eleqtrrdi ⊢ ( 𝐾 ∈ ℕ → ⟨ 1 , 0 ⟩ ∈ ( Vtx ‘ 𝐺 ) )
24 oveq2 ⊢ ( 𝑎 = ⟨ 1 , 0 ⟩ → ( 𝐺 NeighbVtx 𝑎 ) = ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) )
25 biidd ⊢ ( 𝑎 = ⟨ 1 , 0 ⟩ → ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) )
26 24 25 rexeqbidv ⊢ ( 𝑎 = ⟨ 1 , 0 ⟩ → ( ∃ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑎 ) ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ∃ 𝑐 ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) )
27 24 26 rexeqbidv ⊢ ( 𝑎 = ⟨ 1 , 0 ⟩ → ( ∃ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∃ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑎 ) ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ∃ 𝑏 ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) ∃ 𝑐 ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) )
28 27 adantl ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑎 = ⟨ 1 , 0 ⟩ ) → ( ∃ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∃ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑎 ) ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ∃ 𝑏 ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) ∃ 𝑐 ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) )
29 1 gpg3kgrtriexlem3 ⊢ ( 𝐾 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
30 eqid ⊢ 1 = 1
31 30 a1i ⊢ ( 𝐾 ∈ ℕ → 1 = 1 )
32 31 olcd ⊢ ( 𝐾 ∈ ℕ → ( 1 = 0 ∨ 1 = 1 ) )
33 32 12 jca ⊢ ( 𝐾 ∈ ℕ → ( ( 1 = 0 ∨ 1 = 1 ) ∧ 0 ∈ ( 0 ..^ 𝑁 ) ) )
34 29 14 jca ⊢ ( 𝐾 ∈ ℕ → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) )
35 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
36 17 16 2 35 opgpgvtx ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( ⟨ 1 , 0 ⟩ ∈ ( Vtx ‘ 𝐺 ) ↔ ( ( 1 = 0 ∨ 1 = 1 ) ∧ 0 ∈ ( 0 ..^ 𝑁 ) ) ) )
37 34 36 syl ⊢ ( 𝐾 ∈ ℕ → ( ⟨ 1 , 0 ⟩ ∈ ( Vtx ‘ 𝐺 ) ↔ ( ( 1 = 0 ∨ 1 = 1 ) ∧ 0 ∈ ( 0 ..^ 𝑁 ) ) ) )
38 33 37 mpbird ⊢ ( 𝐾 ∈ ℕ → ⟨ 1 , 0 ⟩ ∈ ( Vtx ‘ 𝐺 ) )
39 c0ex ⊢ 0 ∈ V
40 3 39 op1st ⊢ ( 1st ‘ ⟨ 1 , 0 ⟩ ) = 1
41 40 a1i ⊢ ( 𝐾 ∈ ℕ → ( 1st ‘ ⟨ 1 , 0 ⟩ ) = 1 )
42 eqid ⊢ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) = ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ )
43 16 2 35 42 gpgnbgrvtx1 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) ∧ ( ⟨ 1 , 0 ⟩ ∈ ( Vtx ‘ 𝐺 ) ∧ ( 1st ‘ ⟨ 1 , 0 ⟩ ) = 1 ) ) → ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) = { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } )
44 29 14 38 41 43 syl22anc ⊢ ( 𝐾 ∈ ℕ → ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) = { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } )
45 neeq1 ⊢ ( 𝑏 = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ → ( 𝑏 ≠ 𝑐 ↔ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ 𝑐 ) )
46 preq1 ⊢ ( 𝑏 = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ → { 𝑏 , 𝑐 } = { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑐 } )
47 46 eleq1d ⊢ ( 𝑏 = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ → ( { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ↔ { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) )
48 45 47 anbi12d ⊢ ( 𝑏 = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ → ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ 𝑐 ∧ { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) )
49 neeq2 ⊢ ( 𝑐 = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ → ( ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ 𝑐 ↔ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) )
50 preq2 ⊢ ( 𝑐 = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ → { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑐 } = { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } )
51 50 eleq1d ⊢ ( 𝑐 = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ → ( { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ↔ { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ) )
52 49 51 anbi12d ⊢ ( 𝑐 = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ → ( ( ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ 𝑐 ∧ { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ∧ { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ) ) )
53 opex ⊢ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ V
54 53 tpid1 ⊢ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ }
55 eleq2 ⊢ ( ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) = { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } → ( ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) ↔ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ) )
56 55 adantl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) = { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ) → ( ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) ↔ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ) )
57 54 56 mpbiri ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) = { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ) → ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) )
58 opex ⊢ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ V
59 58 tpid3 ⊢ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ }
60 eleq2 ⊢ ( ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) = { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } → ( ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) ↔ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ) )
61 60 adantl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) = { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ) → ( ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) ↔ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ) )
62 59 61 mpbiri ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) = { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ) → ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) )
63 1 gpg3kgrtriexlem5 ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 mod 𝑁 ) ≠ ( - 𝐾 mod 𝑁 ) )
64 3 39 op2nd ⊢ ( 2nd ‘ ⟨ 1 , 0 ⟩ ) = 0
65 64 oveq1i ⊢ ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) = ( 0 + 𝐾 )
66 nncn ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℂ )
67 66 addlidd ⊢ ( 𝐾 ∈ ℕ → ( 0 + 𝐾 ) = 𝐾 )
68 65 67 eqtrid ⊢ ( 𝐾 ∈ ℕ → ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) = 𝐾 )
69 68 oveq1d ⊢ ( 𝐾 ∈ ℕ → ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) = ( 𝐾 mod 𝑁 ) )
70 64 oveq1i ⊢ ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) = ( 0 − 𝐾 )
71 70 a1i ⊢ ( 𝐾 ∈ ℕ → ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) = ( 0 − 𝐾 ) )
72 df-neg ⊢ - 𝐾 = ( 0 − 𝐾 )
73 71 72 eqtr4di ⊢ ( 𝐾 ∈ ℕ → ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) = - 𝐾 )
74 73 oveq1d ⊢ ( 𝐾 ∈ ℕ → ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) = ( - 𝐾 mod 𝑁 ) )
75 63 69 74 3netr4d ⊢ ( 𝐾 ∈ ℕ → ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) )
76 75 olcd ⊢ ( 𝐾 ∈ ℕ → ( 1 ≠ 1 ∨ ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ) )
77 ovex ⊢ ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ∈ V
78 3 77 opthne ⊢ ( ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ↔ ( 1 ≠ 1 ∨ ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ) )
79 76 78 sylibr ⊢ ( 𝐾 ∈ ℕ → ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ )
80 64 a1i ⊢ ( 𝐾 ∈ ℕ → ( 2nd ‘ ⟨ 1 , 0 ⟩ ) = 0 )
81 80 oveq1d ⊢ ( 𝐾 ∈ ℕ → ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) = ( 0 + 𝐾 ) )
82 81 67 eqtrd ⊢ ( 𝐾 ∈ ℕ → ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) = 𝐾 )
83 82 oveq1d ⊢ ( 𝐾 ∈ ℕ → ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) = ( 𝐾 mod 𝑁 ) )
84 83 opeq2d ⊢ ( 𝐾 ∈ ℕ → ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ )
85 80 oveq1d ⊢ ( 𝐾 ∈ ℕ → ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) = ( 0 − 𝐾 ) )
86 85 72 eqtr4di ⊢ ( 𝐾 ∈ ℕ → ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) = - 𝐾 )
87 86 oveq1d ⊢ ( 𝐾 ∈ ℕ → ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) = ( - 𝐾 mod 𝑁 ) )
88 87 opeq2d ⊢ ( 𝐾 ∈ ℕ → ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( - 𝐾 mod 𝑁 ) ⟩ )
89 84 88 preq12d ⊢ ( 𝐾 ∈ ℕ → { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( - 𝐾 mod 𝑁 ) ⟩ } )
90 eqid ⊢ { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( - 𝐾 mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( - 𝐾 mod 𝑁 ) ⟩ }
91 1 2 90 gpg3kgrtriexlem6 ⊢ ( 𝐾 ∈ ℕ → { ⟨ 1 , ( 𝐾 mod 𝑁 ) ⟩ , ⟨ 1 , ( - 𝐾 mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) )
92 89 91 eqeltrd ⊢ ( 𝐾 ∈ ℕ → { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) )
93 79 92 jca ⊢ ( 𝐾 ∈ ℕ → ( ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ∧ { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ) )
94 93 adantr ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) = { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ) → ( ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ∧ { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ ( Edg ‘ 𝐺 ) ) )
95 48 52 57 62 94 2rspcedvdw ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) = { ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 0 ⟩ ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 0 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ) → ∃ 𝑏 ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) ∃ 𝑐 ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) )
96 44 95 mpdan ⊢ ( 𝐾 ∈ ℕ → ∃ 𝑏 ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) ∃ 𝑐 ∈ ( 𝐺 NeighbVtx ⟨ 1 , 0 ⟩ ) ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) )
97 23 28 96 rspcedvd ⊢ ( 𝐾 ∈ ℕ → ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∃ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑎 ) ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) )
98 gpgusgra ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 𝑁 gPetersenGr 𝐾 ) ∈ USGraph )
99 2 98 eqeltrid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → 𝐺 ∈ USGraph )
100 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
101 eqid ⊢ ( 𝐺 NeighbVtx 𝑎 ) = ( 𝐺 NeighbVtx 𝑎 )
102 35 100 101 usgrgrtrirex ⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∃ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑎 ) ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) )
103 34 99 102 3syl ⊢ ( 𝐾 ∈ ℕ → ( ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∃ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑎 ) ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) )
104 97 103 mpbird ⊢ ( 𝐾 ∈ ℕ → ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) )