pgnbgreunbgrlem2lem3

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

	Ref	Expression
Hypotheses	pgnbgreunbgr.g	⊢ 𝐺 = ( 5 gPetersenGr 2 )
	pgnbgreunbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	pgnbgreunbgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	pgnbgreunbgr.n	⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑋 )
Assertion	pgnbgreunbgrlem2lem3	⊢ ( ( ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		pgnbgreunbgr.g	⊢ 𝐺 = ( 5 gPetersenGr 2 )
2		pgnbgreunbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3		pgnbgreunbgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
4		pgnbgreunbgr.n	⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑋 )
5		prcom	⊢ { ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } = { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ }
6	5	eleq1i	⊢ ( { ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
7	6	a1i	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( { ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
8		5eluz3	⊢ 5 ∈ ( ℤ_≥ ‘ 3 )
9		pglem	⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
10	8 9	pm3.2i	⊢ ( 5 ∈ ( ℤ_≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
11		c0ex	⊢ 0 ∈ V
12		vex	⊢ 𝑏 ∈ V
13	11 12	op1st	⊢ ( 1^st ‘ ⟨ 0 , 𝑏 ⟩ ) = 0
14		eqid	⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
15	14 1 2 3	gpgvtxedg0	⊢ ( ( ( 5 ∈ ( ℤ_≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ ( 1^st ‘ ⟨ 0 , 𝑏 ⟩ ) = 0 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) )
16	10 13 15	mp3an12	⊢ ( { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 → ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) )
17	7 16	biimtrdi	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( { ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) )
18	14 1 2 3	gpgvtxedg0	⊢ ( ( ( 5 ∈ ( ℤ_≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ ( 1^st ‘ ⟨ 0 , 𝑏 ⟩ ) = 0 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ( ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) )
19	10 13 18	mp3an12	⊢ ( { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 → ( ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) )
20		1ex	⊢ 1 ∈ V
21		ovex	⊢ ( ( 𝑦 + 2 ) mod 5 ) ∈ V
22	20 21	opth	⊢ ( ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ↔ ( 1 = 0 ∧ ( ( 𝑦 + 2 ) mod 5 ) = ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ) )
23		ax-1ne0	⊢ 1 ≠ 0
24		eqneqall	⊢ ( 1 = 0 → ( 1 ≠ 0 → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
25	23 24	mpi	⊢ ( 1 = 0 → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
26	25	adantr	⊢ ( ( 1 = 0 ∧ ( ( 𝑦 + 2 ) mod 5 ) = ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ) → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
27	22 26	sylbi	⊢ ( ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
28	20 21	opth	⊢ ( ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ↔ ( 1 = 1 ∧ ( ( 𝑦 + 2 ) mod 5 ) = ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ) )
29	11 12	op2nd	⊢ ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) = 𝑏
30	29	eqeq2i	⊢ ( ( ( 𝑦 + 2 ) mod 5 ) = ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ↔ ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 )
31		ovex	⊢ ( ( 𝑦 − 2 ) mod 5 ) ∈ V
32	20 31	opth	⊢ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ↔ ( 1 = 0 ∧ ( ( 𝑦 − 2 ) mod 5 ) = ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ) )
33		eqneqall	⊢ ( 1 = 0 → ( 1 ≠ 0 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) ) )
34	23 33	mpi	⊢ ( 1 = 0 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
35	34	adantr	⊢ ( ( 1 = 0 ∧ ( ( 𝑦 − 2 ) mod 5 ) = ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
36	32 35	sylbi	⊢ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
37	20 31	opth	⊢ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ↔ ( 1 = 1 ∧ ( ( 𝑦 − 2 ) mod 5 ) = ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ) )
38	29	eqeq2i	⊢ ( ( ( 𝑦 − 2 ) mod 5 ) = ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ↔ ( ( 𝑦 − 2 ) mod 5 ) = 𝑏 )
39		eqeq2	⊢ ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 ↔ ( ( 𝑦 + 2 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ) )
40	39	eqcoms	⊢ ( ( ( 𝑦 − 2 ) mod 5 ) = 𝑏 → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 ↔ ( ( 𝑦 + 2 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ) )
41	40	adantl	⊢ ( ( 𝑦 ∈ ( 0 ..^ 5 ) ∧ ( ( 𝑦 − 2 ) mod 5 ) = 𝑏 ) → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 ↔ ( ( 𝑦 + 2 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ) )
42		elfzoelz	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 𝑦 ∈ ℤ )
43		2z	⊢ 2 ∈ ℤ
44	43	a1i	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 2 ∈ ℤ )
45	42 44	zaddcld	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑦 + 2 ) ∈ ℤ )
46	42 44	zsubcld	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑦 − 2 ) ∈ ℤ )
47		5nn	⊢ 5 ∈ ℕ
48	47	a1i	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 5 ∈ ℕ )
49		difmod0	⊢ ( ( ( 𝑦 + 2 ) ∈ ℤ ∧ ( 𝑦 − 2 ) ∈ ℤ ∧ 5 ∈ ℕ ) → ( ( ( ( 𝑦 + 2 ) − ( 𝑦 − 2 ) ) mod 5 ) = 0 ↔ ( ( 𝑦 + 2 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ) )
50	49	bicomd	⊢ ( ( ( 𝑦 + 2 ) ∈ ℤ ∧ ( 𝑦 − 2 ) ∈ ℤ ∧ 5 ∈ ℕ ) → ( ( ( 𝑦 + 2 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ↔ ( ( ( 𝑦 + 2 ) − ( 𝑦 − 2 ) ) mod 5 ) = 0 ) )
51	45 46 48 50	syl3anc	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 + 2 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ↔ ( ( ( 𝑦 + 2 ) − ( 𝑦 − 2 ) ) mod 5 ) = 0 ) )
52	42	zcnd	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 𝑦 ∈ ℂ )
53		2cnd	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 2 ∈ ℂ )
54	52 53 53	pnncand	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 + 2 ) − ( 𝑦 − 2 ) ) = ( 2 + 2 ) )
55		2p2e4	⊢ ( 2 + 2 ) = 4
56	54 55	eqtrdi	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 + 2 ) − ( 𝑦 − 2 ) ) = 4 )
57	56	oveq1d	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 + 2 ) − ( 𝑦 − 2 ) ) mod 5 ) = ( 4 mod 5 ) )
58	57	eqeq1d	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( ( 𝑦 + 2 ) − ( 𝑦 − 2 ) ) mod 5 ) = 0 ↔ ( 4 mod 5 ) = 0 ) )
59		4re	⊢ 4 ∈ ℝ
60		5rp	⊢ 5 ∈ ℝ⁺
61		0re	⊢ 0 ∈ ℝ
62		4pos	⊢ 0 < 4
63	61 59 62	ltleii	⊢ 0 ≤ 4
64		4lt5	⊢ 4 < 5
65		modid	⊢ ( ( ( 4 ∈ ℝ ∧ 5 ∈ ℝ⁺ ) ∧ ( 0 ≤ 4 ∧ 4 < 5 ) ) → ( 4 mod 5 ) = 4 )
66	59 60 63 64 65	mp4an	⊢ ( 4 mod 5 ) = 4
67	66	eqeq1i	⊢ ( ( 4 mod 5 ) = 0 ↔ 4 = 0 )
68		4ne0	⊢ 4 ≠ 0
69	68	a1i	⊢ ( { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 → 4 ≠ 0 )
70	69	necon2bi	⊢ ( 4 = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
71	67 70	sylbi	⊢ ( ( 4 mod 5 ) = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
72	58 71	biimtrdi	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( ( 𝑦 + 2 ) − ( 𝑦 − 2 ) ) mod 5 ) = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
73	51 72	sylbid	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 + 2 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
74	73	adantr	⊢ ( ( 𝑦 ∈ ( 0 ..^ 5 ) ∧ ( ( 𝑦 − 2 ) mod 5 ) = 𝑏 ) → ( ( ( 𝑦 + 2 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
75	41 74	sylbid	⊢ ( ( 𝑦 ∈ ( 0 ..^ 5 ) ∧ ( ( 𝑦 − 2 ) mod 5 ) = 𝑏 ) → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
76	75	ex	⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 − 2 ) mod 5 ) = 𝑏 → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
77	76	adantl	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ( 𝑦 − 2 ) mod 5 ) = 𝑏 → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
78	77	com12	⊢ ( ( ( 𝑦 − 2 ) mod 5 ) = 𝑏 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
79	38 78	sylbi	⊢ ( ( ( 𝑦 − 2 ) mod 5 ) = ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
80	37 79	simplbiim	⊢ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
81	20 31	opth	⊢ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ↔ ( 1 = 0 ∧ ( ( 𝑦 − 2 ) mod 5 ) = ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ) )
82	34	adantr	⊢ ( ( 1 = 0 ∧ ( ( 𝑦 − 2 ) mod 5 ) = ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
83	81 82	sylbi	⊢ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
84	36 80 83	3jaoi	⊢ ( ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
85	84	com13	⊢ ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
86	85	impd	⊢ ( ( ( 𝑦 + 2 ) mod 5 ) = 𝑏 → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
87	30 86	sylbi	⊢ ( ( ( 𝑦 + 2 ) mod 5 ) = ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
88	28 87	simplbiim	⊢ ( ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
89	20 21	opth	⊢ ( ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ↔ ( 1 = 0 ∧ ( ( 𝑦 + 2 ) mod 5 ) = ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ) )
90	25	adantr	⊢ ( ( 1 = 0 ∧ ( ( 𝑦 + 2 ) mod 5 ) = ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ) → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
91	89 90	sylbi	⊢ ( ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
92	27 88 91	3jaoi	⊢ ( ( ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
93	19 92	syl	⊢ ( { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
94		ax-1	⊢ ( ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
95	93 94	pm2.61i	⊢ ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
96	95	ex	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2^nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
97	17 96	syld	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( { ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
98	97	adantl	⊢ ( ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( { ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
99		preq1	⊢ ( 𝐾 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ → { 𝐾 , ⟨ 0 , 𝑏 ⟩ } = { ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } )
100	99	eleq1d	⊢ ( 𝐾 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ → ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) )
101	100	adantl	⊢ ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ) → ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) )
102		preq2	⊢ ( 𝐿 = ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ → { ⟨ 0 , 𝑏 ⟩ , 𝐿 } = { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } )
103	102	eleq1d	⊢ ( 𝐿 = ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ → ( { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
104	103	notbid	⊢ ( 𝐿 = ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ → ( ¬ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
105	104	adantr	⊢ ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ) → ( ¬ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
106	101 105	imbi12d	⊢ ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ↔ ( { ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
107	106	adantr	⊢ ( ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ↔ ( { ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
108	98 107	mpbird	⊢ ( ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) )
109	108	imp	⊢ ( ( ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 )

Metamath Proof Explorer

Theorem pgnbgreunbgrlem2lem3

Proof