pgnbgreunbgrlem2lem2

Description: Lemma 2 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	pgnbgreunbgrlem2lem2	$⊢ (((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	zsubcld	$⊢ y \in (0 ..^5) \to y - 2 \in ℤ$
48	44	peano2zd	$⊢ y \in (0 ..^5) \to y + 1 \in ℤ$
49		5nn	$⊢ 5 \in ℕ$
50	49	a1i	$⊢ y \in (0 ..^5) \to 5 \in ℕ$
51		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)$
52	47 48 50 51	syl3anc	$⊢ y \in (0 ..^5) \to ((y - 2 - (y + 1)) \mod 5 = 0 \leftrightarrow (y - 2) \mod 5 = (y + 1) \mod 5)$
53	44	zcnd	$⊢ y \in (0 ..^5) \to y \in ℂ$
54		2cnd	$⊢ y \in (0 ..^5) \to 2 \in ℂ$
55		1cnd	$⊢ y \in (0 ..^5) \to 1 \in ℂ$
56	53 54 53 55	subsubadd23	$⊢ y \in (0 ..^5) \to y - 2 - (y + 1) = y - y - (2 + 1)$
57	53	subidd	$⊢ y \in (0 ..^5) \to y - y = 0$
58		2p1e3	$⊢ 2 + 1 = 3$
59	58	a1i	$⊢ y \in (0 ..^5) \to 2 + 1 = 3$
60	57 59	oveq12d	$⊢ y \in (0 ..^5) \to y - y - (2 + 1) = 0 - 3$
61		df-neg	$⊢ - 3 = 0 - 3$
62	60 61	eqtr4di	$⊢ y \in (0 ..^5) \to y - y - (2 + 1) = - 3$
63	56 62	eqtrd	$⊢ y \in (0 ..^5) \to y - 2 - (y + 1) = - 3$
64	63	oveq1d	$⊢ y \in (0 ..^5) \to (y - 2 - (y + 1)) \mod 5 = -3 \mod 5$
65	64	eqeq1d	$⊢ y \in (0 ..^5) \to ((y - 2 - (y + 1)) \mod 5 = 0 \leftrightarrow -3 \mod 5 = 0)$
66	43 52 65	3bitr2d	$⊢ y \in (0 ..^5) \to ((y + 1) \mod 5 = (y - 2) \mod 5 \leftrightarrow -3 \mod 5 = 0)$
67		3re	$⊢ 3 \in ℝ$
68		5rp	$⊢ 5 \in ℝ^{+}$
69		negmod0	$⊢ (3 \in ℝ \land 5 \in ℝ^{+}) \to (3 \mod 5 = 0 \leftrightarrow -3 \mod 5 = 0)$
70	67 68 69	mp2an	$⊢ 3 \mod 5 = 0 \leftrightarrow -3 \mod 5 = 0$
71		0re	$⊢ 0 \in ℝ$
72		3pos	$⊢ 0 < 3$
73	71 67 72	ltleii	$⊢ 0 \leq 3$
74		3lt5	$⊢ 3 < 5$
75		modid	$⊢ ((3 \in ℝ \land 5 \in ℝ^{+}) \land (0 \leq 3 \land 3 < 5)) \to 3 \mod 5 = 3$
76	67 68 73 74 75	mp4an	$⊢ 3 \mod 5 = 3$
77	76	eqeq1i	$⊢ 3 \mod 5 = 0 \leftrightarrow 3 = 0$
78	70 77	bitr3i	$⊢ -3 \mod 5 = 0 \leftrightarrow 3 = 0$
79		3ne0	$⊢ 3 \neq 0$
80		eqneqall	$⊢ 3 = 0 \to (3 \neq 0 \to \neg \{⟨0, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E)$
81	79 80	mpi	$⊢ 3 = 0 \to \neg \{⟨0, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E$
82	78 81	sylbi	$⊢ -3 \mod 5 = 0 \to \neg \{⟨0, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E$
83	66 82	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)$
84	83	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)$
85	41 84	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)$
86	85	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))$
87	39 86	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))$
88	8 16	opth	$⊢ ⟨0, b⟩ = ⟨1, 2^{nd} (⟨0, y⟩)⟩ \leftrightarrow (0 = 1 \land b = 2^{nd} (⟨0, y⟩))$
89		0ne1	$⊢ 0 \neq 1$
90		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)))$
91	89 90	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))$
92	91	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))$
93	88 92	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))$
94	33	oveq1i	$⊢ 2^{nd} (⟨0, y⟩) - 1 = y - 1$
95	94	oveq1i	$⊢ (2^{nd} (⟨0, y⟩) - 1) \mod 5 = (y - 1) \mod 5$
96	95	opeq2i	$⊢ ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩ = ⟨0, (y - 1) \mod 5⟩$
97	96	eqeq2i	$⊢ ⟨0, b⟩ = ⟨0, (2^{nd} (⟨0, y⟩) - 1) \mod 5⟩ \leftrightarrow ⟨0, b⟩ = ⟨0, (y - 1) \mod 5⟩$
98	8 16	opth	$⊢ ⟨0, b⟩ = ⟨0, (y - 1) \mod 5⟩ \leftrightarrow (0 = 0 \land b = (y - 1) \mod 5)$
99		eqeq1	$⊢ b = (y - 1) \mod 5 \to (b = (y - 2) \mod 5 \leftrightarrow (y - 1) \mod 5 = (y - 2) \mod 5)$
100	99	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)$
101		1zzd	$⊢ y \in (0 ..^5) \to 1 \in ℤ$
102	44 101	zsubcld	$⊢ y \in (0 ..^5) \to y - 1 \in ℤ$
103		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)$
104	103	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)$
105	102 47 50 104	syl3anc	$⊢ y \in (0 ..^5) \to ((y - 1) \mod 5 = (y - 2) \mod 5 \leftrightarrow (y - 1 - (y - 2)) \mod 5 = 0)$
106	53 55 54	nnncan1d	$⊢ y \in (0 ..^5) \to y - 1 - (y - 2) = 2 - 1$
107		2m1e1	$⊢ 2 - 1 = 1$
108	106 107	eqtrdi	$⊢ y \in (0 ..^5) \to y - 1 - (y - 2) = 1$
109	108	oveq1d	$⊢ y \in (0 ..^5) \to (y - 1 - (y - 2)) \mod 5 = 1 \mod 5$
110	109	eqeq1d	$⊢ y \in (0 ..^5) \to ((y - 1 - (y - 2)) \mod 5 = 0 \leftrightarrow 1 \mod 5 = 0)$
111		1re	$⊢ 1 \in ℝ$
112		0le1	$⊢ 0 \leq 1$
113		1lt5	$⊢ 1 < 5$
114		modid	$⊢ ((1 \in ℝ \land 5 \in ℝ^{+}) \land (0 \leq 1 \land 1 < 5)) \to 1 \mod 5 = 1$
115	111 68 112 113 114	mp4an	$⊢ 1 \mod 5 = 1$
116	115	eqeq1i	$⊢ 1 \mod 5 = 0 \leftrightarrow 1 = 0$
117		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to \neg \{⟨0, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E)$
118	23 117	mpi	$⊢ 1 = 0 \to \neg \{⟨0, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E$
119	116 118	sylbi	$⊢ 1 \mod 5 = 0 \to \neg \{⟨0, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E$
120	110 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	105 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	100 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	98 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	97 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	87 93 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 pgnbgreunbgrlem2lem2

Proof