Theorem gpg3kgrtriex 49013

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

Hypotheses

Ref	Expression
gpg3kgrtriex.n	⊢ 𝑁 = (3 · 𝐾)
gpg3kgrtriex.g	⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)

Assertion

Ref	Expression
gpg3kgrtriex	⊢ (𝐾 ∈ ℕ → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺))

Distinct variable group:   𝑡,𝐺

Allowed substitution hints:   𝐾(𝑡)   𝑁(𝑡)

Proof of Theorem gpg3kgrtriex

Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1elpr01 11232	. . . . . . 7 ⊢ 1 ∈ {0, 1}
2	1	a1i 11	. . . . . 6 ⊢ (𝐾 ∈ ℕ → 1 ∈ {0, 1})
3		gpg3kgrtriex.n	. . . . . . . 8 ⊢ 𝑁 = (3 · 𝐾)
4		3nn 12348	. . . . . . . . . 10 ⊢ 3 ∈ ℕ
5	4	a1i 11	. . . . . . . . 9 ⊢ (𝐾 ∈ ℕ → 3 ∈ ℕ)
6		id 23	. . . . . . . . 9 ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ ℕ)
7	5, 6	nnmulcld 12317	. . . . . . . 8 ⊢ (𝐾 ∈ ℕ → (3 · 𝐾) ∈ ℕ)
8	3, 7	eqeltrid 2866	. . . . . . 7 ⊢ (𝐾 ∈ ℕ → 𝑁 ∈ ℕ)
9		lbfzo0 13759	. . . . . . 7 ⊢ (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
10	8, 9	sylibr 237	. . . . . 6 ⊢ (𝐾 ∈ ℕ → 0 ∈ (0..^𝑁))
11	2, 10	opelxpd 5698	. . . . 5 ⊢ (𝐾 ∈ ℕ → ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁)))
12	3	gpg3kgrtriexlem4 49010	. . . . . . 7 ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ (1..^(⌈‘(𝑁 / 2))))
13	8, 12	jca 521	. . . . . 6 ⊢ (𝐾 ∈ ℕ → (𝑁 ∈ ℕ ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))))
14		eqid 2762	. . . . . . . 8 ⊢ (1..^(⌈‘(𝑁 / 2))) = (1..^(⌈‘(𝑁 / 2)))
15		eqid 2762	. . . . . . . 8 ⊢ (0..^𝑁) = (0..^𝑁)
16	14, 15	gpgvtx 48967	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) → (Vtx‘(𝑁 gPetersenGr 𝐾)) = ({0, 1} × (0..^𝑁)))
17	16	eleq2d 2848	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) → (⟨1, 0⟩ ∈ (Vtx‘(𝑁 gPetersenGr 𝐾)) ↔ ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁))))
18	13, 17	syl 18	. . . . 5 ⊢ (𝐾 ∈ ℕ → (⟨1, 0⟩ ∈ (Vtx‘(𝑁 gPetersenGr 𝐾)) ↔ ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁))))
19	11, 18	mpbird 260	. . . 4 ⊢ (𝐾 ∈ ℕ → ⟨1, 0⟩ ∈ (Vtx‘(𝑁 gPetersenGr 𝐾)))
20		gpg3kgrtriex.g	. . . . 5 ⊢ 𝐺 = (𝑁 gPetersenGr 𝐾)
21	20	fveq2i 6885	. . . 4 ⊢ (Vtx‘𝐺) = (Vtx‘(𝑁 gPetersenGr 𝐾))
22	19, 21	eleqtrrdi 2873	. . 3 ⊢ (𝐾 ∈ ℕ → ⟨1, 0⟩ ∈ (Vtx‘𝐺))
23		oveq2 7425	. . . . 5 ⊢ (𝑎 = ⟨1, 0⟩ → (𝐺 NeighbVtx 𝑎) = (𝐺 NeighbVtx ⟨1, 0⟩))
24		biidd 265	. . . . . 6 ⊢ (𝑎 = ⟨1, 0⟩ → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) ↔ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
25	23, 24	rexeqbidv 3337	. . . . 5 ⊢ (𝑎 = ⟨1, 0⟩ → (∃𝑐 ∈ (𝐺 NeighbVtx 𝑎)(𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) ↔ ∃𝑐 ∈ (𝐺 NeighbVtx ⟨1, 0⟩)(𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
26	23, 25	rexeqbidv 3337	. . . 4 ⊢ (𝑎 = ⟨1, 0⟩ → (∃𝑏 ∈ (𝐺 NeighbVtx 𝑎)∃𝑐 ∈ (𝐺 NeighbVtx 𝑎)(𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) ↔ ∃𝑏 ∈ (𝐺 NeighbVtx ⟨1, 0⟩)∃𝑐 ∈ (𝐺 NeighbVtx ⟨1, 0⟩)(𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
27	26	adantl 487	. . 3 ⊢ ((𝐾 ∈ ℕ ∧ 𝑎 = ⟨1, 0⟩) → (∃𝑏 ∈ (𝐺 NeighbVtx 𝑎)∃𝑐 ∈ (𝐺 NeighbVtx 𝑎)(𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) ↔ ∃𝑏 ∈ (𝐺 NeighbVtx ⟨1, 0⟩)∃𝑐 ∈ (𝐺 NeighbVtx ⟨1, 0⟩)(𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
28	3	gpg3kgrtriexlem3 49009	. . . . 5 ⊢ (𝐾 ∈ ℕ → 𝑁 ∈ (ℤ≥‘3))
29		eqid 2762	. . . . . . . . 9 ⊢ 1 = 1
30	29	a1i 11	. . . . . . . 8 ⊢ (𝐾 ∈ ℕ → 1 = 1)
31	30	olcd 888	. . . . . . 7 ⊢ (𝐾 ∈ ℕ → (1 = 0 ∨ 1 = 1))
32	31, 10	jca 521	. . . . . 6 ⊢ (𝐾 ∈ ℕ → ((1 = 0 ∨ 1 = 1) ∧ 0 ∈ (0..^𝑁)))
33	28, 12	jca 521	. . . . . . 7 ⊢ (𝐾 ∈ ℕ → (𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))))
34		eqid 2762	. . . . . . . 8 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
35	15, 14, 20, 34	opgpgvtx 48979	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) → (⟨1, 0⟩ ∈ (Vtx‘𝐺) ↔ ((1 = 0 ∨ 1 = 1) ∧ 0 ∈ (0..^𝑁))))
36	33, 35	syl 18	. . . . . 6 ⊢ (𝐾 ∈ ℕ → (⟨1, 0⟩ ∈ (Vtx‘𝐺) ↔ ((1 = 0 ∨ 1 = 1) ∧ 0 ∈ (0..^𝑁))))
37	32, 36	mpbird 260	. . . . 5 ⊢ (𝐾 ∈ ℕ → ⟨1, 0⟩ ∈ (Vtx‘𝐺))
38		1ex 11231	. . . . . . 7 ⊢ 1 ∈ V
39		c0ex 11228	. . . . . . 7 ⊢ 0 ∈ V
40	38, 39	op1st 7998	. . . . . 6 ⊢ (1st ‘⟨1, 0⟩) = 1
41	40	a1i 11	. . . . 5 ⊢ (𝐾 ∈ ℕ → (1st ‘⟨1, 0⟩) = 1)
42		eqid 2762	. . . . . 6 ⊢ (𝐺 NeighbVtx ⟨1, 0⟩) = (𝐺 NeighbVtx ⟨1, 0⟩)
43	14, 20, 34, 42	gpgnbgrvtx1 48999	. . . . 5 ⊢ (((𝑁 ∈ (ℤ≥‘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	28, 12, 37, 41, 43	syl22anc 852	. . . 4 ⊢ (𝐾 ∈ ℕ → (𝐺 NeighbVtx ⟨1, 0⟩) = {⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2nd ‘⟨1, 0⟩)⟩, ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩})
45		neeq1 3019	. . . . . 6 ⊢ (𝑏 = ⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ → (𝑏 ≠ 𝑐 ↔ ⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ 𝑐))
46		preq1 4697	. . . . . . 7 ⊢ (𝑏 = ⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ → {𝑏, 𝑐} = {⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, 𝑐})
47	46	eleq1d 2847	. . . . . 6 ⊢ (𝑏 = ⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ → ({𝑏, 𝑐} ∈ (Edg‘𝐺) ↔ {⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, 𝑐} ∈ (Edg‘𝐺)))
48	45, 47	anbi12d 644	. . . . 5 ⊢ (𝑏 = ⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) ↔ (⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ 𝑐 ∧ {⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, 𝑐} ∈ (Edg‘𝐺))))
49		neeq2 3020	. . . . . 6 ⊢ (𝑐 = ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ → (⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ 𝑐 ↔ ⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩))
50		preq2 4698	. . . . . . 7 ⊢ (𝑐 = ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ → {⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, 𝑐} = {⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩})
51	50	eleq1d 2847	. . . . . 6 ⊢ (𝑐 = ⟨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 644	. . . . 5 ⊢ (𝑐 = ⟨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 5443	. . . . . . 7 ⊢ ⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ∈ V
54	53	tpid1 4732	. . . . . 6 ⊢ ⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ∈ {⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2nd ‘⟨1, 0⟩)⟩, ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩}
55		eleq2 2851	. . . . . . 7 ⊢ ((𝐺 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 487	. . . . . 6 ⊢ ((𝐾 ∈ ℕ ∧ (𝐺 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 261	. . . . 5 ⊢ ((𝐾 ∈ ℕ ∧ (𝐺 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 5443	. . . . . . 7 ⊢ ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ∈ V
59	58	tpid3 4737	. . . . . 6 ⊢ ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ∈ {⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2nd ‘⟨1, 0⟩)⟩, ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩}
60		eleq2 2851	. . . . . . 7 ⊢ ((𝐺 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 487	. . . . . 6 ⊢ ((𝐾 ∈ ℕ ∧ (𝐺 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 261	. . . . 5 ⊢ ((𝐾 ∈ ℕ ∧ (𝐺 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	3	gpg3kgrtriexlem5 49011	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ → (𝐾 mod 𝑁) ≠ (-𝐾 mod 𝑁))
64	38, 39	op2nd 7999	. . . . . . . . . . . . 13 ⊢ (2nd ‘⟨1, 0⟩) = 0
65	64	oveq1i 7427	. . . . . . . . . . . 12 ⊢ ((2nd ‘⟨1, 0⟩) + 𝐾) = (0 + 𝐾)
66		nncn 12269	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ ℂ)
67	66	addlidd 11439	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℕ → (0 + 𝐾) = 𝐾)
68	65, 67	eqtrid 2809	. . . . . . . . . . 11 ⊢ (𝐾 ∈ ℕ → ((2nd ‘⟨1, 0⟩) + 𝐾) = 𝐾)
69	68	oveq1d 7432	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ → (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁) = (𝐾 mod 𝑁))
70	64	oveq1i 7427	. . . . . . . . . . . . 13 ⊢ ((2nd ‘⟨1, 0⟩) − 𝐾) = (0 − 𝐾)
71	70	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℕ → ((2nd ‘⟨1, 0⟩) − 𝐾) = (0 − 𝐾))
72		df-neg 11472	. . . . . . . . . . . 12 ⊢ -𝐾 = (0 − 𝐾)
73	71, 72	eqtr4di 2815	. . . . . . . . . . 11 ⊢ (𝐾 ∈ ℕ → ((2nd ‘⟨1, 0⟩) − 𝐾) = -𝐾)
74	73	oveq1d 7432	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ → (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁) = (-𝐾 mod 𝑁))
75	63, 69, 74	3netr4d 3034	. . . . . . . . 9 ⊢ (𝐾 ∈ ℕ → (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁) ≠ (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁))
76	75	olcd 888	. . . . . . . 8 ⊢ (𝐾 ∈ ℕ → (1 ≠ 1 ∨ (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁) ≠ (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)))
77		ovex 7450	. . . . . . . . 9 ⊢ (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁) ∈ V
78	38, 77	opthne 5462	. . . . . . . 8 ⊢ (⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ↔ (1 ≠ 1 ∨ (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁) ≠ (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)))
79	76, 78	sylibr 237	. . . . . . 7 ⊢ (𝐾 ∈ ℕ → ⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩)
80	64	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ ℕ → (2nd ‘⟨1, 0⟩) = 0)
81	80	oveq1d 7432	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℕ → ((2nd ‘⟨1, 0⟩) + 𝐾) = (0 + 𝐾))
82	81, 67	eqtrd 2797	. . . . . . . . . . 11 ⊢ (𝐾 ∈ ℕ → ((2nd ‘⟨1, 0⟩) + 𝐾) = 𝐾)
83	82	oveq1d 7432	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ → (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁) = (𝐾 mod 𝑁))
84	83	opeq2d 4843	. . . . . . . . 9 ⊢ (𝐾 ∈ ℕ → ⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ = ⟨1, (𝐾 mod 𝑁)⟩)
85	80	oveq1d 7432	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℕ → ((2nd ‘⟨1, 0⟩) − 𝐾) = (0 − 𝐾))
86	85, 72	eqtr4di 2815	. . . . . . . . . . 11 ⊢ (𝐾 ∈ ℕ → ((2nd ‘⟨1, 0⟩) − 𝐾) = -𝐾)
87	86	oveq1d 7432	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ → (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁) = (-𝐾 mod 𝑁))
88	87	opeq2d 4843	. . . . . . . . 9 ⊢ (𝐾 ∈ ℕ → ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ = ⟨1, (-𝐾 mod 𝑁)⟩)
89	84, 88	preq12d 4705	. . . . . . . 8 ⊢ (𝐾 ∈ ℕ → {⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩} = {⟨1, (𝐾 mod 𝑁)⟩, ⟨1, (-𝐾 mod 𝑁)⟩})
90		eqid 2762	. . . . . . . . 9 ⊢ {⟨1, (𝐾 mod 𝑁)⟩, ⟨1, (-𝐾 mod 𝑁)⟩} = {⟨1, (𝐾 mod 𝑁)⟩, ⟨1, (-𝐾 mod 𝑁)⟩}
91	3, 20, 90	gpg3kgrtriexlem6 49012	. . . . . . . 8 ⊢ (𝐾 ∈ ℕ → {⟨1, (𝐾 mod 𝑁)⟩, ⟨1, (-𝐾 mod 𝑁)⟩} ∈ (Edg‘𝐺))
92	89, 91	eqeltrd 2862	. . . . . . 7 ⊢ (𝐾 ∈ ℕ → {⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩} ∈ (Edg‘𝐺))
93	79, 92	jca 521	. . . . . 6 ⊢ (𝐾 ∈ ℕ → (⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ∧ {⟨1, (((2nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨1, (((2nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩} ∈ (Edg‘𝐺)))
94	93	adantr 486	. . . . 5 ⊢ ((𝐾 ∈ ℕ ∧ (𝐺 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 3593	. . . 4 ⊢ ((𝐾 ∈ ℕ ∧ (𝐺 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 700	. . 3 ⊢ (𝐾 ∈ ℕ → ∃𝑏 ∈ (𝐺 NeighbVtx ⟨1, 0⟩)∃𝑐 ∈ (𝐺 NeighbVtx ⟨1, 0⟩)(𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))
97	22, 27, 96	rspcedvd 3581	. 2 ⊢ (𝐾 ∈ ℕ → ∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (𝐺 NeighbVtx 𝑎)∃𝑐 ∈ (𝐺 NeighbVtx 𝑎)(𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))
98		gpgusgra 48981	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) → (𝑁 gPetersenGr 𝐾) ∈ USGraph)
99	20, 98	eqeltrid 2866	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) → 𝐺 ∈ USGraph)
100		eqid 2762	. . . 4 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
101		eqid 2762	. . . 4 ⊢ (𝐺 NeighbVtx 𝑎) = (𝐺 NeighbVtx 𝑎)
102	34, 100, 101	usgrgrtrirex 48874	. . 3 ⊢ (𝐺 ∈ USGraph → (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (𝐺 NeighbVtx 𝑎)∃𝑐 ∈ (𝐺 NeighbVtx 𝑎)(𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
103	33, 99, 102	3syl 19	. 2 ⊢ (𝐾 ∈ ℕ → (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (𝐺 NeighbVtx 𝑎)∃𝑐 ∈ (𝐺 NeighbVtx 𝑎)(𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
104	97, 103	mpbird 260	1 ⊢ (𝐾 ∈ ℕ → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2957  ∃wrex 3088  {cpr 4589  {ctp 4591  ⟨cop 4593   × cxp 5657  ‘cfv 6537  (class class class)co 7417  1^st c1st 7988  2^nd c2nd 7989  0cc0 11128  1c1 11129   + caddc 11131   · cmul 11133   − cmin 11469  -cneg 11470   / cdiv 11899  ℕcn 12261  2c2 12323  3c3 12324  ℤ_≥cuz 12891  ..^cfzo 13713  ⌈cceil 13856   mod cmo 13934  Vtxcvtx 29461  Edgcedg 29512  USGraphcusgr 29617   NeighbVtx cnbgr 29800  GrTrianglescgrtri 48861   gPetersenGr cgpg 48964

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205  ax-pre-sup 11206

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7867  df-1st 7990  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-2o 8460  df-3o 8461  df-oadd 8463  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-fin 8960  df-sup 9416  df-inf 9417  df-dju 9910  df-card 9948  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472  df-div 11900  df-nn 12262  df-2 12331  df-3 12332  df-4 12333  df-5 12334  df-6 12335  df-7 12336  df-8 12337  df-9 12338  df-n0 12533  df-xnn0 12606  df-z 12620  df-dec 12741  df-uz 12892  df-rp 13047  df-ico 13408  df-fz 13566  df-fzo 13714  df-fl 13857  df-ceil 13858  df-mod 13935  df-hash 14399  df-dvds 16349  df-struct 17245  df-slot 17280  df-ndx 17292  df-base 17308  df-edgf 29454  df-vtx 29463  df-iedg 29464  df-edg 29513  df-uhgr 29523  df-upgr 29547  df-umgr 29548  df-uspgr 29618  df-usgr 29619  df-nbgr 29801  df-grtri 48862  df-gpg 48965

This theorem is used by: (None)