Metamath Proof Explorer

Theorem gpgvtxedg0

Description: The edges starting at a vertex X of the first kind in a generalized Petersen graph G . (Contributed by AV, 30-Aug-2025)

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