gpgvtx1

Description: The vertices of the second kind in a generalized Petersen graph G . (Contributed by AV, 28-Aug-2025)

	Ref	Expression
Hypotheses	gpgvtx0.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	gpgvtx0.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
	gpgvtx0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	gpgvtx1	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		gpgvtx0.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2		gpgvtx0.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
3		gpgvtx0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4		eqid	⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
5	4 1 2 3	gpgvtxel	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) )
6	2	fveq2i	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) )
7	3 6	eqtri	⊢ 𝑉 = ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) )
8		eluzge3nn	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 𝑁 ∈ ℕ )
9	1 4	gpgvtx	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
10	8 9	sylan	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
11	10	adantr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
12	7 11	eqtrid	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
13		1ex	⊢ 1 ∈ V
14	13	prid2	⊢ 1 ∈ { 0 , 1 }
15	14	a1i	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → 1 ∈ { 0 , 1 } )
16		elfzoelz	⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 𝑦 ∈ ℤ )
17	16	adantl	⊢ ( ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑦 ∈ ℤ )
18	17	adantl	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → 𝑦 ∈ ℤ )
19		elfzoelz	⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℤ )
20	19 1	eleq2s	⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℤ )
21	20	adantl	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝐾 ∈ ℤ )
22	21	adantr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → 𝐾 ∈ ℤ )
23	18 22	zaddcld	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝑦 + 𝐾 ) ∈ ℤ )
24	8	adantr	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝑁 ∈ ℕ )
25	24	adantr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
26		zmodfzo	⊢ ( ( ( 𝑦 + 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
27	23 25 26	syl2anc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
28	15 27	opelxpd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
29		simprr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → 𝑦 ∈ ( 0 ..^ 𝑁 ) )
30	15 29	opelxpd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ⟨ 1 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
31	18 22	zsubcld	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝑦 − 𝐾 ) ∈ ℤ )
32		zmodfzo	⊢ ( ( ( 𝑦 − 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
33	31 25 32	syl2anc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
34	15 33	opelxpd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
35	28 30 34	3jca	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
36	35	adantr	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
37		eleq2	⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
38		eleq2	⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ↔ ⟨ 1 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
39		eleq2	⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
40	37 38 39	3anbi123d	⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ↔ ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) ) )
41	40	adantl	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) → ( ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ↔ ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) ) )
42	36 41	mpbird	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
43	12 42	mpdan	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
44		vex	⊢ 𝑥 ∈ V
45		vex	⊢ 𝑦 ∈ V
46	44 45	op2ndd	⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2^nd ‘ 𝑋 ) = 𝑦 )
47		oveq1	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) = ( 𝑦 + 𝐾 ) )
48	47	oveq1d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) = ( ( 𝑦 + 𝐾 ) mod 𝑁 ) )
49	48	opeq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ )
50	49	eleq1d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
51		opeq2	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ = ⟨ 1 , 𝑦 ⟩ )
52	51	eleq1d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ↔ ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ) )
53		oveq1	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) = ( 𝑦 − 𝐾 ) )
54	53	oveq1d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) = ( ( 𝑦 − 𝐾 ) mod 𝑁 ) )
55	54	opeq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ )
56	55	eleq1d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
57	50 52 56	3anbi123d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ↔ ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
58	46 57	syl	⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ↔ ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
59	43 58	syl5ibrcom	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
60	59	rexlimdvva	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
61	5 60	sylbid	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
62	61	imp	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )

Metamath Proof Explorer

Theorem gpgvtx1

Proof