gpg3kgrtriexlem6

Description: Lemma 6 for gpg3kgrtriex : E is an edge in the generalized Petersen graph G(N,K) with N = 3 x. K . (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 \|-
	gpg3kgrtriex.e	$⊢ E = \{⟨1, K \mod N⟩, ⟨1, (- K) \mod N⟩\}$
Assertion	gpg3kgrtriexlem6	$⊢ K \in ℕ \to E \in Edg (G)$

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		gpg3kgrtriex.e	$⊢ E = \{⟨1, K \mod N⟩, ⟨1, (- K) \mod N⟩\}$
4		nnz	$⊢ K \in ℕ \to K \in ℤ$
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		zmodfzo	$⊢ (K \in ℤ \land N \in ℕ) \to K \mod N \in (0 ..^N)$
11	4 9 10	syl2anc	$⊢ K \in ℕ \to K \mod N \in (0 ..^N)$
12		opeq2	$⊢ x = K \mod N \to ⟨0, x⟩ = ⟨0, K \mod N⟩$
13		oveq1	$⊢ x = K \mod N \to x + 1 = (K \mod N) + 1$
14	13	oveq1d	$⊢ x = K \mod N \to (x + 1) \mod N = ((K \mod N) + 1) \mod N$
15	14	opeq2d	$⊢ x = K \mod N \to ⟨0, (x + 1) \mod N⟩ = ⟨0, ((K \mod N) + 1) \mod N⟩$
16	12 15	preq12d	$⊢ x = K \mod N \to \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} = \{⟨0, K \mod N⟩, ⟨0, ((K \mod N) + 1) \mod N⟩\}$
17	16	eqeq2d	$⊢ x = K \mod N \to (E = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \leftrightarrow E = \{⟨0, K \mod N⟩, ⟨0, ((K \mod N) + 1) \mod N⟩\})$
18		opeq2	$⊢ x = K \mod N \to ⟨1, x⟩ = ⟨1, K \mod N⟩$
19	12 18	preq12d	$⊢ x = K \mod N \to \{⟨0, x⟩, ⟨1, x⟩\} = \{⟨0, K \mod N⟩, ⟨1, K \mod N⟩\}$
20	19	eqeq2d	$⊢ x = K \mod N \to (E = \{⟨0, x⟩, ⟨1, x⟩\} \leftrightarrow E = \{⟨0, K \mod N⟩, ⟨1, K \mod N⟩\})$
21		oveq1	$⊢ x = K \mod N \to x + K = (K \mod N) + K$
22	21	oveq1d	$⊢ x = K \mod N \to (x + K) \mod N = ((K \mod N) + K) \mod N$
23	22	opeq2d	$⊢ x = K \mod N \to ⟨1, (x + K) \mod N⟩ = ⟨1, ((K \mod N) + K) \mod N⟩$
24	18 23	preq12d	$⊢ x = K \mod N \to \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} = \{⟨1, K \mod N⟩, ⟨1, ((K \mod N) + K) \mod N⟩\}$
25	24	eqeq2d	$⊢ x = K \mod N \to (E = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\} \leftrightarrow E = \{⟨1, K \mod N⟩, ⟨1, ((K \mod N) + K) \mod N⟩\})$
26	17 20 25	3orbi123d	$⊢ x = K \mod N \to ((E = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor E = \{⟨0, x⟩, ⟨1, x⟩\} \lor E = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (E = \{⟨0, K \mod N⟩, ⟨0, ((K \mod N) + 1) \mod N⟩\} \lor E = \{⟨0, K \mod N⟩, ⟨1, K \mod N⟩\} \lor E = \{⟨1, K \mod N⟩, ⟨1, ((K \mod N) + K) \mod N⟩\}))$
27	26	adantl	$⊢ (K \in ℕ \land x = K \mod N) \to ((E = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor E = \{⟨0, x⟩, ⟨1, x⟩\} \lor E = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}) \leftrightarrow (E = \{⟨0, K \mod N⟩, ⟨0, ((K \mod N) + 1) \mod N⟩\} \lor E = \{⟨0, K \mod N⟩, ⟨1, K \mod N⟩\} \lor E = \{⟨1, K \mod N⟩, ⟨1, ((K \mod N) + K) \mod N⟩\}))$
28	1	gpg3kgrtriexlem2	$⊢ K \in ℕ \to (- K) \mod N = ((K \mod N) + K) \mod N$
29	28	opeq2d	$⊢ K \in ℕ \to ⟨1, (- K) \mod N⟩ = ⟨1, ((K \mod N) + K) \mod N⟩$
30	29	preq2d	$⊢ K \in ℕ \to \{⟨1, K \mod N⟩, ⟨1, (- K) \mod N⟩\} = \{⟨1, K \mod N⟩, ⟨1, ((K \mod N) + K) \mod N⟩\}$
31	3 30	eqtrid	$⊢ K \in ℕ \to E = \{⟨1, K \mod N⟩, ⟨1, ((K \mod N) + K) \mod N⟩\}$
32	31	3mix3d	$⊢ K \in ℕ \to (E = \{⟨0, K \mod N⟩, ⟨0, ((K \mod N) + 1) \mod N⟩\} \lor E = \{⟨0, K \mod N⟩, ⟨1, K \mod N⟩\} \lor E = \{⟨1, K \mod N⟩, ⟨1, ((K \mod N) + K) \mod N⟩\})$
33	11 27 32	rspcedvd	$⊢ K \in ℕ \to \exists x \in (0 ..^N) (E = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor E = \{⟨0, x⟩, ⟨1, x⟩\} \lor E = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\})$
34		3z	$⊢ 3 \in ℤ$
35	34	a1i	$⊢ K \in ℕ \to 3 \in ℤ$
36	35 4	zmulcld	$⊢ K \in ℕ \to 3 K \in ℤ$
37		3t1e3	$⊢ 3 \cdot 1 = 3$
38		nnge1	$⊢ K \in ℕ \to 1 \leq K$
39		1red	$⊢ K \in ℕ \to 1 \in ℝ$
40		nnre	$⊢ K \in ℕ \to K \in ℝ$
41		3re	$⊢ 3 \in ℝ$
42		3pos	$⊢ 0 < 3$
43	41 42	pm3.2i	$⊢ (3 \in ℝ \land 0 < 3)$
44	43	a1i	$⊢ K \in ℕ \to (3 \in ℝ \land 0 < 3)$
45		lemul2	$⊢ (1 \in ℝ \land K \in ℝ \land (3 \in ℝ \land 0 < 3)) \to (1 \leq K \leftrightarrow 3 \cdot 1 \leq 3 K)$
46	39 40 44 45	syl3anc	$⊢ K \in ℕ \to (1 \leq K \leftrightarrow 3 \cdot 1 \leq 3 K)$
47	38 46	mpbid	$⊢ K \in ℕ \to 3 \cdot 1 \leq 3 K$
48	37 47	eqbrtrrid	$⊢ K \in ℕ \to 3 \leq 3 K$
49		eluz2	$⊢ 3 K \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land 3 K \in ℤ \land 3 \leq 3 K)$
50	35 36 48 49	syl3anbrc	$⊢ K \in ℕ \to 3 K \in ℤ_{\geq 3}$
51	1 50	eqeltrid	$⊢ K \in ℕ \to N \in ℤ_{\geq 3}$
52	41	a1i	$⊢ K \in ℕ \to 3 \in ℝ$
53	52 40	remulcld	$⊢ K \in ℕ \to 3 K \in ℝ$
54	1 53	eqeltrid	$⊢ K \in ℕ \to N \in ℝ$
55	54	rehalfcld	$⊢ K \in ℕ \to \frac{N}{2} \in ℝ$
56	55	ceilcld	$⊢ K \in ℕ \to ⌈\frac{N}{2}⌉ \in ℤ$
57	56	zred	$⊢ K \in ℕ \to ⌈\frac{N}{2}⌉ \in ℝ$
58	53	rehalfcld	$⊢ K \in ℕ \to \frac{3 K}{2} \in ℝ$
59	58	ceilcld	$⊢ K \in ℕ \to ⌈\frac{3 K}{2}⌉ \in ℤ$
60	59	zred	$⊢ K \in ℕ \to ⌈\frac{3 K}{2}⌉ \in ℝ$
61		gpg3kgrtriexlem1	$⊢ K \in ℕ \to K < ⌈\frac{3 K}{2}⌉$
62	40 60 61	ltled	$⊢ K \in ℕ \to K \leq ⌈\frac{3 K}{2}⌉$
63	1	oveq1i	$⊢ \frac{N}{2} = \frac{3 K}{2}$
64	63	fveq2i	$⊢ ⌈\frac{N}{2}⌉ = ⌈\frac{3 K}{2}⌉$
65	62 64	breqtrrdi	$⊢ K \in ℕ \to K \leq ⌈\frac{N}{2}⌉$
66	39 40 57 38 65	letrd	$⊢ K \in ℕ \to 1 \leq ⌈\frac{N}{2}⌉$
67		elnnz1	$⊢ ⌈\frac{N}{2}⌉ \in ℕ \leftrightarrow (⌈\frac{N}{2}⌉ \in ℤ \land 1 \leq ⌈\frac{N}{2}⌉)$
68	56 66 67	sylanbrc	$⊢ K \in ℕ \to ⌈\frac{N}{2}⌉ \in ℕ$
69	61 64	breqtrrdi	$⊢ K \in ℕ \to K < ⌈\frac{N}{2}⌉$
70		elfzo1	$⊢ K \in (1 ..^⌈\frac{N}{2}⌉) \leftrightarrow (K \in ℕ \land ⌈\frac{N}{2}⌉ \in ℕ \land K < ⌈\frac{N}{2}⌉)$
71	7 68 69 70	syl3anbrc	$⊢ K \in ℕ \to K \in (1 ..^⌈\frac{N}{2}⌉)$
72		eqid	$⊢ (0 ..^N) = (0 ..^N)$
73		eqid	$⊢ (1 ..^⌈\frac{N}{2}⌉) = (1 ..^⌈\frac{N}{2}⌉)$
74		eqid	$⊢ Edg (G) = Edg (G)$
75	72 73 2 74	gpgedgel	$⊢ (N \in ℤ_{\geq 3} \land K \in (1 ..^⌈\frac{N}{2}⌉)) \to (E \in Edg (G) \leftrightarrow \exists x \in (0 ..^N) (E = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor E = \{⟨0, x⟩, ⟨1, x⟩\} \lor E = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
76	51 71 75	syl2anc	$⊢ K \in ℕ \to (E \in Edg (G) \leftrightarrow \exists x \in (0 ..^N) (E = \{⟨0, x⟩, ⟨0, (x + 1) \mod N⟩\} \lor E = \{⟨0, x⟩, ⟨1, x⟩\} \lor E = \{⟨1, x⟩, ⟨1, (x + K) \mod N⟩\}))$
77	33 76	mpbird	$⊢ K \in ℕ \to E \in Edg (G)$

Metamath Proof Explorer

Theorem gpg3kgrtriexlem6

Proof