gpgvtxedg1

Description: The edges starting at an inside vertex X in a generalized Petersen graph G . (Contributed by AV, 2-Sep-2025)

	Ref	Expression
Hypotheses	gpgedgvtx0.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	gpgedgvtx0.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
	gpgedgvtx0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	gpgedgvtx0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	gpgvtxedg1	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		gpgedgvtx0.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2		gpgedgvtx0.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
3		gpgedgvtx0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4		gpgedgvtx0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
5		gpgusgra	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 𝑁 gPetersenGr 𝐾 ) ∈ USGraph )
6	1	eleq2i	⊢ ( 𝐾 ∈ 𝐽 ↔ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
7	6	anbi2i	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ↔ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) )
8	2	eleq1i	⊢ ( 𝐺 ∈ USGraph ↔ ( 𝑁 gPetersenGr 𝐾 ) ∈ USGraph )
9	5 7 8	3imtr4i	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝐺 ∈ USGraph )
10	9	3ad2ant1	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → 𝐺 ∈ USGraph )
11		simp3	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { 𝑋 , 𝑌 } ∈ 𝐸 )
12	4 3	usgrpredgv	⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) )
13	10 11 12	syl2anc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) )
14		eqid	⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
15	14 1 2 4	gpgedgel	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 ↔ ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { 𝑋 , 𝑌 } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
16	15	3ad2ant1	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 ↔ ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { 𝑋 , 𝑌 } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
17		simp3	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) )
18	17	adantr	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) )
19		opex	⊢ ⟨ 0 , 𝑦 ⟩ ∈ V
20		opex	⊢ ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ V
21	19 20	pm3.2i	⊢ ( ⟨ 0 , 𝑦 ⟩ ∈ V ∧ ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ V )
22		preq12bg	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ⟨ 0 , 𝑦 ⟩ ∈ V ∧ ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∈ V ) ) → ( { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ↔ ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ) ∨ ( 𝑋 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) ) ) )
23	18 21 22	sylancl	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ↔ ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ) ∨ ( 𝑋 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) ) ) )
24		c0ex	⊢ 0 ∈ V
25		vex	⊢ 𝑦 ∈ V
26	24 25	op1std	⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 1^st ‘ 𝑋 ) = 0 )
27	26	eqeq1d	⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( 1^st ‘ 𝑋 ) = 1 ↔ 0 = 1 ) )
28		eqcom	⊢ ( 0 = 1 ↔ 1 = 0 )
29	27 28	bitrdi	⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( 1^st ‘ 𝑋 ) = 1 ↔ 1 = 0 ) )
30		ax-1ne0	⊢ 1 ≠ 0
31		eqneqall	⊢ ( 1 = 0 → ( 1 ≠ 0 → ( 𝑌 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
32	31	com12	⊢ ( 1 ≠ 0 → ( 1 = 0 → ( 𝑌 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
33	30 32	mp1i	⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 1 = 0 → ( 𝑌 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
34	29 33	sylbid	⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( 1^st ‘ 𝑋 ) = 1 → ( 𝑌 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
35	34	com12	⊢ ( ( 1^st ‘ 𝑋 ) = 1 → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 𝑌 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
36	35	impd	⊢ ( ( 1^st ‘ 𝑋 ) = 1 → ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
37		ovex	⊢ ( ( 𝑦 + 1 ) mod 𝑁 ) ∈ V
38	24 37	op1std	⊢ ( 𝑋 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ → ( 1^st ‘ 𝑋 ) = 0 )
39	38	eqeq1d	⊢ ( 𝑋 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ → ( ( 1^st ‘ 𝑋 ) = 1 ↔ 0 = 1 ) )
40	39 28	bitrdi	⊢ ( 𝑋 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ → ( ( 1^st ‘ 𝑋 ) = 1 ↔ 1 = 0 ) )
41		eqneqall	⊢ ( 1 = 0 → ( 1 ≠ 0 → ( 𝑌 = ⟨ 0 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
42	41	com12	⊢ ( 1 ≠ 0 → ( 1 = 0 → ( 𝑌 = ⟨ 0 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
43	30 42	mp1i	⊢ ( 𝑋 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ → ( 1 = 0 → ( 𝑌 = ⟨ 0 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
44	40 43	sylbid	⊢ ( 𝑋 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ → ( ( 1^st ‘ 𝑋 ) = 1 → ( 𝑌 = ⟨ 0 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
45	44	com12	⊢ ( ( 1^st ‘ 𝑋 ) = 1 → ( 𝑋 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ → ( 𝑌 = ⟨ 0 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
46	45	impd	⊢ ( ( 1^st ‘ 𝑋 ) = 1 → ( ( 𝑋 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
47	36 46	jaod	⊢ ( ( 1^st ‘ 𝑋 ) = 1 → ( ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ) ∨ ( 𝑋 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
48	47	3ad2ant2	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ) ∨ ( 𝑋 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
49	48	adantr	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ) ∨ ( 𝑋 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
50	23 49	sylbid	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
51		opex	⊢ ⟨ 1 , 𝑦 ⟩ ∈ V
52	19 51	pm3.2i	⊢ ( ⟨ 0 , 𝑦 ⟩ ∈ V ∧ ⟨ 1 , 𝑦 ⟩ ∈ V )
53		preq12bg	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ⟨ 0 , 𝑦 ⟩ ∈ V ∧ ⟨ 1 , 𝑦 ⟩ ∈ V ) ) → ( { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ↔ ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) ∨ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) ) ) )
54	18 52 53	sylancl	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ↔ ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) ∨ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) ) ) )
55		eqneqall	⊢ ( 1 = 0 → ( 1 ≠ 0 → ( 𝑌 = ⟨ 1 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
56	55	com12	⊢ ( 1 ≠ 0 → ( 1 = 0 → ( 𝑌 = ⟨ 1 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
57	30 56	mp1i	⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 1 = 0 → ( 𝑌 = ⟨ 1 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
58	29 57	sylbid	⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( 1^st ‘ 𝑋 ) = 1 → ( 𝑌 = ⟨ 1 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
59	58	com12	⊢ ( ( 1^st ‘ 𝑋 ) = 1 → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
60	59	3ad2ant2	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
61	60	adantr	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , 𝑦 ⟩ → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) )
62	61	impd	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
63		simpr	⊢ ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) → 𝑌 = ⟨ 0 , 𝑦 ⟩ )
64		1ex	⊢ 1 ∈ V
65	64 25	op2ndd	⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( 2^nd ‘ 𝑋 ) = 𝑦 )
66	65	eqcomd	⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → 𝑦 = ( 2^nd ‘ 𝑋 ) )
67	66	adantr	⊢ ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) → 𝑦 = ( 2^nd ‘ 𝑋 ) )
68	67	opeq2d	⊢ ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ )
69	63 68	eqtrd	⊢ ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) → 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ )
70	69	adantl	⊢ ( ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) ) → 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ )
71	70	3mix2d	⊢ ( ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) )
72	71	ex	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
73	62 72	jaod	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) ∨ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 0 , 𝑦 ⟩ ) ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
74	54 73	sylbid	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
75		opex	⊢ ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ V
76	51 75	pm3.2i	⊢ ( ⟨ 1 , 𝑦 ⟩ ∈ V ∧ ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ V )
77		preq12bg	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ⟨ 1 , 𝑦 ⟩ ∈ V ∧ ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ V ) ) → ( { 𝑋 , 𝑌 } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ↔ ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ) ∨ ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) ) ) )
78	18 76 77	sylancl	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( { 𝑋 , 𝑌 } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ↔ ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ) ∨ ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) ) ) )
79		simpr	⊢ ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑌 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ )
80	66	oveq1d	⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( 𝑦 + 𝐾 ) = ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) )
81	80	oveq1d	⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( 𝑦 + 𝐾 ) mod 𝑁 ) = ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) )
82	81	adantr	⊢ ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ) → ( ( 𝑦 + 𝐾 ) mod 𝑁 ) = ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) )
83	82	opeq2d	⊢ ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ) → ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ )
84	79 83	eqtrd	⊢ ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ )
85	84	3mix1d	⊢ ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) )
86	85	a1i	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
87		elfzoelz	⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 𝑦 ∈ ℤ )
88	87	zred	⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 𝑦 ∈ ℝ )
89	88	adantl	⊢ ( ( 𝐾 ∈ 𝐽 ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑦 ∈ ℝ )
90		elfzoelz	⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℤ )
91	90	zred	⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℝ )
92	6 91	sylbi	⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℝ )
93	92	adantr	⊢ ( ( 𝐾 ∈ 𝐽 ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝐾 ∈ ℝ )
94	89 93	readdcld	⊢ ( ( 𝐾 ∈ 𝐽 ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 + 𝐾 ) ∈ ℝ )
95		elfzo0	⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝑦 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) )
96		nnrp	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ⁺ )
97	96	3ad2ant2	⊢ ( ( 𝑦 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → 𝑁 ∈ ℝ⁺ )
98	95 97	sylbi	⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 𝑁 ∈ ℝ⁺ )
99	98	adantl	⊢ ( ( 𝐾 ∈ 𝐽 ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℝ⁺ )
100		modsubmod	⊢ ( ( ( 𝑦 + 𝐾 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ⁺ ) → ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) = ( ( ( 𝑦 + 𝐾 ) − 𝐾 ) mod 𝑁 ) )
101	94 93 99 100	syl3anc	⊢ ( ( 𝐾 ∈ 𝐽 ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) = ( ( ( 𝑦 + 𝐾 ) − 𝐾 ) mod 𝑁 ) )
102	87	zcnd	⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 𝑦 ∈ ℂ )
103	102	adantl	⊢ ( ( 𝐾 ∈ 𝐽 ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑦 ∈ ℂ )
104	93	recnd	⊢ ( ( 𝐾 ∈ 𝐽 ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝐾 ∈ ℂ )
105	103 104	pncand	⊢ ( ( 𝐾 ∈ 𝐽 ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑦 + 𝐾 ) − 𝐾 ) = 𝑦 )
106	105	oveq1d	⊢ ( ( 𝐾 ∈ 𝐽 ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑦 + 𝐾 ) − 𝐾 ) mod 𝑁 ) = ( 𝑦 mod 𝑁 ) )
107		zmodidfzoimp	⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( 𝑦 mod 𝑁 ) = 𝑦 )
108	107	adantl	⊢ ( ( 𝐾 ∈ 𝐽 ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 mod 𝑁 ) = 𝑦 )
109	101 106 108	3eqtrrd	⊢ ( ( 𝐾 ∈ 𝐽 ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑦 = ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) )
110	109	ex	⊢ ( 𝐾 ∈ 𝐽 → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 𝑦 = ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) ) )
111	110	adantl	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 𝑦 = ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) ) )
112	111	3ad2ant1	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 𝑦 = ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) ) )
113	112	imp	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑦 = ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) )
114	113	adantr	⊢ ( ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) ) → 𝑦 = ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) )
115	114	opeq2d	⊢ ( ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) ) → ⟨ 1 , 𝑦 ⟩ = ⟨ 1 , ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) ⟩ )
116		simpr	⊢ ( ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) → 𝑌 = ⟨ 1 , 𝑦 ⟩ )
117		ovex	⊢ ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ∈ V
118	64 117	op2ndd	⊢ ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ → ( 2^nd ‘ 𝑋 ) = ( ( 𝑦 + 𝐾 ) mod 𝑁 ) )
119	118	oveq1d	⊢ ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ → ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) = ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) )
120	119	oveq1d	⊢ ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ → ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) = ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) )
121	120	opeq2d	⊢ ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ → ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) ⟩ )
122	121	adantr	⊢ ( ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) → ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) ⟩ )
123	116 122	eqeq12d	⊢ ( ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ↔ ⟨ 1 , 𝑦 ⟩ = ⟨ 1 , ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) ⟩ ) )
124	123	adantl	⊢ ( ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ↔ ⟨ 1 , 𝑦 ⟩ = ⟨ 1 , ( ( ( ( 𝑦 + 𝐾 ) mod 𝑁 ) − 𝐾 ) mod 𝑁 ) ⟩ ) )
125	115 124	mpbird	⊢ ( ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) ) → 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ )
126	125	3mix3d	⊢ ( ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) )
127	126	ex	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
128	86 127	jaod	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑋 = ⟨ 1 , 𝑦 ⟩ ∧ 𝑌 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ) ∨ ( 𝑋 = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∧ 𝑌 = ⟨ 1 , 𝑦 ⟩ ) ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
129	78 128	sylbid	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( { 𝑋 , 𝑌 } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
130	50 74 129	3jaod	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { 𝑋 , 𝑌 } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
131	130	rexlimdva	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) ( { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { 𝑋 , 𝑌 } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { 𝑋 , 𝑌 } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
132	16 131	sylbid	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
133	132	3exp	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ( 1^st ‘ 𝑋 ) = 1 → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) ) )
134	133	com34	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ( 1^st ‘ 𝑋 ) = 1 → ( { 𝑋 , 𝑌 } ∈ 𝐸 → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) ) ) )
135	134	3imp	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
136	13 135	mpd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1^st ‘ 𝑋 ) = 1 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ 𝑌 = ⟨ 0 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝑌 = ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ) )

Metamath Proof Explorer

Theorem gpgvtxedg1

Proof