gpg3kgrtriex - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > gpg3kgrtriex		Structured version Visualization version GIF version

Theorem gpg3kgrtriex 48887

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 11222	. . . . . . 7 ⊢ 1 ∈ {0, 1}
2	1	a1i 11	. . . . . 6 ⊢ (𝐾 ∈ ℕ → 1 ∈ {0, 1})
3		gpg3kgrtriex.n	. . . . . . . 8 ⊢ 𝑁 = (3 · 𝐾)
4		3nn 12338	. . . . . . . . . 10 ⊢ 3 ∈ ℕ
5	4	a1i 11	. . . . . . . . 9 ⊢ (𝐾 ∈ ℕ → 3 ∈ ℕ)
6		id 23	. . . . . . . . 9 ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ ℕ)
7	5, 6	nnmulcld 12307	. . . . . . . 8 ⊢ (𝐾 ∈ ℕ → (3 · 𝐾) ∈ ℕ)
8	3, 7	eqeltrid 2870	. . . . . . 7 ⊢ (𝐾 ∈ ℕ → 𝑁 ∈ ℕ)
9		lbfzo0 13747	. . . . . . 7 ⊢ (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
10	8, 9	sylibr 237	. . . . . 6 ⊢ (𝐾 ∈ ℕ → 0 ∈ (0..^𝑁))
11	2, 10	opelxpd 5705	. . . . 5 ⊢ (𝐾 ∈ ℕ → ⟨1, 0⟩ ∈ ({0, 1} × (0..^𝑁)))
12	3	gpg3kgrtriexlem4 48884	. . . . . . 7 ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ (1..^(⌈‘(𝑁 / 2))))
13	8, 12	jca 521	. . . . . 6 ⊢ (𝐾 ∈ ℕ → (𝑁 ∈ ℕ ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))))
14		eqid 2766	. . . . . . . 8 ⊢ (1..^(⌈‘(𝑁 / 2))) = (1..^(⌈‘(𝑁 / 2)))
15		eqid 2766	. . . . . . . 8 ⊢ (0..^𝑁) = (0..^𝑁)
16	14, 15	gpgvtx 48841	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) → (Vtx‘(𝑁 gPetersenGr 𝐾)) = ({0, 1} × (0..^𝑁)))
17	16	eleq2d 2852	. . . . . 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 6891	. . . 4 ⊢ (Vtx‘𝐺) = (Vtx‘(𝑁 gPetersenGr 𝐾))
22	19, 21	eleqtrrdi 2877	. . 3 ⊢ (𝐾 ∈ ℕ → ⟨1, 0⟩ ∈ (Vtx‘𝐺))
23		oveq2 7431	. . . . 5 ⊢ (𝑎 = ⟨1, 0⟩ → (𝐺 NeighbVtx 𝑎) = (𝐺 NeighbVtx ⟨1, 0⟩))
24		biidd 265	. . . . . 6 ⊢ (𝑎 = ⟨1, 0⟩ → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) ↔ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
25	23, 24	rexeqbidv 3342	. . . . 5 ⊢ (𝑎 = ⟨1, 0⟩ → (∃𝑐 ∈ (𝐺 NeighbVtx 𝑎)(𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) ↔ ∃𝑐 ∈ (𝐺 NeighbVtx ⟨1, 0⟩)(𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
26	23, 25	rexeqbidv 3342	. . . 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 48883	. . . . 5 ⊢ (𝐾 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘3))
29		eqid 2766	. . . . . . . . 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 2766	. . . . . . . 8 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
35	15, 14, 20, 34	opgpgvtx 48853	. . . . . . 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 11221	. . . . . . 7 ⊢ 1 ∈ V
39		c0ex 11218	. . . . . . 7 ⊢ 0 ∈ V
40	38, 39	op1st 8003	. . . . . 6 ⊢ (1^st ‘⟨1, 0⟩) = 1
41	40	a1i 11	. . . . 5 ⊢ (𝐾 ∈ ℕ → (1^st ‘⟨1, 0⟩) = 1)
42		eqid 2766	. . . . . 6 ⊢ (𝐺 NeighbVtx ⟨1, 0⟩) = (𝐺 NeighbVtx ⟨1, 0⟩)
43	14, 20, 34, 42	gpgnbgrvtx1 48873	. . . . 5 ⊢ (((𝑁 ∈ (ℤ_≥‘3) ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) ∧ (⟨1, 0⟩ ∈ (Vtx‘𝐺) ∧ (1^st ‘⟨1, 0⟩) = 1)) → (𝐺 NeighbVtx ⟨1, 0⟩) = {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩})
44	28, 12, 37, 41, 43	syl22anc 852	. . . 4 ⊢ (𝐾 ∈ ℕ → (𝐺 NeighbVtx ⟨1, 0⟩) = {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩})
45		neeq1 3023	. . . . . 6 ⊢ (𝑏 = ⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ → (𝑏 ≠ 𝑐 ↔ ⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ 𝑐))
46		preq1 4704	. . . . . . 7 ⊢ (𝑏 = ⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ → {𝑏, 𝑐} = {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, 𝑐})
47	46	eleq1d 2851	. . . . . 6 ⊢ (𝑏 = ⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ → ({𝑏, 𝑐} ∈ (Edg‘𝐺) ↔ {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, 𝑐} ∈ (Edg‘𝐺)))
48	45, 47	anbi12d 644	. . . . 5 ⊢ (𝑏 = ⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) ↔ (⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ 𝑐 ∧ {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, 𝑐} ∈ (Edg‘𝐺))))
49		neeq2 3024	. . . . . 6 ⊢ (𝑐 = ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ → (⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ 𝑐 ↔ ⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩))
50		preq2 4705	. . . . . . 7 ⊢ (𝑐 = ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ → {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, 𝑐} = {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩})
51	50	eleq1d 2851	. . . . . 6 ⊢ (𝑐 = ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ → ({⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, 𝑐} ∈ (Edg‘𝐺) ↔ {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩} ∈ (Edg‘𝐺)))
52	49, 51	anbi12d 644	. . . . 5 ⊢ (𝑐 = ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ → ((⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ 𝑐 ∧ {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, 𝑐} ∈ (Edg‘𝐺)) ↔ (⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ∧ {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩} ∈ (Edg‘𝐺))))
53		opex 5450	. . . . . . 7 ⊢ ⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ∈ V
54	53	tpid1 4739	. . . . . 6 ⊢ ⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ∈ {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩}
55		eleq2 2855	. . . . . . 7 ⊢ ((𝐺 NeighbVtx ⟨1, 0⟩) = {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩} → (⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ∈ (𝐺 NeighbVtx ⟨1, 0⟩) ↔ ⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ∈ {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩}))
56	55	adantl 487	. . . . . 6 ⊢ ((𝐾 ∈ ℕ ∧ (𝐺 NeighbVtx ⟨1, 0⟩) = {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩}) → (⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ∈ (𝐺 NeighbVtx ⟨1, 0⟩) ↔ ⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ∈ {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩}))
57	54, 56	mpbiri 261	. . . . 5 ⊢ ((𝐾 ∈ ℕ ∧ (𝐺 NeighbVtx ⟨1, 0⟩) = {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩}) → ⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ∈ (𝐺 NeighbVtx ⟨1, 0⟩))
58		opex 5450	. . . . . . 7 ⊢ ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ∈ V
59	58	tpid3 4744	. . . . . 6 ⊢ ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ∈ {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩}
60		eleq2 2855	. . . . . . 7 ⊢ ((𝐺 NeighbVtx ⟨1, 0⟩) = {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩} → (⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ∈ (𝐺 NeighbVtx ⟨1, 0⟩) ↔ ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ∈ {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩}))
61	60	adantl 487	. . . . . 6 ⊢ ((𝐾 ∈ ℕ ∧ (𝐺 NeighbVtx ⟨1, 0⟩) = {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩}) → (⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ∈ (𝐺 NeighbVtx ⟨1, 0⟩) ↔ ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ∈ {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩}))
62	59, 61	mpbiri 261	. . . . 5 ⊢ ((𝐾 ∈ ℕ ∧ (𝐺 NeighbVtx ⟨1, 0⟩) = {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩}) → ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ∈ (𝐺 NeighbVtx ⟨1, 0⟩))
63	3	gpg3kgrtriexlem5 48885	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ → (𝐾 mod 𝑁) ≠ (-𝐾 mod 𝑁))
64	38, 39	op2nd 8004	. . . . . . . . . . . . 13 ⊢ (2^nd ‘⟨1, 0⟩) = 0
65	64	oveq1i 7433	. . . . . . . . . . . 12 ⊢ ((2^nd ‘⟨1, 0⟩) + 𝐾) = (0 + 𝐾)
66		nncn 12259	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ ℂ)
67	66	addlidd 11429	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℕ → (0 + 𝐾) = 𝐾)
68	65, 67	eqtrid 2813	. . . . . . . . . . 11 ⊢ (𝐾 ∈ ℕ → ((2^nd ‘⟨1, 0⟩) + 𝐾) = 𝐾)
69	68	oveq1d 7438	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ → (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁) = (𝐾 mod 𝑁))
70	64	oveq1i 7433	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘⟨1, 0⟩) − 𝐾) = (0 − 𝐾)
71	70	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℕ → ((2^nd ‘⟨1, 0⟩) − 𝐾) = (0 − 𝐾))
72		df-neg 11462	. . . . . . . . . . . 12 ⊢ -𝐾 = (0 − 𝐾)
73	71, 72	eqtr4di 2819	. . . . . . . . . . 11 ⊢ (𝐾 ∈ ℕ → ((2^nd ‘⟨1, 0⟩) − 𝐾) = -𝐾)
74	73	oveq1d 7438	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ → (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁) = (-𝐾 mod 𝑁))
75	63, 69, 74	3netr4d 3038	. . . . . . . . 9 ⊢ (𝐾 ∈ ℕ → (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁) ≠ (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁))
76	75	olcd 888	. . . . . . . 8 ⊢ (𝐾 ∈ ℕ → (1 ≠ 1 ∨ (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁) ≠ (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)))
77		ovex 7456	. . . . . . . . 9 ⊢ (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁) ∈ V
78	38, 77	opthne 5469	. . . . . . . 8 ⊢ (⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ↔ (1 ≠ 1 ∨ (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁) ≠ (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)))
79	76, 78	sylibr 237	. . . . . . 7 ⊢ (𝐾 ∈ ℕ → ⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩)
80	64	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ ℕ → (2^nd ‘⟨1, 0⟩) = 0)
81	80	oveq1d 7438	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℕ → ((2^nd ‘⟨1, 0⟩) + 𝐾) = (0 + 𝐾))
82	81, 67	eqtrd 2801	. . . . . . . . . . 11 ⊢ (𝐾 ∈ ℕ → ((2^nd ‘⟨1, 0⟩) + 𝐾) = 𝐾)
83	82	oveq1d 7438	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ → (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁) = (𝐾 mod 𝑁))
84	83	opeq2d 4850	. . . . . . . . 9 ⊢ (𝐾 ∈ ℕ → ⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ = ⟨1, (𝐾 mod 𝑁)⟩)
85	80	oveq1d 7438	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℕ → ((2^nd ‘⟨1, 0⟩) − 𝐾) = (0 − 𝐾))
86	85, 72	eqtr4di 2819	. . . . . . . . . . 11 ⊢ (𝐾 ∈ ℕ → ((2^nd ‘⟨1, 0⟩) − 𝐾) = -𝐾)
87	86	oveq1d 7438	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℕ → (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁) = (-𝐾 mod 𝑁))
88	87	opeq2d 4850	. . . . . . . . 9 ⊢ (𝐾 ∈ ℕ → ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ = ⟨1, (-𝐾 mod 𝑁)⟩)
89	84, 88	preq12d 4712	. . . . . . . 8 ⊢ (𝐾 ∈ ℕ → {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩} = {⟨1, (𝐾 mod 𝑁)⟩, ⟨1, (-𝐾 mod 𝑁)⟩})
90		eqid 2766	. . . . . . . . 9 ⊢ {⟨1, (𝐾 mod 𝑁)⟩, ⟨1, (-𝐾 mod 𝑁)⟩} = {⟨1, (𝐾 mod 𝑁)⟩, ⟨1, (-𝐾 mod 𝑁)⟩}
91	3, 20, 90	gpg3kgrtriexlem6 48886	. . . . . . . 8 ⊢ (𝐾 ∈ ℕ → {⟨1, (𝐾 mod 𝑁)⟩, ⟨1, (-𝐾 mod 𝑁)⟩} ∈ (Edg‘𝐺))
92	89, 91	eqeltrd 2866	. . . . . . 7 ⊢ (𝐾 ∈ ℕ → {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩} ∈ (Edg‘𝐺))
93	79, 92	jca 521	. . . . . 6 ⊢ (𝐾 ∈ ℕ → (⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ∧ {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩} ∈ (Edg‘𝐺)))
94	93	adantr 486	. . . . 5 ⊢ ((𝐾 ∈ ℕ ∧ (𝐺 NeighbVtx ⟨1, 0⟩) = {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩}) → (⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩ ≠ ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩ ∧ {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨1, (((2^nd ‘⟨1, 0⟩) − 𝐾) mod 𝑁)⟩} ∈ (Edg‘𝐺)))
95	48, 52, 57, 62, 94	2rspcedvdw 3598	. . . 4 ⊢ ((𝐾 ∈ ℕ ∧ (𝐺 NeighbVtx ⟨1, 0⟩) = {⟨1, (((2^nd ‘⟨1, 0⟩) + 𝐾) mod 𝑁)⟩, ⟨0, (2^nd ‘⟨1, 0⟩)⟩, ⟨1, (((2^nd ‘⟨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 3586	. 2 ⊢ (𝐾 ∈ ℕ → ∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (𝐺 NeighbVtx 𝑎)∃𝑐 ∈ (𝐺 NeighbVtx 𝑎)(𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))
98		gpgusgra 48855	. . . 4 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) → (𝑁 gPetersenGr 𝐾) ∈ USGraph)
99	20, 98	eqeltrid 2870	. . 3 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) → 𝐺 ∈ USGraph)
100		eqid 2766	. . . 4 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
101		eqid 2766	. . . 4 ⊢ (𝐺 NeighbVtx 𝑎) = (𝐺 NeighbVtx 𝑎)
102	34, 100, 101	usgrgrtrirex 48748	. . 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‘𝐺))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∃wex 1812 ∈ wcel 2146 ≠ wne 2961 ∃wrex 3092 {cpr 4596 {ctp 4598 ⟨cop 4600 × cxp 5664 ‘cfv 6543 (class class class)co 7423 1^st c1st 7993 2^nd c2nd 7994 0cc0 11118 1c1 11119 + caddc 11121 · cmul 11123 − cmin 11459 -cneg 11460 / cdiv 11889 ℕcn 12251 2c2 12313 3c3 12314 ℤ_≥cuz 12880 ..^cfzo 13701 ⌈cceil 13844 mod cmo 13922 Vtxcvtx 29376 Edgcedg 29427 USGraphcusgr 29529 NeighbVtx cnbgr 29712 GrTrianglescgrtri 48735 gPetersenGr cgpg 48838

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196

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 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-2o 8463 df-3o 8464 df-oadd 8466 df-er 8703 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-sup 9412 df-inf 9413 df-dju 9906 df-card 9944 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-3 12322 df-4 12323 df-5 12324 df-6 12325 df-7 12326 df-8 12327 df-9 12328 df-n0 12523 df-xnn0 12596 df-z 12610 df-dec 12730 df-uz 12881 df-rp 13035 df-ico 13396 df-fz 13554 df-fzo 13702 df-fl 13845 df-ceil 13846 df-mod 13923 df-hash 14387 df-dvds 16336 df-struct 17232 df-slot 17267 df-ndx 17279 df-base 17295 df-edgf 29369 df-vtx 29378 df-iedg 29379 df-edg 29428 df-uhgr 29438 df-upgr 29462 df-umgr 29463 df-uspgr 29530 df-usgr 29531 df-nbgr 29713 df-grtri 48736 df-gpg 48839

This theorem is used by: (None)

W3C validator