Metamath Proof Explorer

Theorem gpgedgvtx1

Description: The edges starting at an inside vertex 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 gpgedgvtx1 ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 gpgedgvtx0.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2 gpgedgvtx0.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
3 gpgedgvtx0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4 gpgedgvtx0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
5 eqid ⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
6 5 1 2 3 gpgvtxel ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) )
7 fveq2 ⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st ‘ 𝑋 ) = ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
8 7 adantl ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 1st ‘ 𝑋 ) = ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
9 vex ⊢ 𝑥 ∈ V
10 vex ⊢ 𝑦 ∈ V
11 9 10 op1st ⊢ ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑥
12 8 11 eqtrdi ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 1st ‘ 𝑋 ) = 𝑥 )
13 12 eqeq1d ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 1st ‘ 𝑋 ) = 1 ↔ 𝑥 = 1 ) )
14 opeq1 ⊢ ( 𝑥 = 1 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 1 , 𝑦 ⟩ )
15 14 eqeq2d ⊢ ( 𝑥 = 1 → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) )
16 15 adantl ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑥 = 1 ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) )
17 opeq2 ⊢ ( 𝑧 = 𝑦 → ⟨ 0 , 𝑧 ⟩ = ⟨ 0 , 𝑦 ⟩ )
18 oveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 + 1 ) = ( 𝑦 + 1 ) )
19 18 oveq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 + 1 ) mod 𝑁 ) = ( ( 𝑦 + 1 ) mod 𝑁 ) )
20 19 opeq2d ⊢ ( 𝑧 = 𝑦 → ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ )
21 17 20 preq12d ⊢ ( 𝑧 = 𝑦 → { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } )
22 21 eqeq2d ⊢ ( 𝑧 = 𝑦 → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ) )
23 opeq2 ⊢ ( 𝑧 = 𝑦 → ⟨ 1 , 𝑧 ⟩ = ⟨ 1 , 𝑦 ⟩ )
24 17 23 preq12d ⊢ ( 𝑧 = 𝑦 → { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } )
25 24 eqeq2d ⊢ ( 𝑧 = 𝑦 → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) )
26 oveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 + 𝐾 ) = ( 𝑦 + 𝐾 ) )
27 26 oveq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 + 𝐾 ) mod 𝑁 ) = ( ( 𝑦 + 𝐾 ) mod 𝑁 ) )
28 27 opeq2d ⊢ ( 𝑧 = 𝑦 → ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ )
29 23 28 preq12d ⊢ ( 𝑧 = 𝑦 → { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } )
30 29 eqeq2d ⊢ ( 𝑧 = 𝑦 → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
31 22 25 30 3orbi123d ⊢ ( 𝑧 = 𝑦 → ( ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
32 simpr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑦 ∈ ( 0 ..^ 𝑁 ) )
33 eqid ⊢ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ }
34 33 3mix3i ⊢ ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } )
35 34 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
36 31 32 35 rspcedvdw ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
37 21 eqeq2d ⊢ ( 𝑧 = 𝑦 → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ) )
38 24 eqeq2d ⊢ ( 𝑧 = 𝑦 → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) )
39 29 eqeq2d ⊢ ( 𝑧 = 𝑦 → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
40 37 38 39 3orbi123d ⊢ ( 𝑧 = 𝑦 → ( ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
41 prcom ⊢ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ }
42 41 3mix2i ⊢ ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } )
43 42 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
44 40 32 43 rspcedvdw ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
45 elfzoelz ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℤ )
46 45 1 eleq2s ⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℤ )
47 46 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝐾 ∈ ℤ )
48 47 anim1ci ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ℤ ) )
49 fzospliti ⊢ ( ( 𝑦 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐾 ∈ ℤ ) → ( 𝑦 ∈ ( 0 ..^ 𝐾 ) ∨ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) )
50 48 49 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 0 ..^ 𝐾 ) ∨ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) )
51 50 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( 𝑦 ∈ ( 0 ..^ 𝐾 ) ∨ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) ) )
52 opeq2 ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → ⟨ 0 , 𝑧 ⟩ = ⟨ 0 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ )
53 oveq1 ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → ( 𝑧 + 1 ) = ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 1 ) )
54 53 oveq1d ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → ( ( 𝑧 + 1 ) mod 𝑁 ) = ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 1 ) mod 𝑁 ) )
55 54 opeq2d ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 1 ) mod 𝑁 ) ⟩ )
56 52 55 preq12d ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 0 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 1 ) mod 𝑁 ) ⟩ } )
57 56 eqeq2d ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 0 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 1 ) mod 𝑁 ) ⟩ } ) )
58 opeq2 ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → ⟨ 1 , 𝑧 ⟩ = ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ )
59 52 58 preq12d ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } = { ⟨ 0 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ } )
60 59 eqeq2d ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ } ) )
61 oveq1 ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → ( 𝑧 + 𝐾 ) = ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) )
62 61 oveq1d ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → ( ( 𝑧 + 𝐾 ) mod 𝑁 ) = ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) mod 𝑁 ) )
63 62 opeq2d ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ )
64 58 63 preq12d ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 1 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ } )
65 64 eqeq2d ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 1 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) )
66 57 60 65 3orbi123d ⊢ ( 𝑧 = ( ( 𝑁 + 𝑦 ) − 𝐾 ) → ( ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 0 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 1 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
67 eluz3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
68 67 nnzd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
69 68 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝑁 ∈ ℤ )
70 69 zcnd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝑁 ∈ ℂ )
71 70 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝑁 ∈ ℂ )
72 elfzoel2 ⊢ ( 𝑦 ∈ ( 0 ..^ 𝐾 ) → 𝐾 ∈ ℤ )
73 72 zcnd ⊢ ( 𝑦 ∈ ( 0 ..^ 𝐾 ) → 𝐾 ∈ ℂ )
74 73 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝐾 ∈ ℂ )
75 elfzoelz ⊢ ( 𝑦 ∈ ( 0 ..^ 𝐾 ) → 𝑦 ∈ ℤ )
76 75 zcnd ⊢ ( 𝑦 ∈ ( 0 ..^ 𝐾 ) → 𝑦 ∈ ℂ )
77 76 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝑦 ∈ ℂ )
78 71 74 77 subsub3d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( 𝑁 − ( 𝐾 − 𝑦 ) ) = ( ( 𝑁 + 𝑦 ) − 𝐾 ) )
79 1zzd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 1 ∈ ℤ )
80 69 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝑁 ∈ ℤ )
81 72 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝐾 ∈ ℤ )
82 75 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝑦 ∈ ℤ )
83 81 82 zsubcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( 𝐾 − 𝑦 ) ∈ ℤ )
84 elfzo0subge1 ⊢ ( 𝑦 ∈ ( 0 ..^ 𝐾 ) → 1 ≤ ( 𝐾 − 𝑦 ) )
85 84 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 1 ≤ ( 𝐾 − 𝑦 ) )
86 83 zred ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( 𝐾 − 𝑦 ) ∈ ℝ )
87 81 zred ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝐾 ∈ ℝ )
88 80 zred ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝑁 ∈ ℝ )
89 elfzo0suble ⊢ ( 𝑦 ∈ ( 0 ..^ 𝐾 ) → ( 𝐾 − 𝑦 ) ≤ 𝐾 )
90 89 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( 𝐾 − 𝑦 ) ≤ 𝐾 )
91 1 5 gpgedgvtx1lem ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )
92 elfzo0le ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ≤ 𝑁 )
93 91 92 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝐾 ≤ 𝑁 )
94 93 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝐾 ≤ 𝑁 )
95 86 87 88 90 94 letrd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( 𝐾 − 𝑦 ) ≤ 𝑁 )
96 79 80 83 85 95 elfzd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( 𝐾 − 𝑦 ) ∈ ( 1 ... 𝑁 ) )
97 ubmelfzo ⊢ ( ( 𝐾 − 𝑦 ) ∈ ( 1 ... 𝑁 ) → ( 𝑁 − ( 𝐾 − 𝑦 ) ) ∈ ( 0 ..^ 𝑁 ) )
98 96 97 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( 𝑁 − ( 𝐾 − 𝑦 ) ) ∈ ( 0 ..^ 𝑁 ) )
99 78 98 eqeltrrd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( ( 𝑁 + 𝑦 ) − 𝐾 ) ∈ ( 0 ..^ 𝑁 ) )
100 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℂ )
101 100 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝑁 ∈ ℂ )
102 101 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝑁 ∈ ℂ )
103 102 77 addcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( 𝑁 + 𝑦 ) ∈ ℂ )
104 103 74 npcand ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) = ( 𝑁 + 𝑦 ) )
105 104 oveq1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) mod 𝑁 ) = ( ( 𝑁 + 𝑦 ) mod 𝑁 ) )
106 elfzonn0 ⊢ ( 𝑦 ∈ ( 0 ..^ 𝐾 ) → 𝑦 ∈ ℕ0 )
107 106 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝑦 ∈ ℕ0 )
108 67 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝑁 ∈ ℕ )
109 108 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝑁 ∈ ℕ )
110 elfzouz2 ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
111 fzoss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 0 ..^ 𝐾 ) ⊆ ( 0 ..^ 𝑁 ) )
112 110 111 syl ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 0 ..^ 𝐾 ) ⊆ ( 0 ..^ 𝑁 ) )
113 112 sseld ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑦 ∈ ( 0 ..^ 𝐾 ) → 𝑦 ∈ ( 0 ..^ 𝑁 ) ) )
114 elfzolt2 ⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 𝑦 < 𝑁 )
115 113 114 syl6 ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑦 ∈ ( 0 ..^ 𝐾 ) → 𝑦 < 𝑁 ) )
116 91 115 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑦 ∈ ( 0 ..^ 𝐾 ) → 𝑦 < 𝑁 ) )
117 116 imp ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝑦 < 𝑁 )
118 addmodid ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → ( ( 𝑁 + 𝑦 ) mod 𝑁 ) = 𝑦 )
119 107 109 117 118 syl3anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( ( 𝑁 + 𝑦 ) mod 𝑁 ) = 𝑦 )
120 105 119 eqtr2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝑦 = ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) mod 𝑁 ) )
121 120 opeq2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ⟨ 1 , 𝑦 ⟩ = ⟨ 1 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ )
122 simpr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝑦 ∈ ( 0 ..^ 𝐾 ) )
123 elfzolt2 ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 < 𝑁 )
124 91 123 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝐾 < 𝑁 )
125 124 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → 𝐾 < 𝑁 )
126 submodlt ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ∧ 𝐾 < 𝑁 ) → ( ( 𝑦 − 𝐾 ) mod 𝑁 ) = ( ( 𝑁 + 𝑦 ) − 𝐾 ) )
127 109 122 125 126 syl3anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( ( 𝑦 − 𝐾 ) mod 𝑁 ) = ( ( 𝑁 + 𝑦 ) − 𝐾 ) )
128 127 opeq2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ )
129 121 128 preq12d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ } )
130 prcom ⊢ { ⟨ 1 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ } = { ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 1 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ }
131 129 130 eqtrdi ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 1 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ } )
132 131 3mix3d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 0 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( ( 𝑁 + 𝑦 ) − 𝐾 ) ⟩ , ⟨ 1 , ( ( ( ( 𝑁 + 𝑦 ) − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) )
133 66 99 132 rspcedvdw ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝐾 ) ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
134 133 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑦 ∈ ( 0 ..^ 𝐾 ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
135 opeq2 ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → ⟨ 0 , 𝑧 ⟩ = ⟨ 0 , ( 𝑦 − 𝐾 ) ⟩ )
136 oveq1 ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → ( 𝑧 + 1 ) = ( ( 𝑦 − 𝐾 ) + 1 ) )
137 136 oveq1d ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → ( ( 𝑧 + 1 ) mod 𝑁 ) = ( ( ( 𝑦 − 𝐾 ) + 1 ) mod 𝑁 ) )
138 137 opeq2d ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 𝑦 − 𝐾 ) + 1 ) mod 𝑁 ) ⟩ )
139 135 138 preq12d ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 0 , ( ( ( 𝑦 − 𝐾 ) + 1 ) mod 𝑁 ) ⟩ } )
140 139 eqeq2d ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 0 , ( ( ( 𝑦 − 𝐾 ) + 1 ) mod 𝑁 ) ⟩ } ) )
141 opeq2 ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → ⟨ 1 , 𝑧 ⟩ = ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ )
142 135 141 preq12d ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } = { ⟨ 0 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ } )
143 142 eqeq2d ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ } ) )
144 oveq1 ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → ( 𝑧 + 𝐾 ) = ( ( 𝑦 − 𝐾 ) + 𝐾 ) )
145 144 oveq1d ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → ( ( 𝑧 + 𝐾 ) mod 𝑁 ) = ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) )
146 145 opeq2d ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ )
147 141 146 preq12d ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 1 , ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ } )
148 147 eqeq2d ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 1 , ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) )
149 140 143 148 3orbi123d ⊢ ( 𝑧 = ( 𝑦 − 𝐾 ) → ( ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 0 , ( ( ( 𝑦 − 𝐾 ) + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 1 , ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
150 elfzo1 ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ↔ ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
151 150 simp1bi ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℕ )
152 151 nnnn0d ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℕ0 )
153 152 1 eleq2s ⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℕ0 )
154 153 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝐾 ∈ ℕ0 )
155 elfzoextl ⊢ ( ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑦 ∈ ( 𝐾 ..^ ( 𝐾 + 𝑁 ) ) )
156 154 155 sylan2 ⊢ ( ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → 𝑦 ∈ ( 𝐾 ..^ ( 𝐾 + 𝑁 ) ) )
157 156 ancoms ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → 𝑦 ∈ ( 𝐾 ..^ ( 𝐾 + 𝑁 ) ) )
158 108 nnzd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝑁 ∈ ℤ )
159 158 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → 𝑁 ∈ ℤ )
160 fzosubel3 ⊢ ( ( 𝑦 ∈ ( 𝐾 ..^ ( 𝐾 + 𝑁 ) ) ∧ 𝑁 ∈ ℤ ) → ( 𝑦 − 𝐾 ) ∈ ( 0 ..^ 𝑁 ) )
161 157 159 160 syl2anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → ( 𝑦 − 𝐾 ) ∈ ( 0 ..^ 𝑁 ) )
162 elfzoelz ⊢ ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) → 𝑦 ∈ ℤ )
163 162 zcnd ⊢ ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) → 𝑦 ∈ ℂ )
164 elfzoel1 ⊢ ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) → 𝐾 ∈ ℤ )
165 164 zcnd ⊢ ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) → 𝐾 ∈ ℂ )
166 163 165 npcand ⊢ ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) → ( ( 𝑦 − 𝐾 ) + 𝐾 ) = 𝑦 )
167 166 oveq1d ⊢ ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) → ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) = ( 𝑦 mod 𝑁 ) )
168 167 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) = ( 𝑦 mod 𝑁 ) )
169 67 nnrpd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℝ+ )
170 169 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝑁 ∈ ℝ+ )
171 162 zred ⊢ ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) → 𝑦 ∈ ℝ )
172 170 171 anim12ci ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
173 elfzole1 ⊢ ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) → 𝐾 ≤ 𝑦 )
174 173 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → 𝐾 ≤ 𝑦 )
175 0red ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) ∧ 𝐾 ≤ 𝑦 ) → 0 ∈ ℝ )
176 164 zred ⊢ ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) → 𝐾 ∈ ℝ )
177 176 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) ∧ 𝐾 ≤ 𝑦 ) → 𝐾 ∈ ℝ )
178 171 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) ∧ 𝐾 ≤ 𝑦 ) → 𝑦 ∈ ℝ )
179 nnnn0 ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ0 )
180 179 nn0ge0d ⊢ ( 𝐾 ∈ ℕ → 0 ≤ 𝐾 )
181 151 180 syl ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 0 ≤ 𝐾 )
182 181 1 eleq2s ⊢ ( 𝐾 ∈ 𝐽 → 0 ≤ 𝐾 )
183 182 ad3antlr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) ∧ 𝐾 ≤ 𝑦 ) → 0 ≤ 𝐾 )
184 simpr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) ∧ 𝐾 ≤ 𝑦 ) → 𝐾 ≤ 𝑦 )
185 175 177 178 183 184 letrd ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) ∧ 𝐾 ≤ 𝑦 ) → 0 ≤ 𝑦 )
186 174 185 mpdan ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → 0 ≤ 𝑦 )
187 elfzolt2 ⊢ ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) → 𝑦 < 𝑁 )
188 187 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → 𝑦 < 𝑁 )
189 modid ⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝑦 mod 𝑁 ) = 𝑦 )
190 172 186 188 189 syl12anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → ( 𝑦 mod 𝑁 ) = 𝑦 )
191 168 190 eqtr2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → 𝑦 = ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) )
192 191 opeq2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → ⟨ 1 , 𝑦 ⟩ = ⟨ 1 , ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ )
193 171 176 resubcld ⊢ ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) → ( 𝑦 − 𝐾 ) ∈ ℝ )
194 170 193 anim12ci ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → ( ( 𝑦 − 𝐾 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
195 elfzo2 ⊢ ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ↔ ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) )
196 eluz2 ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) )
197 simp13 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → 𝐾 ≤ 𝑦 )
198 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
199 zre ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℝ )
200 198 199 anim12ci ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑦 ∈ ℝ ∧ 𝐾 ∈ ℝ ) )
201 200 3adant3 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) → ( 𝑦 ∈ ℝ ∧ 𝐾 ∈ ℝ ) )
202 201 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → ( 𝑦 ∈ ℝ ∧ 𝐾 ∈ ℝ ) )
203 subge0 ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 0 ≤ ( 𝑦 − 𝐾 ) ↔ 𝐾 ≤ 𝑦 ) )
204 202 203 syl ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → ( 0 ≤ ( 𝑦 − 𝐾 ) ↔ 𝐾 ≤ 𝑦 ) )
205 197 204 mpbird ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → 0 ≤ ( 𝑦 − 𝐾 ) )
206 199 3ad2ant2 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) → 𝑦 ∈ ℝ )
207 206 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → 𝑦 ∈ ℝ )
208 198 3ad2ant1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) → 𝐾 ∈ ℝ )
209 208 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → 𝐾 ∈ ℝ )
210 207 209 resubcld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → ( 𝑦 − 𝐾 ) ∈ ℝ )
211 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
212 211 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) → 𝑁 ∈ ℝ )
213 212 3ad2ant2 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → 𝑁 ∈ ℝ )
214 nnrp ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ+ )
215 214 3ad2ant1 ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ∧ 𝐾 < ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℝ+ )
216 150 215 sylbi ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℝ+ )
217 216 1 eleq2s ⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℝ+ )
218 217 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝐾 ∈ ℝ+ )
219 218 3ad2ant3 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → 𝐾 ∈ ℝ+ )
220 207 219 ltsubrpd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → ( 𝑦 − 𝐾 ) < 𝑦 )
221 simp2r ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → 𝑦 < 𝑁 )
222 210 207 213 220 221 lttrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → ( 𝑦 − 𝐾 ) < 𝑁 )
223 205 222 jca ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ) → ( 0 ≤ ( 𝑦 − 𝐾 ) ∧ ( 𝑦 − 𝐾 ) < 𝑁 ) )
224 223 3exp ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) → ( ( 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 0 ≤ ( 𝑦 − 𝐾 ) ∧ ( 𝑦 − 𝐾 ) < 𝑁 ) ) ) )
225 224 expd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ≤ 𝑦 ) → ( 𝑁 ∈ ℤ → ( 𝑦 < 𝑁 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 0 ≤ ( 𝑦 − 𝐾 ) ∧ ( 𝑦 − 𝐾 ) < 𝑁 ) ) ) ) )
226 196 225 sylbi ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑁 ∈ ℤ → ( 𝑦 < 𝑁 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 0 ≤ ( 𝑦 − 𝐾 ) ∧ ( 𝑦 − 𝐾 ) < 𝑁 ) ) ) ) )
227 226 3imp ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 0 ≤ ( 𝑦 − 𝐾 ) ∧ ( 𝑦 − 𝐾 ) < 𝑁 ) ) )
228 195 227 sylbi ⊢ ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 0 ≤ ( 𝑦 − 𝐾 ) ∧ ( 𝑦 − 𝐾 ) < 𝑁 ) ) )
229 228 impcom ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → ( 0 ≤ ( 𝑦 − 𝐾 ) ∧ ( 𝑦 − 𝐾 ) < 𝑁 ) )
230 modid ⊢ ( ( ( ( 𝑦 − 𝐾 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝑦 − 𝐾 ) ∧ ( 𝑦 − 𝐾 ) < 𝑁 ) ) → ( ( 𝑦 − 𝐾 ) mod 𝑁 ) = ( 𝑦 − 𝐾 ) )
231 194 229 230 syl2anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → ( ( 𝑦 − 𝐾 ) mod 𝑁 ) = ( 𝑦 − 𝐾 ) )
232 231 opeq2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ )
233 192 232 preq12d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ } )
234 prcom ⊢ { ⟨ 1 , ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ } = { ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 1 , ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ }
235 233 234 eqtrdi ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 1 , ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ } )
236 235 3mix3d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 0 , ( ( ( 𝑦 − 𝐾 ) + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑦 − 𝐾 ) ⟩ , ⟨ 1 , ( ( ( 𝑦 − 𝐾 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) )
237 149 161 236 rspcedvdw ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
238 237 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
239 134 238 jaod ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ( 𝑦 ∈ ( 0 ..^ 𝐾 ) ∨ 𝑦 ∈ ( 𝐾 ..^ 𝑁 ) ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
240 51 239 syld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
241 240 imp ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
242 5 1 2 4 gpgedgel ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
243 5 1 2 4 gpgedgel ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } ∈ 𝐸 ↔ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
244 5 1 2 4 gpgedgel ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
245 242 243 244 3anbi123d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ ( ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ∧ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ∧ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) )
246 245 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ ( ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ∧ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ∧ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) )
247 36 44 241 246 mpbir3and ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
248 247 adantrl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
249 id ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → 𝑋 = ⟨ 1 , 𝑦 ⟩ )
250 1ex ⊢ 1 ∈ V
251 250 10 op2ndd ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( 2nd ‘ 𝑋 ) = 𝑦 )
252 251 oveq1d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( 2nd ‘ 𝑋 ) + 𝐾 ) = ( 𝑦 + 𝐾 ) )
253 252 oveq1d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) = ( ( 𝑦 + 𝐾 ) mod 𝑁 ) )
254 253 opeq2d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ )
255 249 254 preq12d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } )
256 255 eleq1d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
257 251 opeq2d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ = ⟨ 0 , 𝑦 ⟩ )
258 249 257 preq12d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → { 𝑋 , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } )
259 258 eleq1d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( { 𝑋 , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } ∈ 𝐸 ) )
260 251 oveq1d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( 2nd ‘ 𝑋 ) − 𝐾 ) = ( 𝑦 − 𝐾 ) )
261 260 oveq1d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) = ( ( 𝑦 − 𝐾 ) mod 𝑁 ) )
262 261 opeq2d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ )
263 249 262 preq12d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } )
264 263 eleq1d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
265 256 259 264 3anbi123d ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑦 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
266 248 265 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
267 266 adantr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑥 = 1 ) → ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
268 16 267 sylbid ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑥 = 1 ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
269 268 impancom ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑥 = 1 → ( { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
270 13 269 sylbid ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 1st ‘ 𝑋 ) = 1 → ( { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
271 270 ex ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1st ‘ 𝑋 ) = 1 → ( { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) ) )
272 271 rexlimdvva ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1st ‘ 𝑋 ) = 1 → ( { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) ) )
273 6 272 sylbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 → ( ( 1st ‘ 𝑋 ) = 1 → ( { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) ) )
274 273 imp32 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → ( { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )