gpgvtx1

Description: The inside vertices 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		eluz3nn	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 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		1elpr01	⊢ 1 ∈ { 0 , 1 }
14	13	a1i	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → 1 ∈ { 0 , 1 } )
15		elfzoelz	⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 𝑦 ∈ ℤ )
16	15	adantl	⊢ ( ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑦 ∈ ℤ )
17	16	adantl	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → 𝑦 ∈ ℤ )
18		elfzoelz	⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℤ )
19	18 1	eleq2s	⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℤ )
20	19	adantl	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝐾 ∈ ℤ )
21	20	adantr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → 𝐾 ∈ ℤ )
22	17 21	zaddcld	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝑦 + 𝐾 ) ∈ ℤ )
23	8	adantr	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝑁 ∈ ℕ )
24	23	adantr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
25		zmodfzo	⊢ ( ( ( 𝑦 + 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
26	22 24 25	syl2anc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
27	14 26	opelxpd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
28		simprr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → 𝑦 ∈ ( 0 ..^ 𝑁 ) )
29	14 28	opelxpd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ⟨ 1 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
30	17 21	zsubcld	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝑦 − 𝐾 ) ∈ ℤ )
31		zmodfzo	⊢ ( ( ( 𝑦 − 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
32	30 24 31	syl2anc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
33	14 32	opelxpd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
34	27 29 33	3jca	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
35	34	adantr	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
36		eleq2	⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
37		eleq2	⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ↔ ⟨ 1 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
38		eleq2	⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) )
39	36 37 38	3anbi123d	⊢ ( 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) → ( ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ↔ ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , 𝑦 ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) ) )
40	39	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 ..^ 𝑁 ) ) ) ) )
41	35 40	mpbird	⊢ ( ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑉 = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
42	12 41	mpdan	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
43		vex	⊢ 𝑥 ∈ V
44		vex	⊢ 𝑦 ∈ V
45	43 44	op2ndd	⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2^nd ‘ 𝑋 ) = 𝑦 )
46		oveq1	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) = ( 𝑦 + 𝐾 ) )
47	46	oveq1d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) = ( ( 𝑦 + 𝐾 ) mod 𝑁 ) )
48	47	opeq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ )
49	48	eleq1d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
50		opeq2	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ = ⟨ 1 , 𝑦 ⟩ )
51	50	eleq1d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ↔ ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ) )
52		oveq1	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) = ( 𝑦 − 𝐾 ) )
53	52	oveq1d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) = ( ( 𝑦 − 𝐾 ) mod 𝑁 ) )
54	53	opeq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ )
55	54	eleq1d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ↔ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )
56	49 51 55	3anbi123d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ↔ ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
57	45 56	syl	⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ↔ ( ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , 𝑦 ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
58	42 57	syl5ibrcom	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
59	58	rexlimdvva	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
60	5 59	sylbid	⊢ ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) ) )
61	60	imp	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝑉 ∧ ⟨ 1 , ( ( ( 2^nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ ∈ 𝑉 ) )

Metamath Proof Explorer

Theorem gpgvtx1

Proof