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		1elpr01	$⊢ 1 \in \{0, 1\}$
4	3	a1i	$⊢ K \in ℕ \to 1 \in \{0, 1\}$
5		3nn	$⊢ 3 \in ℕ$
6	5	a1i	$⊢ K \in ℕ \to 3 \in ℕ$
7		id	$⊢ K \in ℕ \to K \in ℕ$
8	6 7	nnmulcld	$⊢ K \in ℕ \to 3 K \in ℕ$
9	1 8	eqeltrid	$⊢ K \in ℕ \to N \in ℕ$
10		lbfzo0	$⊢ 0 \in (0 ..^N) \leftrightarrow N \in ℕ$
11	9 10	sylibr	$⊢ K \in ℕ \to 0 \in (0 ..^N)$
12	4 11	opelxpd	$⊢ K \in ℕ \to ⟨1, 0⟩ \in (\{0, 1\} \times (0 ..^N))$
13	1	gpg3kgrtriexlem4	$⊢ K \in ℕ \to K \in (1 ..^⌈\frac{N}{2}⌉)$
14	9 13	jca	$⊢ K \in ℕ \to (N \in ℕ \land K \in (1 ..^⌈\frac{N}{2}⌉))$
15		eqid	$⊢ (1 ..^⌈\frac{N}{2}⌉) = (1 ..^⌈\frac{N}{2}⌉)$
16		eqid	$⊢ (0 ..^N) = (0 ..^N)$
17	15 16	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 \|-
18	17	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 \|-
19	14 18	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 \|-
20	12 19	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 \|-
21	2	fveq2i	Could not format ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) ) : No typesetting found for \|- ( Vtx ` G ) = ( Vtx ` ( N gPetersenGr K ) ) with typecode \|-
22	20 21	eleqtrrdi	$⊢ K \in ℕ \to ⟨1, 0⟩ \in Vtx (G)$
23		oveq2	$⊢ a = ⟨1, 0⟩ \to G NeighbVtx a = G NeighbVtx ⟨1, 0⟩$
24		biidd	$⊢ a = ⟨1, 0⟩ \to ((b \neq c \land \{b, c\} \in Edg (G)) \leftrightarrow (b \neq c \land \{b, c\} \in Edg (G)))$
25	23 24	rexeqbidv	$⊢ a = ⟨1, 0⟩ \to (\exists c \in (G NeighbVtx a) (b \neq c \land \{b, c\} \in Edg (G)) \leftrightarrow \exists c \in (G NeighbVtx ⟨1, 0⟩) (b \neq c \land \{b, c\} \in Edg (G)))$
26	23 25	rexeqbidv	$⊢ a = ⟨1, 0⟩ \to (\exists b \in (G NeighbVtx a) \exists c \in (G NeighbVtx a) (b \neq c \land \{b, c\} \in Edg (G)) \leftrightarrow \exists b \in (G NeighbVtx ⟨1, 0⟩) \exists c \in (G NeighbVtx ⟨1, 0⟩) (b \neq c \land \{b, c\} \in Edg (G)))$
27	26	adantl	$⊢ (K \in ℕ \land a = ⟨1, 0⟩) \to (\exists b \in (G NeighbVtx a) \exists c \in (G NeighbVtx a) (b \neq c \land \{b, c\} \in Edg (G)) \leftrightarrow \exists b \in (G NeighbVtx ⟨1, 0⟩) \exists c \in (G NeighbVtx ⟨1, 0⟩) (b \neq c \land \{b, c\} \in Edg (G)))$
28	1	gpg3kgrtriexlem3	$⊢ K \in ℕ \to N \in ℤ_{\geq 3}$
29		eqid	$⊢ 1 = 1$
30	29	a1i	$⊢ K \in ℕ \to 1 = 1$
31	30	olcd	$⊢ K \in ℕ \to (1 = 0 \lor 1 = 1)$
32	31 11	jca	$⊢ K \in ℕ \to ((1 = 0 \lor 1 = 1) \land 0 \in (0 ..^N))$
33	28 13	jca	$⊢ K \in ℕ \to (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉))$
34		eqid	$⊢ Vtx (G) = Vtx (G)$
35	16 15 2 34	opgpgvtx	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to (⟨1, 0⟩ \in Vtx (G) \leftrightarrow ((1 = 0 \lor 1 = 1) \land 0 \in (0 ..^N)))$
36	33 35	syl	$⊢ K \in ℕ \to (⟨1, 0⟩ \in Vtx (G) \leftrightarrow ((1 = 0 \lor 1 = 1) \land 0 \in (0 ..^N)))$
37	32 36	mpbird	$⊢ K \in ℕ \to ⟨1, 0⟩ \in Vtx (G)$
38		1ex	$⊢ 1 \in V$
39		c0ex	$⊢ 0 \in V$
40	38 39	op1st	$⊢ 1^{st} (⟨1, 0⟩) = 1$
41	40	a1i	$⊢ K \in ℕ \to 1^{st} (⟨1, 0⟩) = 1$
42		eqid	$⊢ G NeighbVtx ⟨1, 0⟩ = G NeighbVtx ⟨1, 0⟩$
43	15 2 34 42	gpgnbgrvtx1	$⊢ ((N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \land (⟨1, 0⟩ \in Vtx (G) \land 1^{st} (⟨1, 0⟩) = 1)) \to 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	28 13 37 41 43	syl22anc	$⊢ K \in ℕ \to 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⟩ \to (b \neq c \leftrightarrow ⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \neq c)$
46		preq1	$⊢ b = ⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \to \{b, c\} = \{⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩, c\}$
47	46	eleq1d	$⊢ b = ⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \to (\{b, c\} \in Edg (G) \leftrightarrow \{⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩, c\} \in Edg (G))$
48	45 47	anbi12d	$⊢ b = ⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \to ((b \neq c \land \{b, c\} \in Edg (G)) \leftrightarrow (⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \neq c \land \{⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩, c\} \in Edg (G)))$
49		neeq2	$⊢ c = ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \to (⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \neq c \leftrightarrow ⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \neq ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩)$
50		preq2	$⊢ c = ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \to \{⟨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⟩ \to (\{⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩, c\} \in Edg (G) \leftrightarrow \{⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩, ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩\} \in Edg (G))$
52	49 51	anbi12d	$⊢ c = ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \to ((⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \neq c \land \{⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩, c\} \in Edg (G)) \leftrightarrow (⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \neq ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \land \{⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩, ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩\} \in Edg (G)))$
53		opex	$⊢ ⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \in V$
54	53	tpid1	$⊢ ⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \in \{⟨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⟩\} \to (⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \in (G NeighbVtx ⟨1, 0⟩) \leftrightarrow ⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \in \{⟨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 \in ℕ \land 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⟩\}) \to (⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \in (G NeighbVtx ⟨1, 0⟩) \leftrightarrow ⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \in \{⟨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 \in ℕ \land 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⟩\}) \to ⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \in (G NeighbVtx ⟨1, 0⟩)$
58		opex	$⊢ ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \in V$
59	58	tpid3	$⊢ ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \in \{⟨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⟩\} \to (⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \in (G NeighbVtx ⟨1, 0⟩) \leftrightarrow ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \in \{⟨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 \in ℕ \land 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⟩\}) \to (⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \in (G NeighbVtx ⟨1, 0⟩) \leftrightarrow ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \in \{⟨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 \in ℕ \land 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⟩\}) \to ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \in (G NeighbVtx ⟨1, 0⟩)$
63	1	gpg3kgrtriexlem5	$⊢ K \in ℕ \to K \mod N \neq (- K) \mod N$
64	38 39	op2nd	$⊢ 2^{nd} (⟨1, 0⟩) = 0$
65	64	oveq1i	$⊢ 2^{nd} (⟨1, 0⟩) + K = 0 + K$
66		nncn	$⊢ K \in ℕ \to K \in ℂ$
67	66	addlidd	$⊢ K \in ℕ \to 0 + K = K$
68	65 67	eqtrid	$⊢ K \in ℕ \to 2^{nd} (⟨1, 0⟩) + K = K$
69	68	oveq1d	$⊢ K \in ℕ \to (2^{nd} (⟨1, 0⟩) + K) \mod N = K \mod N$
70	64	oveq1i	$⊢ 2^{nd} (⟨1, 0⟩) - K = 0 - K$
71	70	a1i	$⊢ K \in ℕ \to 2^{nd} (⟨1, 0⟩) - K = 0 - K$
72		df-neg	$⊢ - K = 0 - K$
73	71 72	eqtr4di	$⊢ K \in ℕ \to 2^{nd} (⟨1, 0⟩) - K = - K$
74	73	oveq1d	$⊢ K \in ℕ \to (2^{nd} (⟨1, 0⟩) - K) \mod N = (- K) \mod N$
75	63 69 74	3netr4d	$⊢ K \in ℕ \to (2^{nd} (⟨1, 0⟩) + K) \mod N \neq (2^{nd} (⟨1, 0⟩) - K) \mod N$
76	75	olcd	$⊢ K \in ℕ \to (1 \neq 1 \lor (2^{nd} (⟨1, 0⟩) + K) \mod N \neq (2^{nd} (⟨1, 0⟩) - K) \mod N)$
77		ovex	$⊢ (2^{nd} (⟨1, 0⟩) + K) \mod N \in V$
78	38 77	opthne	$⊢ ⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \neq ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \leftrightarrow (1 \neq 1 \lor (2^{nd} (⟨1, 0⟩) + K) \mod N \neq (2^{nd} (⟨1, 0⟩) - K) \mod N)$
79	76 78	sylibr	$⊢ K \in ℕ \to ⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \neq ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩$
80	64	a1i	$⊢ K \in ℕ \to 2^{nd} (⟨1, 0⟩) = 0$
81	80	oveq1d	$⊢ K \in ℕ \to 2^{nd} (⟨1, 0⟩) + K = 0 + K$
82	81 67	eqtrd	$⊢ K \in ℕ \to 2^{nd} (⟨1, 0⟩) + K = K$
83	82	oveq1d	$⊢ K \in ℕ \to (2^{nd} (⟨1, 0⟩) + K) \mod N = K \mod N$
84	83	opeq2d	$⊢ K \in ℕ \to ⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ = ⟨1, K \mod N⟩$
85	80	oveq1d	$⊢ K \in ℕ \to 2^{nd} (⟨1, 0⟩) - K = 0 - K$
86	85 72	eqtr4di	$⊢ K \in ℕ \to 2^{nd} (⟨1, 0⟩) - K = - K$
87	86	oveq1d	$⊢ K \in ℕ \to (2^{nd} (⟨1, 0⟩) - K) \mod N = (- K) \mod N$
88	87	opeq2d	$⊢ K \in ℕ \to ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ = ⟨1, (- K) \mod N⟩$
89	84 88	preq12d	$⊢ K \in ℕ \to \{⟨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 \in ℕ \to \{⟨1, K \mod N⟩, ⟨1, (- K) \mod N⟩\} \in Edg (G)$
92	89 91	eqeltrd	$⊢ K \in ℕ \to \{⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩, ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩\} \in Edg (G)$
93	79 92	jca	$⊢ K \in ℕ \to (⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \neq ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \land \{⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩, ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩\} \in Edg (G))$
94	93	adantr	$⊢ (K \in ℕ \land 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⟩\}) \to (⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩ \neq ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩ \land \{⟨1, (2^{nd} (⟨1, 0⟩) + K) \mod N⟩, ⟨1, (2^{nd} (⟨1, 0⟩) - K) \mod N⟩\} \in Edg (G))$
95	48 52 57 62 94	2rspcedvdw	$⊢ (K \in ℕ \land 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⟩\}) \to \exists b \in (G NeighbVtx ⟨1, 0⟩) \exists c \in (G NeighbVtx ⟨1, 0⟩) (b \neq c \land \{b, c\} \in Edg (G))$
96	44 95	mpdan	$⊢ K \in ℕ \to \exists b \in (G NeighbVtx ⟨1, 0⟩) \exists c \in (G NeighbVtx ⟨1, 0⟩) (b \neq c \land \{b, c\} \in Edg (G))$
97	22 27 96	rspcedvd	$⊢ K \in ℕ \to \exists a \in Vtx (G) \exists b \in (G NeighbVtx a) \exists c \in (G NeighbVtx a) (b \neq c \land \{b, c\} \in 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 \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to G \in USGraph$
100		eqid	$⊢ Edg (G) = Edg (G)$
101		eqid	$⊢ G NeighbVtx a = G NeighbVtx a$
102	34 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	33 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 \|-

Metamath Proof Explorer

Theorem gpg3kgrtriex

Proof