pgnbgreunbgrlem2lem3

Description: Lemma 3 for pgnbgreunbgrlem2 . (Contributed by AV, 17-Nov-2025)

	Ref	Expression
Hypotheses	pgnbgreunbgr.g	No typesetting found for \|- G = ( 5 gPetersenGr 2 ) with typecode \|-
	pgnbgreunbgr.v	$⊢ V = Vtx (G)$
	pgnbgreunbgr.e	$⊢ E = Edg (G)$
	pgnbgreunbgr.n	$⊢ N = G NeighbVtx X$
Assertion	pgnbgreunbgrlem2lem3	$⊢ (((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨0, b⟩\} \in E) \to \neg \{⟨0, b⟩, L\} \in E$

Proof

Step	Hyp	Ref	Expression
1		pgnbgreunbgr.g	Could not format G = ( 5 gPetersenGr 2 ) : No typesetting found for \|- G = ( 5 gPetersenGr 2 ) with typecode \|-
2		pgnbgreunbgr.v	$⊢ V = Vtx (G)$
3		pgnbgreunbgr.e	$⊢ E = Edg (G)$
4		pgnbgreunbgr.n	$⊢ N = G NeighbVtx X$
5		prcom	$⊢ \{⟨1, (y - 2) \mod 5⟩, ⟨0, b⟩\} = \{⟨0, b⟩, ⟨1, (y - 2) \mod 5⟩\}$
6	5	eleq1i	$⊢ \{⟨1, (y - 2) \mod 5⟩, ⟨0, b⟩\} \in E \leftrightarrow \{⟨0, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E$
7	6	a1i	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨1, (y - 2) \mod 5⟩, ⟨0, b⟩\} \in E \leftrightarrow \{⟨0, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E)$
8		5eluz3	$⊢ 5 \in ℤ_{\geq 3}$
9		pglem	$⊢ 2 \in (1 ..^⌈\frac{5}{2}⌉)$
10	8 9	pm3.2i	$⊢ (5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉))$
11		c0ex	$⊢ 0 \in V$
12		vex	$⊢ b \in V$
13	11 12	op1st	$⊢ 1^{st} (⟨0, b⟩) = 0$
14		eqid	$⊢ (1 ..^⌈\frac{5}{2}⌉) = (1 ..^⌈\frac{5}{2}⌉)$
15	14 1 2 3	gpgvtxedg0	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land 1^{st} (⟨0, b⟩) = 0 \land \{⟨0, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E) \to (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)$
16	10 13 15	mp3an12	$⊢ \{⟨0, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E \to (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)$
17	7 16	biimtrdi	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨1, (y - 2) \mod 5⟩, ⟨0, b⟩\} \in E \to (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩))$
18	14 1 2 3	gpgvtxedg0	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land 1^{st} (⟨0, b⟩) = 0 \land \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E) \to (⟨1, (y + 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y + 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y + 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)$
19	10 13 18	mp3an12	$⊢ \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E \to (⟨1, (y + 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y + 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y + 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)$
20		1ex	$⊢ 1 \in V$
21		ovex	$⊢ (y + 2) \mod 5 \in V$
22	20 21	opth	$⊢ ⟨1, (y + 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \leftrightarrow (1 = 0 \land (y + 2) \mod 5 = (2^{nd} (⟨0, b⟩) + 1) \mod 5)$
23		ax-1ne0	$⊢ 1 \neq 0$
24		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
25	23 24	mpi	$⊢ 1 = 0 \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
26	25	adantr	$⊢ (1 = 0 \land (y + 2) \mod 5 = (2^{nd} (⟨0, b⟩) + 1) \mod 5) \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
27	22 26	sylbi	$⊢ ⟨1, (y + 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
28	20 21	opth	$⊢ ⟨1, (y + 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \leftrightarrow (1 = 1 \land (y + 2) \mod 5 = 2^{nd} (⟨0, b⟩))$
29	11 12	op2nd	$⊢ 2^{nd} (⟨0, b⟩) = b$
30	29	eqeq2i	$⊢ (y + 2) \mod 5 = 2^{nd} (⟨0, b⟩) \leftrightarrow (y + 2) \mod 5 = b$
31		ovex	$⊢ (y - 2) \mod 5 \in V$
32	20 31	opth	$⊢ ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \leftrightarrow (1 = 0 \land (y - 2) \mod 5 = (2^{nd} (⟨0, b⟩) + 1) \mod 5)$
33		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((y + 2) \mod 5 = b \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)))$
34	23 33	mpi	$⊢ 1 = 0 \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((y + 2) \mod 5 = b \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
35	34	adantr	$⊢ (1 = 0 \land (y - 2) \mod 5 = (2^{nd} (⟨0, b⟩) + 1) \mod 5) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((y + 2) \mod 5 = b \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
36	32 35	sylbi	$⊢ ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((y + 2) \mod 5 = b \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
37	20 31	opth	$⊢ ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \leftrightarrow (1 = 1 \land (y - 2) \mod 5 = 2^{nd} (⟨0, b⟩))$
38	29	eqeq2i	$⊢ (y - 2) \mod 5 = 2^{nd} (⟨0, b⟩) \leftrightarrow (y - 2) \mod 5 = b$
39		eqeq2	$⊢ b = (y - 2) \mod 5 \to ((y + 2) \mod 5 = b \leftrightarrow (y + 2) \mod 5 = (y - 2) \mod 5)$
40	39	eqcoms	$⊢ (y - 2) \mod 5 = b \to ((y + 2) \mod 5 = b \leftrightarrow (y + 2) \mod 5 = (y - 2) \mod 5)$
41	40	adantl	$⊢ (y \in (0 ..^5) \land (y - 2) \mod 5 = b) \to ((y + 2) \mod 5 = b \leftrightarrow (y + 2) \mod 5 = (y - 2) \mod 5)$
42		elfzoelz	$⊢ y \in (0 ..^5) \to y \in ℤ$
43		2z	$⊢ 2 \in ℤ$
44	43	a1i	$⊢ y \in (0 ..^5) \to 2 \in ℤ$
45	42 44	zaddcld	$⊢ y \in (0 ..^5) \to y + 2 \in ℤ$
46	42 44	zsubcld	$⊢ y \in (0 ..^5) \to y - 2 \in ℤ$
47		5nn	$⊢ 5 \in ℕ$
48	47	a1i	$⊢ y \in (0 ..^5) \to 5 \in ℕ$
49		difmod0	$⊢ (y + 2 \in ℤ \land y - 2 \in ℤ \land 5 \in ℕ) \to ((y + 2 - (y - 2)) \mod 5 = 0 \leftrightarrow (y + 2) \mod 5 = (y - 2) \mod 5)$
50	49	bicomd	$⊢ (y + 2 \in ℤ \land y - 2 \in ℤ \land 5 \in ℕ) \to ((y + 2) \mod 5 = (y - 2) \mod 5 \leftrightarrow (y + 2 - (y - 2)) \mod 5 = 0)$
51	45 46 48 50	syl3anc	$⊢ y \in (0 ..^5) \to ((y + 2) \mod 5 = (y - 2) \mod 5 \leftrightarrow (y + 2 - (y - 2)) \mod 5 = 0)$
52	42	zcnd	$⊢ y \in (0 ..^5) \to y \in ℂ$
53		2cnd	$⊢ y \in (0 ..^5) \to 2 \in ℂ$
54	52 53 53	pnncand	$⊢ y \in (0 ..^5) \to y + 2 - (y - 2) = 2 + 2$
55		2p2e4	$⊢ 2 + 2 = 4$
56	54 55	eqtrdi	$⊢ y \in (0 ..^5) \to y + 2 - (y - 2) = 4$
57	56	oveq1d	$⊢ y \in (0 ..^5) \to (y + 2 - (y - 2)) \mod 5 = 4 \mod 5$
58	57	eqeq1d	$⊢ y \in (0 ..^5) \to ((y + 2 - (y - 2)) \mod 5 = 0 \leftrightarrow 4 \mod 5 = 0)$
59		4re	$⊢ 4 \in ℝ$
60		5rp	$⊢ 5 \in ℝ^{+}$
61		0re	$⊢ 0 \in ℝ$
62		4pos	$⊢ 0 < 4$
63	61 59 62	ltleii	$⊢ 0 \leq 4$
64		4lt5	$⊢ 4 < 5$
65		modid	$⊢ ((4 \in ℝ \land 5 \in ℝ^{+}) \land (0 \leq 4 \land 4 < 5)) \to 4 \mod 5 = 4$
66	59 60 63 64 65	mp4an	$⊢ 4 \mod 5 = 4$
67	66	eqeq1i	$⊢ 4 \mod 5 = 0 \leftrightarrow 4 = 0$
68		4ne0	$⊢ 4 \neq 0$
69	68	a1i	$⊢ \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E \to 4 \neq 0$
70	69	necon2bi	$⊢ 4 = 0 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E$
71	67 70	sylbi	$⊢ 4 \mod 5 = 0 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E$
72	58 71	biimtrdi	$⊢ y \in (0 ..^5) \to ((y + 2 - (y - 2)) \mod 5 = 0 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
73	51 72	sylbid	$⊢ y \in (0 ..^5) \to ((y + 2) \mod 5 = (y - 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
74	73	adantr	$⊢ (y \in (0 ..^5) \land (y - 2) \mod 5 = b) \to ((y + 2) \mod 5 = (y - 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
75	41 74	sylbid	$⊢ (y \in (0 ..^5) \land (y - 2) \mod 5 = b) \to ((y + 2) \mod 5 = b \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
76	75	ex	$⊢ y \in (0 ..^5) \to ((y - 2) \mod 5 = b \to ((y + 2) \mod 5 = b \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
77	76	adantl	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((y - 2) \mod 5 = b \to ((y + 2) \mod 5 = b \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
78	77	com12	$⊢ (y - 2) \mod 5 = b \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((y + 2) \mod 5 = b \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
79	38 78	sylbi	$⊢ (y - 2) \mod 5 = 2^{nd} (⟨0, b⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((y + 2) \mod 5 = b \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
80	37 79	simplbiim	$⊢ ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((y + 2) \mod 5 = b \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
81	20 31	opth	$⊢ ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩ \leftrightarrow (1 = 0 \land (y - 2) \mod 5 = (2^{nd} (⟨0, b⟩) - 1) \mod 5)$
82	34	adantr	$⊢ (1 = 0 \land (y - 2) \mod 5 = (2^{nd} (⟨0, b⟩) - 1) \mod 5) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((y + 2) \mod 5 = b \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
83	81 82	sylbi	$⊢ ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((y + 2) \mod 5 = b \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
84	36 80 83	3jaoi	$⊢ (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((y + 2) \mod 5 = b \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
85	84	com13	$⊢ (y + 2) \mod 5 = b \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
86	85	impd	$⊢ (y + 2) \mod 5 = b \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
87	30 86	sylbi	$⊢ (y + 2) \mod 5 = 2^{nd} (⟨0, b⟩) \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
88	28 87	simplbiim	$⊢ ⟨1, (y + 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
89	20 21	opth	$⊢ ⟨1, (y + 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩ \leftrightarrow (1 = 0 \land (y + 2) \mod 5 = (2^{nd} (⟨0, b⟩) - 1) \mod 5)$
90	25	adantr	$⊢ (1 = 0 \land (y + 2) \mod 5 = (2^{nd} (⟨0, b⟩) - 1) \mod 5) \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
91	89 90	sylbi	$⊢ ⟨1, (y + 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩ \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
92	27 88 91	3jaoi	$⊢ (⟨1, (y + 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y + 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y + 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩) \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
93	19 92	syl	$⊢ \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
94		ax-1	$⊢ \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
95	93 94	pm2.61i	$⊢ ((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E$
96	95	ex	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) + 1) \mod 5⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \lor ⟨1, (y - 2) \mod 5⟩ = ⟨0, (2^{nd} (⟨0, b⟩) - 1) \mod 5⟩) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
97	17 96	syld	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨1, (y - 2) \mod 5⟩, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
98	97	adantl	$⊢ ((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{⟨1, (y - 2) \mod 5⟩, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
99		preq1	$⊢ K = ⟨1, (y - 2) \mod 5⟩ \to \{K, ⟨0, b⟩\} = \{⟨1, (y - 2) \mod 5⟩, ⟨0, b⟩\}$
100	99	eleq1d	$⊢ K = ⟨1, (y - 2) \mod 5⟩ \to (\{K, ⟨0, b⟩\} \in E \leftrightarrow \{⟨1, (y - 2) \mod 5⟩, ⟨0, b⟩\} \in E)$
101	100	adantl	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to (\{K, ⟨0, b⟩\} \in E \leftrightarrow \{⟨1, (y - 2) \mod 5⟩, ⟨0, b⟩\} \in E)$
102		preq2	$⊢ L = ⟨1, (y + 2) \mod 5⟩ \to \{⟨0, b⟩, L\} = \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\}$
103	102	eleq1d	$⊢ L = ⟨1, (y + 2) \mod 5⟩ \to (\{⟨0, b⟩, L\} \in E \leftrightarrow \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
104	103	notbid	$⊢ L = ⟨1, (y + 2) \mod 5⟩ \to (\neg \{⟨0, b⟩, L\} \in E \leftrightarrow \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
105	104	adantr	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to (\neg \{⟨0, b⟩, L\} \in E \leftrightarrow \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
106	101 105	imbi12d	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to ((\{K, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, L\} \in E) \leftrightarrow (\{⟨1, (y - 2) \mod 5⟩, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
107	106	adantr	$⊢ ((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, L\} \in E) \leftrightarrow (\{⟨1, (y - 2) \mod 5⟩, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
108	98 107	mpbird	$⊢ ((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{K, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, L\} \in E)$
109	108	imp	$⊢ (((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \land \{K, ⟨0, b⟩\} \in E) \to \neg \{⟨0, b⟩, L\} \in E$

Metamath Proof Explorer

Theorem pgnbgreunbgrlem2lem3

Proof