Metamath Proof Explorer

Theorem gpgedg2iv

Description: The edges of the generalized Petersen graph GPG(N,K) between two inside vertices. (Contributed by AV, 20-Nov-2025)

Ref Expression
Hypotheses gpgedgiov.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
gpgedgiov.i ⊢ 𝐼 = ( 0 ..^ 𝑁 )
gpgedgiov.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
gpgedgiov.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion gpgedg2iv ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑋 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 gpgedgiov.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2 gpgedgiov.i ⊢ 𝐼 = ( 0 ..^ 𝑁 )
3 gpgedgiov.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
4 gpgedgiov.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
5 prcom ⊢ { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑋 ⟩ } = { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ }
6 5 eleq1i ⊢ ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑋 ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
7 uzuzle35 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
8 simpl ⊢ ( ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) → 𝐾 ∈ 𝐽 )
9 7 8 anim12i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) )
10 9 3adant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) )
11 10 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) )
12 1ex ⊢ 1 ∈ V
13 12 a1i ⊢ ( 𝑌 ∈ 𝐼 → 1 ∈ V )
14 13 anim1i ⊢ ( ( 𝑌 ∈ 𝐼 ∧ 𝑋 ∈ 𝐼 ) → ( 1 ∈ V ∧ 𝑋 ∈ 𝐼 ) )
15 14 ancoms ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 1 ∈ V ∧ 𝑋 ∈ 𝐼 ) )
16 op1stg ⊢ ( ( 1 ∈ V ∧ 𝑋 ∈ 𝐼 ) → ( 1st ‘ ⟨ 1 , 𝑋 ⟩ ) = 1 )
17 15 16 syl ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 1st ‘ ⟨ 1 , 𝑋 ⟩ ) = 1 )
18 17 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( 1st ‘ ⟨ 1 , 𝑋 ⟩ ) = 1 )
19 18 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 1st ‘ ⟨ 1 , 𝑋 ⟩ ) = 1 )
20 simpr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
21 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
22 1 3 21 4 gpgvtxedg1 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1st ‘ ⟨ 1 , 𝑋 ⟩ ) = 1 ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) )
23 11 19 20 22 syl3anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) )
24 23 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
25 6 24 biimtrid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑋 ⟩ } ∈ 𝐸 → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
26 10 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) )
27 18 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 1st ‘ ⟨ 1 , 𝑋 ⟩ ) = 1 )
28 simpr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
29 1 3 21 4 gpgvtxedg1 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1st ‘ ⟨ 1 , 𝑋 ⟩ ) = 1 ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) )
30 26 27 28 29 syl3anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) )
31 30 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
32 ovex ⊢ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ∈ V
33 12 32 opth ⊢ ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ↔ ( 1 = 1 ∧ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ) )
34 7 3ad2ant1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
35 simp2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) )
36 35 ancomd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( 𝑌 ∈ 𝐼 ∧ 𝑋 ∈ 𝐼 ) )
37 elfzoelz ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℤ )
38 37 1 eleq2s ⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℤ )
39 38 adantr ⊢ ( ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) → 𝐾 ∈ ℤ )
40 39 3ad2ant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → 𝐾 ∈ ℤ )
41 2 modaddid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑌 ∈ 𝐼 ∧ 𝑋 ∈ 𝐼 ) ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ↔ 𝑌 = 𝑋 ) )
42 34 36 40 41 syl3anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ↔ 𝑌 = 𝑋 ) )
43 42 biimpa ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ) → 𝑌 = 𝑋 )
44 43 eqcomd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ) → 𝑋 = 𝑌 )
45 44 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) → 𝑋 = 𝑌 ) )
46 45 adantld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( 1 = 1 ∧ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ) → 𝑋 = 𝑌 ) )
47 33 46 biimtrid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
48 47 a1dd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
49 12 32 opth ⊢ ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ↔ ( 1 = 0 ∧ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = 𝑋 ) )
50 49 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ↔ ( 1 = 0 ∧ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = 𝑋 ) ) )
51 ax-1ne0 ⊢ 1 ≠ 0
52 eqneqall ⊢ ( 1 = 0 → ( 1 ≠ 0 → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = 𝑋 → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) ) )
53 51 52 mpi ⊢ ( 1 = 0 → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = 𝑋 → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
54 53 imp ⊢ ( ( 1 = 0 ∧ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = 𝑋 ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
55 50 54 biimtrdi ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
56 55 imp ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
57 ovex ⊢ ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ∈ V
58 12 57 opth ⊢ ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ↔ ( 1 = 0 ∧ ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = 𝑋 ) )
59 58 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ↔ ( 1 = 0 ∧ ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = 𝑋 ) ) )
60 eqneqall ⊢ ( 1 = 0 → ( 1 ≠ 0 → ( ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = 𝑋 → 𝑋 = 𝑌 ) ) )
61 51 60 mpi ⊢ ( 1 = 0 → ( ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = 𝑋 → 𝑋 = 𝑌 ) )
62 61 imp ⊢ ( ( 1 = 0 ∧ ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = 𝑋 ) → 𝑋 = 𝑌 )
63 59 62 biimtrdi ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ → 𝑋 = 𝑌 ) )
64 51 orci ⊢ ( 1 ≠ 0 ∨ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ≠ 𝑋 )
65 12 32 opthne ⊢ ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , 𝑋 ⟩ ↔ ( 1 ≠ 0 ∨ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ≠ 𝑋 ) )
66 64 65 mpbir ⊢ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , 𝑋 ⟩
67 66 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , 𝑋 ⟩ )
68 eqneqall ⊢ ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , 𝑋 ⟩ → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
69 67 68 mpan9 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
70 56 63 69 3jaod ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ) → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) )
71 70 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
72 12 32 opth ⊢ ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ↔ ( 1 = 1 ∧ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ) )
73 12 57 opth ⊢ ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ↔ ( 1 = 1 ∧ ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ) )
74 eluz3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
75 7 74 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 𝑁 ∈ ℕ )
76 75 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑁 ∈ ℕ )
77 76 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝐾 ∈ 𝐽 ) → 𝑁 ∈ ℕ )
78 elfzoelz ⊢ ( 𝑋 ∈ ( 0 ..^ 𝑁 ) → 𝑋 ∈ ℤ )
79 78 2 eleq2s ⊢ ( 𝑋 ∈ 𝐼 → 𝑋 ∈ ℤ )
80 79 ad2antrl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑋 ∈ ℤ )
81 80 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝐾 ∈ 𝐽 ) → 𝑋 ∈ ℤ )
82 elfzoelz ⊢ ( 𝑌 ∈ ( 0 ..^ 𝑁 ) → 𝑌 ∈ ℤ )
83 82 2 eleq2s ⊢ ( 𝑌 ∈ 𝐼 → 𝑌 ∈ ℤ )
84 83 ad2antll ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑌 ∈ ℤ )
85 84 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝐾 ∈ 𝐽 ) → 𝑌 ∈ ℤ )
86 38 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝐾 ∈ 𝐽 ) → 𝐾 ∈ ℤ )
87 modmkpkne ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ↔ ( ( 4 · 𝐾 ) mod 𝑁 ) = 0 ) ) )
88 77 81 85 86 87 syl13anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝐾 ∈ 𝐽 ) → ( ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ↔ ( ( 4 · 𝐾 ) mod 𝑁 ) = 0 ) ) )
89 88 imp ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ) → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ↔ ( ( 4 · 𝐾 ) mod 𝑁 ) = 0 ) )
90 eqneqall ⊢ ( ( ( 4 · 𝐾 ) mod 𝑁 ) = 0 → ( ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 → 𝑋 = 𝑌 ) )
91 89 90 biimtrdi ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ) → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) → ( ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 → 𝑋 = 𝑌 ) ) )
92 91 expimpd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝐾 ∈ 𝐽 ) → ( ( ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ∧ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ) → ( ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 → 𝑋 = 𝑌 ) ) )
93 92 com23 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝐾 ∈ 𝐽 ) → ( ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 → ( ( ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ∧ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ) → 𝑋 = 𝑌 ) ) )
94 93 expimpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) → ( ( ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ∧ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ) → 𝑋 = 𝑌 ) ) )
95 94 3impia ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ∧ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ) → 𝑋 = 𝑌 ) )
96 95 expd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) → 𝑋 = 𝑌 ) ) )
97 96 adantld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( 1 = 1 ∧ ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ) → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) → 𝑋 = 𝑌 ) ) )
98 73 97 biimtrid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) → 𝑋 = 𝑌 ) ) )
99 98 com23 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
100 99 adantld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( 1 = 1 ∧ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
101 72 100 biimtrid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
102 101 imp ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
103 51 orci ⊢ ( 1 ≠ 0 ∨ ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ≠ 𝑋 )
104 12 57 opthne ⊢ ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , 𝑋 ⟩ ↔ ( 1 ≠ 0 ∨ ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ≠ 𝑋 ) )
105 103 104 mpbir ⊢ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , 𝑋 ⟩
106 eqneqall ⊢ ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , 𝑋 ⟩ → 𝑋 = 𝑌 ) )
107 105 106 mpi ⊢ ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ → 𝑋 = 𝑌 )
108 107 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ → 𝑋 = 𝑌 ) )
109 eqeq2 ⊢ ( ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ↔ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ ) )
110 109 eqcoms ⊢ ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ↔ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ ) )
111 110 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ↔ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ ) )
112 12 57 opth ⊢ ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ ↔ ( 1 = 1 ∧ ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ) )
113 simpr ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → 𝑌 ∈ 𝐼 )
114 1 2 modmknepk ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑌 ∈ 𝐼 ∧ 𝐾 ∈ 𝐽 ) → ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ≠ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) )
115 7 113 8 114 syl3an ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ≠ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) )
116 eqneqall ⊢ ( ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑌 + 𝐾 ) mod 𝑁 ) → ( ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ≠ ( ( 𝑌 + 𝐾 ) mod 𝑁 ) → 𝑋 = 𝑌 ) )
117 115 116 syl5com ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑌 + 𝐾 ) mod 𝑁 ) → 𝑋 = 𝑌 ) )
118 117 adantld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( 1 = 1 ∧ ( ( 𝑌 − 𝐾 ) mod 𝑁 ) = ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ) → 𝑋 = 𝑌 ) )
119 112 118 biimtrid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
120 119 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
121 111 120 sylbid ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
122 102 108 121 3jaod ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) ∧ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) )
123 122 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
124 48 71 123 3jaod ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
125 op2ndg ⊢ ( ( 1 ∈ V ∧ 𝑋 ∈ 𝐼 ) → ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 )
126 15 125 syl ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 )
127 126 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 )
128 oveq1 ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) = ( 𝑋 + 𝐾 ) )
129 128 oveq1d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) = ( ( 𝑋 + 𝐾 ) mod 𝑁 ) )
130 129 opeq2d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ )
131 130 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ↔ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ) )
132 opeq2 ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ = ⟨ 0 , 𝑋 ⟩ )
133 132 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ↔ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ) )
134 oveq1 ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) = ( 𝑋 − 𝐾 ) )
135 134 oveq1d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) = ( ( 𝑋 − 𝐾 ) mod 𝑁 ) )
136 135 opeq2d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ )
137 136 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ↔ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) )
138 131 133 137 3orbi123d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) ↔ ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
139 130 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ↔ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ) )
140 132 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ↔ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ) )
141 136 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ↔ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) )
142 139 140 141 3orbi123d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) ↔ ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) ) )
143 142 imbi1d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ↔ ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
144 138 143 imbi12d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) = 𝑋 → ( ( ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) ↔ ( ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) ) )
145 127 144 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) ↔ ( ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , 𝑋 ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑋 − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) ) )
146 124 145 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
147 31 146 syld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
148 147 com23 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑋 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ ) → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → 𝑋 = 𝑌 ) ) )
149 25 148 syld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑋 ⟩ } ∈ 𝐸 → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → 𝑋 = 𝑌 ) ) )
150 149 impd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑋 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → 𝑋 = 𝑌 ) )
151 eqid ⊢ 1 = 1
152 151 olci ⊢ ( 1 = 0 ∨ 1 = 1 )
153 152 2a1i ⊢ ( 𝑌 ∈ 𝐼 → ( 𝑋 ∈ 𝐼 → ( 1 = 0 ∨ 1 = 1 ) ) )
154 153 imdistanri ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ( 1 = 0 ∨ 1 = 1 ) ∧ 𝑌 ∈ 𝐼 ) )
155 154 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( 1 = 0 ∨ 1 = 1 ) ∧ 𝑌 ∈ 𝐼 ) )
156 2 1 3 21 opgpgvtx ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ⟨ 1 , 𝑌 ⟩ ∈ ( Vtx ‘ 𝐺 ) ↔ ( ( 1 = 0 ∨ 1 = 1 ) ∧ 𝑌 ∈ 𝐼 ) ) )
157 9 156 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ⟨ 1 , 𝑌 ⟩ ∈ ( Vtx ‘ 𝐺 ) ↔ ( ( 1 = 0 ∨ 1 = 1 ) ∧ 𝑌 ∈ 𝐼 ) ) )
158 157 3adant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ⟨ 1 , 𝑌 ⟩ ∈ ( Vtx ‘ 𝐺 ) ↔ ( ( 1 = 0 ∨ 1 = 1 ) ∧ 𝑌 ∈ 𝐼 ) ) )
159 155 158 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ⟨ 1 , 𝑌 ⟩ ∈ ( Vtx ‘ 𝐺 ) )
160 12 a1i ⊢ ( 𝑋 ∈ 𝐼 → 1 ∈ V )
161 op1stg ⊢ ( ( 1 ∈ V ∧ 𝑌 ∈ 𝐼 ) → ( 1st ‘ ⟨ 1 , 𝑌 ⟩ ) = 1 )
162 160 161 sylan ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 1st ‘ ⟨ 1 , 𝑌 ⟩ ) = 1 )
163 162 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( 1st ‘ ⟨ 1 , 𝑌 ⟩ ) = 1 )
164 1 3 21 4 gpgedgvtx1 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( ⟨ 1 , 𝑌 ⟩ ∈ ( Vtx ‘ 𝐺 ) ∧ ( 1st ‘ ⟨ 1 , 𝑌 ⟩ ) = 1 ) ) → ( { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
165 10 159 163 164 syl12anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
166 op2ndg ⊢ ( ( 1 ∈ V ∧ 𝑌 ∈ 𝐼 ) → ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 )
167 12 166 mpan ⊢ ( 𝑌 ∈ 𝐼 → ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 )
168 oveq1 ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 → ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) = ( 𝑌 − 𝐾 ) )
169 168 oveq1d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 → ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) = ( ( 𝑌 − 𝐾 ) mod 𝑁 ) )
170 169 opeq2d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 → ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ )
171 170 preq2d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 → { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ } )
172 prcom ⊢ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ }
173 171 172 eqtrdi ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 → { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } )
174 173 eleq1d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 → ( { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ) )
175 oveq1 ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 → ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) = ( 𝑌 + 𝐾 ) )
176 175 oveq1d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 → ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) = ( ( 𝑌 + 𝐾 ) mod 𝑁 ) )
177 176 opeq2d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 → ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ )
178 177 preq2d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 → { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } )
179 178 eleq1d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 → ( { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
180 174 179 anbi12d ⊢ ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) = 𝑌 → ( ( { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
181 167 180 syl ⊢ ( 𝑌 ∈ 𝐼 → ( ( { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
182 181 biimpcd ⊢ ( ( { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 𝑌 ∈ 𝐼 → ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
183 182 ancoms ⊢ ( ( { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 𝑌 ∈ 𝐼 → ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
184 183 3adant2 ⊢ ( ( { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 𝑌 ∈ 𝐼 → ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
185 184 com12 ⊢ ( 𝑌 ∈ 𝐼 → ( ( { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
186 185 adantl ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ( { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
187 186 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 0 , ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , 𝑌 ⟩ ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
188 165 187 mpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
189 opeq2 ⊢ ( 𝑋 = 𝑌 → ⟨ 1 , 𝑋 ⟩ = ⟨ 1 , 𝑌 ⟩ )
190 189 preq2d ⊢ ( 𝑋 = 𝑌 → { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑋 ⟩ } = { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } )
191 190 eleq1d ⊢ ( 𝑋 = 𝑌 → ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑋 ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ) )
192 189 preq1d ⊢ ( 𝑋 = 𝑌 → { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } )
193 192 eleq1d ⊢ ( 𝑋 = 𝑌 → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
194 191 193 anbi12d ⊢ ( 𝑋 = 𝑌 → ( ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑋 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
195 188 194 syl5ibrcom ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( 𝑋 = 𝑌 → ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑋 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
196 150 195 impbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ ( 𝐾 ∈ 𝐽 ∧ ( ( 4 · 𝐾 ) mod 𝑁 ) ≠ 0 ) ) → ( ( { ⟨ 1 , ( ( 𝑌 − 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , 𝑋 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ 𝑋 = 𝑌 ) )