pgnbgreunbgrlem2lem1

Description: Lemma 1 for pgnbgreunbgrlem2 . (Contributed by AV, 16-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	pgnbgreunbgrlem2lem1	$⊢ (((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \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		5eluz3	$⊢ 5 \in ℤ_{\geq 3}$
6		pglem	$⊢ 2 \in (1 ..^⌈\frac{5}{2}⌉)$
7	5 6	pm3.2i	$⊢ (5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉))$
8		c0ex	$⊢ 0 \in V$
9		vex	$⊢ y \in V$
10	8 9	op1st	$⊢ 1^{st} (⟨0, y⟩) = 0$
11		simpr	$⊢ ((b \in (0 ..^5) \land y \in (0 ..^5)) \land \{⟨0, y⟩, ⟨0, b⟩\} \in E) \to \{⟨0, y⟩, ⟨0, b⟩\} \in E$
12		eqid	$⊢ (1 ..^⌈\frac{5}{2}⌉) = (1 ..^⌈\frac{5}{2}⌉)$
13	12 1 2 3	gpgvtxedg0	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land 1^{st} (⟨0, y⟩) = 0 \land \{⟨0, y⟩, ⟨0, b⟩\} \in E) \to (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩)$
14	7 10 11 13	mp3an12i	$⊢ ((b \in (0 ..^5) \land y \in (0 ..^5)) \land \{⟨0, y⟩, ⟨0, b⟩\} \in E) \to (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩)$
15	14	ex	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨0, y⟩, ⟨0, b⟩\} \in E \to (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩))$
16		vex	$⊢ b \in V$
17	8 16	op1st	$⊢ 1^{st} (⟨0, b⟩) = 0$
18	12 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	7 17 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 (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 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 (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 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 (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 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 (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 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	8 16	op2nd	$⊢ 2^{nd} (⟨0, b⟩) = b$
30	29	eqeq2i	$⊢ (y + 2) \mod 5 = 2^{nd} (⟨0, b⟩) \leftrightarrow (y + 2) \mod 5 = b$
31		eqcom	$⊢ (y + 2) \mod 5 = b \leftrightarrow b = (y + 2) \mod 5$
32	30 31	bitri	$⊢ (y + 2) \mod 5 = 2^{nd} (⟨0, b⟩) \leftrightarrow b = (y + 2) \mod 5$
33	8 9	op2nd	$⊢ 2^{nd} (⟨0, y⟩) = y$
34	33	oveq1i	$⊢ 2^{nd} (⟨0, y⟩) + 1 = y + 1$
35	34	oveq1i	$⊢ (2^{nd} (⟨0, y⟩) + 1) \mod 5 = (y + 1) \mod 5$
36	35	opeq2i	$⊢ ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ = ⟨0, (y + 1) \mod 5⟩$
37	36	eqeq2i	$⊢ ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \leftrightarrow ⟨0, b⟩ = ⟨0, (y + 1) \mod 5⟩$
38	8 16	opth	$⊢ ⟨0, b⟩ = ⟨0, (y + 1) \mod 5⟩ \leftrightarrow (0 = 0 \land b = (y + 1) \mod 5)$
39	37 38	bitri	$⊢ ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \leftrightarrow (0 = 0 \land b = (y + 1) \mod 5)$
40		eqeq1	$⊢ b = (y + 1) \mod 5 \to (b = (y + 2) \mod 5 \leftrightarrow (y + 1) \mod 5 = (y + 2) \mod 5)$
41	40	adantr	$⊢ (b = (y + 1) \mod 5 \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (b = (y + 2) \mod 5 \leftrightarrow (y + 1) \mod 5 = (y + 2) \mod 5)$
42		eqcom	$⊢ (y + 1) \mod 5 = (y + 2) \mod 5 \leftrightarrow (y + 2) \mod 5 = (y + 1) \mod 5$
43	42	a1i	$⊢ y \in (0 ..^5) \to ((y + 1) \mod 5 = (y + 2) \mod 5 \leftrightarrow (y + 2) \mod 5 = (y + 1) \mod 5)$
44		elfzoelz	$⊢ y \in (0 ..^5) \to y \in ℤ$
45		2z	$⊢ 2 \in ℤ$
46	45	a1i	$⊢ y \in (0 ..^5) \to 2 \in ℤ$
47	44 46	zaddcld	$⊢ y \in (0 ..^5) \to y + 2 \in ℤ$
48		1zzd	$⊢ y \in (0 ..^5) \to 1 \in ℤ$
49	44 48	zaddcld	$⊢ y \in (0 ..^5) \to y + 1 \in ℤ$
50		5nn	$⊢ 5 \in ℕ$
51	50	a1i	$⊢ y \in (0 ..^5) \to 5 \in ℕ$
52		difmod0	$⊢ (y + 2 \in ℤ \land y + 1 \in ℤ \land 5 \in ℕ) \to ((y + 2 - (y + 1)) \mod 5 = 0 \leftrightarrow (y + 2) \mod 5 = (y + 1) \mod 5)$
53	47 49 51 52	syl3anc	$⊢ y \in (0 ..^5) \to ((y + 2 - (y + 1)) \mod 5 = 0 \leftrightarrow (y + 2) \mod 5 = (y + 1) \mod 5)$
54	44	zcnd	$⊢ y \in (0 ..^5) \to y \in ℂ$
55		2cnd	$⊢ y \in (0 ..^5) \to 2 \in ℂ$
56		1cnd	$⊢ y \in (0 ..^5) \to 1 \in ℂ$
57	54 55 56	pnpcand	$⊢ y \in (0 ..^5) \to y + 2 - (y + 1) = 2 - 1$
58		2m1e1	$⊢ 2 - 1 = 1$
59	57 58	eqtrdi	$⊢ y \in (0 ..^5) \to y + 2 - (y + 1) = 1$
60	59	oveq1d	$⊢ y \in (0 ..^5) \to (y + 2 - (y + 1)) \mod 5 = 1 \mod 5$
61	60	eqeq1d	$⊢ y \in (0 ..^5) \to ((y + 2 - (y + 1)) \mod 5 = 0 \leftrightarrow 1 \mod 5 = 0)$
62	43 53 61	3bitr2d	$⊢ y \in (0 ..^5) \to ((y + 1) \mod 5 = (y + 2) \mod 5 \leftrightarrow 1 \mod 5 = 0)$
63		1re	$⊢ 1 \in ℝ$
64		5rp	$⊢ 5 \in ℝ^{+}$
65		0le1	$⊢ 0 \leq 1$
66		1lt5	$⊢ 1 < 5$
67		modid	$⊢ ((1 \in ℝ \land 5 \in ℝ^{+}) \land (0 \leq 1 \land 1 < 5)) \to 1 \mod 5 = 1$
68	63 64 65 66 67	mp4an	$⊢ 1 \mod 5 = 1$
69	68	eqeq1i	$⊢ 1 \mod 5 = 0 \leftrightarrow 1 = 0$
70		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
71	23 70	mpi	$⊢ 1 = 0 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E$
72	69 71	sylbi	$⊢ 1 \mod 5 = 0 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E$
73	62 72	biimtrdi	$⊢ y \in (0 ..^5) \to ((y + 1) \mod 5 = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
74	73	ad2antll	$⊢ (b = (y + 1) \mod 5 \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((y + 1) \mod 5 = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
75	41 74	sylbid	$⊢ (b = (y + 1) \mod 5 \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (b = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
76	75	ex	$⊢ b = (y + 1) \mod 5 \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (b = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
77	39 76	simplbiim	$⊢ ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (b = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
78	8 16	opth	$⊢ ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \leftrightarrow (0 = 1 \land b = 2^{nd} (⟨0, y⟩))$
79		0ne1	$⊢ 0 \neq 1$
80		eqneqall	$⊢ 0 = 1 \to (0 \neq 1 \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (b = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)))$
81	79 80	mpi	$⊢ 0 = 1 \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (b = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
82	81	adantr	$⊢ (0 = 1 \land b = 2^{nd} (⟨0, y⟩)) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (b = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
83	78 82	sylbi	$⊢ ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (b = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
84	33	oveq1i	$⊢ 2^{nd} (⟨0, y⟩) - 1 = y - 1$
85	84	oveq1i	$⊢ (2^{nd} (⟨0, y⟩) - 1) \mod 5 = (y - 1) \mod 5$
86	85	opeq2i	$⊢ ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩ = ⟨0, (y - 1) \mod 5⟩$
87	86	eqeq2i	$⊢ ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩ \leftrightarrow ⟨0, b⟩ = ⟨0, (y - 1) \mod 5⟩$
88	8 16	opth	$⊢ ⟨0, b⟩ = ⟨0, (y - 1) \mod 5⟩ \leftrightarrow (0 = 0 \land b = (y - 1) \mod 5)$
89		eqeq1	$⊢ b = (y - 1) \mod 5 \to (b = (y + 2) \mod 5 \leftrightarrow (y - 1) \mod 5 = (y + 2) \mod 5)$
90	89	adantr	$⊢ (b = (y - 1) \mod 5 \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (b = (y + 2) \mod 5 \leftrightarrow (y - 1) \mod 5 = (y + 2) \mod 5)$
91	44 48	zsubcld	$⊢ y \in (0 ..^5) \to y - 1 \in ℤ$
92		difmod0	$⊢ (y - 1 \in ℤ \land y + 2 \in ℤ \land 5 \in ℕ) \to ((y - 1 - (y + 2)) \mod 5 = 0 \leftrightarrow (y - 1) \mod 5 = (y + 2) \mod 5)$
93	92	bicomd	$⊢ (y - 1 \in ℤ \land y + 2 \in ℤ \land 5 \in ℕ) \to ((y - 1) \mod 5 = (y + 2) \mod 5 \leftrightarrow (y - 1 - (y + 2)) \mod 5 = 0)$
94	91 47 51 93	syl3anc	$⊢ y \in (0 ..^5) \to ((y - 1) \mod 5 = (y + 2) \mod 5 \leftrightarrow (y - 1 - (y + 2)) \mod 5 = 0)$
95	54 56 54 55	subsubadd23	$⊢ y \in (0 ..^5) \to y - 1 - (y + 2) = y - y - (1 + 2)$
96	54	subidd	$⊢ y \in (0 ..^5) \to y - y = 0$
97		1p2e3	$⊢ 1 + 2 = 3$
98	97	a1i	$⊢ y \in (0 ..^5) \to 1 + 2 = 3$
99	96 98	oveq12d	$⊢ y \in (0 ..^5) \to y - y - (1 + 2) = 0 - 3$
100		df-neg	$⊢ - 3 = 0 - 3$
101	99 100	eqtr4di	$⊢ y \in (0 ..^5) \to y - y - (1 + 2) = - 3$
102	95 101	eqtrd	$⊢ y \in (0 ..^5) \to y - 1 - (y + 2) = - 3$
103	102	oveq1d	$⊢ y \in (0 ..^5) \to (y - 1 - (y + 2)) \mod 5 = -3 \mod 5$
104	103	eqeq1d	$⊢ y \in (0 ..^5) \to ((y - 1 - (y + 2)) \mod 5 = 0 \leftrightarrow -3 \mod 5 = 0)$
105		3re	$⊢ 3 \in ℝ$
106		negmod0	$⊢ (3 \in ℝ \land 5 \in ℝ^{+}) \to (3 \mod 5 = 0 \leftrightarrow -3 \mod 5 = 0)$
107	105 64 106	mp2an	$⊢ 3 \mod 5 = 0 \leftrightarrow -3 \mod 5 = 0$
108		0re	$⊢ 0 \in ℝ$
109		3pos	$⊢ 0 < 3$
110	108 105 109	ltleii	$⊢ 0 \leq 3$
111		3lt5	$⊢ 3 < 5$
112		modid	$⊢ ((3 \in ℝ \land 5 \in ℝ^{+}) \land (0 \leq 3 \land 3 < 5)) \to 3 \mod 5 = 3$
113	105 64 110 111 112	mp4an	$⊢ 3 \mod 5 = 3$
114	113	eqeq1i	$⊢ 3 \mod 5 = 0 \leftrightarrow 3 = 0$
115		3ne0	$⊢ 3 \neq 0$
116		eqneqall	$⊢ 3 = 0 \to (3 \neq 0 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
117	115 116	mpi	$⊢ 3 = 0 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E$
118	114 117	sylbi	$⊢ 3 \mod 5 = 0 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E$
119	107 118	sylbir	$⊢ -3 \mod 5 = 0 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E$
120	104 119	biimtrdi	$⊢ y \in (0 ..^5) \to ((y - 1 - (y + 2)) \mod 5 = 0 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
121	94 120	sylbid	$⊢ y \in (0 ..^5) \to ((y - 1) \mod 5 = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
122	121	ad2antll	$⊢ (b = (y - 1) \mod 5 \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((y - 1) \mod 5 = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
123	90 122	sylbid	$⊢ (b = (y - 1) \mod 5 \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (b = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
124	123	ex	$⊢ b = (y - 1) \mod 5 \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (b = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
125	88 124	simplbiim	$⊢ ⟨0, b⟩ = ⟨0, (y - 1) \mod 5⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (b = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
126	87 125	sylbi	$⊢ ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (b = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
127	77 83 126	3jaoi	$⊢ (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (b = (y + 2) \mod 5 \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
128	127	com13	$⊢ b = (y + 2) \mod 5 \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
129	128	impd	$⊢ b = (y + 2) \mod 5 \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
130	32 129	sylbi	$⊢ (y + 2) \mod 5 = 2^{nd} (⟨0, b⟩) \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
131	28 130	simplbiim	$⊢ ⟨1, (y + 2) \mod 5⟩ = ⟨1, 2^{nd} (⟨0, b⟩)⟩ \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
132	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)$
133	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 (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
134	132 133	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 (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
135	27 131 134	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 (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
136	19 135	syl	$⊢ \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
137		ax-1	$⊢ \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E \to (((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
138	136 137	pm2.61i	$⊢ ((b \in (0 ..^5) \land y \in (0 ..^5)) \land (⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩)) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E$
139	138	ex	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) + 1) \mod 5⟩ \lor ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \lor ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩) \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
140	15 139	syld	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨0, y⟩, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
141	140	adantl	$⊢ ((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{⟨0, y⟩, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
142		preq1	$⊢ K = ⟨0, y⟩ \to \{K, ⟨0, b⟩\} = \{⟨0, y⟩, ⟨0, b⟩\}$
143	142	eleq1d	$⊢ K = ⟨0, y⟩ \to (\{K, ⟨0, b⟩\} \in E \leftrightarrow \{⟨0, y⟩, ⟨0, b⟩\} \in E)$
144	143	adantl	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \to (\{K, ⟨0, b⟩\} \in E \leftrightarrow \{⟨0, y⟩, ⟨0, b⟩\} \in E)$
145		preq2	$⊢ L = ⟨1, (y + 2) \mod 5⟩ \to \{⟨0, b⟩, L\} = \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\}$
146	145	eleq1d	$⊢ L = ⟨1, (y + 2) \mod 5⟩ \to (\{⟨0, b⟩, L\} \in E \leftrightarrow \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
147	146	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)$
148	147	adantr	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \to (\neg \{⟨0, b⟩, L\} \in E \leftrightarrow \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
149	144 148	imbi12d	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \to ((\{K, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, L\} \in E) \leftrightarrow (\{⟨0, y⟩, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
150	149	adantr	$⊢ ((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, L\} \in E) \leftrightarrow (\{⟨0, y⟩, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
151	141 150	mpbird	$⊢ ((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{K, ⟨0, b⟩\} \in E \to \neg \{⟨0, b⟩, L\} \in E)$
152	151	imp	$⊢ (((L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \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 pgnbgreunbgrlem2lem1

Proof