| 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 ‘ 𝑋 ) = 0 ↔ 𝑥 = 0 ) ) |
| 14 |
|
opeq1 |
⊢ ( 𝑥 = 0 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 0 , 𝑦 ⟩ ) |
| 15 |
14
|
eqeq2d |
⊢ ( 𝑥 = 0 → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 0 , 𝑦 ⟩ ) ) |
| 16 |
15
|
adantl |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑥 = 0 ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 0 , 𝑦 ⟩ ) ) |
| 17 |
|
simpr |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → 𝑦 ∈ ( 0 ..^ 𝑁 ) ) |
| 18 |
|
opeq2 |
⊢ ( 𝑧 = 𝑦 → ⟨ 0 , 𝑧 ⟩ = ⟨ 0 , 𝑦 ⟩ ) |
| 19 |
|
oveq1 |
⊢ ( 𝑧 = 𝑦 → ( 𝑧 + 1 ) = ( 𝑦 + 1 ) ) |
| 20 |
19
|
oveq1d |
⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 + 1 ) mod 𝑁 ) = ( ( 𝑦 + 1 ) mod 𝑁 ) ) |
| 21 |
20
|
opeq2d |
⊢ ( 𝑧 = 𝑦 → ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ) |
| 22 |
18 21
|
preq12d |
⊢ ( 𝑧 = 𝑦 → { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ) |
| 23 |
22
|
eqeq2d |
⊢ ( 𝑧 = 𝑦 → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ) ) |
| 24 |
|
opeq2 |
⊢ ( 𝑧 = 𝑦 → ⟨ 1 , 𝑧 ⟩ = ⟨ 1 , 𝑦 ⟩ ) |
| 25 |
18 24
|
preq12d |
⊢ ( 𝑧 = 𝑦 → { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) |
| 26 |
25
|
eqeq2d |
⊢ ( 𝑧 = 𝑦 → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) |
| 27 |
|
oveq1 |
⊢ ( 𝑧 = 𝑦 → ( 𝑧 + 𝐾 ) = ( 𝑦 + 𝐾 ) ) |
| 28 |
27
|
oveq1d |
⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 + 𝐾 ) mod 𝑁 ) = ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ) |
| 29 |
28
|
opeq2d |
⊢ ( 𝑧 = 𝑦 → ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ ) |
| 30 |
24 29
|
preq12d |
⊢ ( 𝑧 = 𝑦 → { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) |
| 31 |
30
|
eqeq2d |
⊢ ( 𝑧 = 𝑦 → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) |
| 32 |
23 26 31
|
3orbi123d |
⊢ ( 𝑧 = 𝑦 → ( ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 33 |
32
|
adantl |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑧 = 𝑦 ) → ( ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 34 |
|
eqid |
⊢ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } |
| 35 |
34
|
3mix1i |
⊢ ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) |
| 36 |
35
|
a1i |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) |
| 37 |
17 33 36
|
rspcedvd |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) |
| 38 |
22
|
eqeq2d |
⊢ ( 𝑧 = 𝑦 → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ) ) |
| 39 |
25
|
eqeq2d |
⊢ ( 𝑧 = 𝑦 → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) |
| 40 |
30
|
eqeq2d |
⊢ ( 𝑧 = 𝑦 → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) |
| 41 |
38 39 40
|
3orbi123d |
⊢ ( 𝑧 = 𝑦 → ( ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 42 |
41
|
adantl |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑧 = 𝑦 ) → ( ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 43 |
|
eqid |
⊢ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } |
| 44 |
43
|
3mix2i |
⊢ ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) |
| 45 |
44
|
a1i |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 1 , ( ( 𝑦 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) |
| 46 |
17 42 45
|
rspcedvd |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) |
| 47 |
|
elfzo0l |
⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( 𝑦 = 0 ∨ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ) |
| 48 |
|
eluzge3nn |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ ) |
| 49 |
48
|
ad2antrr |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 = 0 ) → 𝑁 ∈ ℕ ) |
| 50 |
|
fzo0end |
⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) |
| 51 |
49 50
|
syl |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 = 0 ) → ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) |
| 52 |
|
opeq2 |
⊢ ( 𝑦 = 0 → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 0 ⟩ ) |
| 53 |
|
oveq1 |
⊢ ( 𝑦 = 0 → ( 𝑦 − 1 ) = ( 0 − 1 ) ) |
| 54 |
53
|
oveq1d |
⊢ ( 𝑦 = 0 → ( ( 𝑦 − 1 ) mod 𝑁 ) = ( ( 0 − 1 ) mod 𝑁 ) ) |
| 55 |
54
|
opeq2d |
⊢ ( 𝑦 = 0 → ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ ) |
| 56 |
52 55
|
preq12d |
⊢ ( 𝑦 = 0 → { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } ) |
| 57 |
|
opeq2 |
⊢ ( 𝑧 = ( 𝑁 − 1 ) → ⟨ 0 , 𝑧 ⟩ = ⟨ 0 , ( 𝑁 − 1 ) ⟩ ) |
| 58 |
|
oveq1 |
⊢ ( 𝑧 = ( 𝑁 − 1 ) → ( 𝑧 + 1 ) = ( ( 𝑁 − 1 ) + 1 ) ) |
| 59 |
58
|
oveq1d |
⊢ ( 𝑧 = ( 𝑁 − 1 ) → ( ( 𝑧 + 1 ) mod 𝑁 ) = ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ) |
| 60 |
59
|
opeq2d |
⊢ ( 𝑧 = ( 𝑁 − 1 ) → ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ⟩ ) |
| 61 |
57 60
|
preq12d |
⊢ ( 𝑧 = ( 𝑁 − 1 ) → { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑁 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ⟩ } ) |
| 62 |
56 61
|
eqeqan12d |
⊢ ( ( 𝑦 = 0 ∧ 𝑧 = ( 𝑁 − 1 ) ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑁 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ⟩ } ) ) |
| 63 |
|
opeq2 |
⊢ ( 𝑧 = ( 𝑁 − 1 ) → ⟨ 1 , 𝑧 ⟩ = ⟨ 1 , ( 𝑁 − 1 ) ⟩ ) |
| 64 |
57 63
|
preq12d |
⊢ ( 𝑧 = ( 𝑁 − 1 ) → { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } = { ⟨ 0 , ( 𝑁 − 1 ) ⟩ , ⟨ 1 , ( 𝑁 − 1 ) ⟩ } ) |
| 65 |
56 64
|
eqeqan12d |
⊢ ( ( 𝑦 = 0 ∧ 𝑧 = ( 𝑁 − 1 ) ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ↔ { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑁 − 1 ) ⟩ , ⟨ 1 , ( 𝑁 − 1 ) ⟩ } ) ) |
| 66 |
|
oveq1 |
⊢ ( 𝑧 = ( 𝑁 − 1 ) → ( 𝑧 + 𝐾 ) = ( ( 𝑁 − 1 ) + 𝐾 ) ) |
| 67 |
66
|
oveq1d |
⊢ ( 𝑧 = ( 𝑁 − 1 ) → ( ( 𝑧 + 𝐾 ) mod 𝑁 ) = ( ( ( 𝑁 − 1 ) + 𝐾 ) mod 𝑁 ) ) |
| 68 |
67
|
opeq2d |
⊢ ( 𝑧 = ( 𝑁 − 1 ) → ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 𝑁 − 1 ) + 𝐾 ) mod 𝑁 ) ⟩ ) |
| 69 |
63 68
|
preq12d |
⊢ ( 𝑧 = ( 𝑁 − 1 ) → { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑁 − 1 ) ⟩ , ⟨ 1 , ( ( ( 𝑁 − 1 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) |
| 70 |
56 69
|
eqeqan12d |
⊢ ( ( 𝑦 = 0 ∧ 𝑧 = ( 𝑁 − 1 ) ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑁 − 1 ) ⟩ , ⟨ 1 , ( ( ( 𝑁 − 1 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) ) |
| 71 |
62 65 70
|
3orbi123d |
⊢ ( ( 𝑦 = 0 ∧ 𝑧 = ( 𝑁 − 1 ) ) → ( ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑁 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑁 − 1 ) ⟩ , ⟨ 1 , ( 𝑁 − 1 ) ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑁 − 1 ) ⟩ , ⟨ 1 , ( ( ( 𝑁 − 1 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 72 |
71
|
adantll |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 = 0 ) ∧ 𝑧 = ( 𝑁 − 1 ) ) → ( ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑁 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑁 − 1 ) ⟩ , ⟨ 1 , ( 𝑁 − 1 ) ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑁 − 1 ) ⟩ , ⟨ 1 , ( ( ( 𝑁 − 1 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 73 |
|
nncn |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ ) |
| 74 |
|
npcan1 |
⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 ) |
| 75 |
48 73 74
|
3syl |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 ) |
| 76 |
75
|
oveq1d |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) = ( 𝑁 mod 𝑁 ) ) |
| 77 |
|
nnrp |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ ) |
| 78 |
|
modid0 |
⊢ ( 𝑁 ∈ ℝ+ → ( 𝑁 mod 𝑁 ) = 0 ) |
| 79 |
48 77 78
|
3syl |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 mod 𝑁 ) = 0 ) |
| 80 |
76 79
|
eqtr2d |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 0 = ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ) |
| 81 |
80
|
opeq2d |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ⟨ 0 , 0 ⟩ = ⟨ 0 , ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ⟩ ) |
| 82 |
|
df-neg |
⊢ - 1 = ( 0 − 1 ) |
| 83 |
82
|
eqcomi |
⊢ ( 0 − 1 ) = - 1 |
| 84 |
83
|
a1i |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 0 − 1 ) = - 1 ) |
| 85 |
84
|
oveq1d |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 0 − 1 ) mod 𝑁 ) = ( - 1 mod 𝑁 ) ) |
| 86 |
|
m1modnnsub1 |
⊢ ( 𝑁 ∈ ℕ → ( - 1 mod 𝑁 ) = ( 𝑁 − 1 ) ) |
| 87 |
48 86
|
syl |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( - 1 mod 𝑁 ) = ( 𝑁 − 1 ) ) |
| 88 |
85 87
|
eqtrd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 0 − 1 ) mod 𝑁 ) = ( 𝑁 − 1 ) ) |
| 89 |
88
|
opeq2d |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 𝑁 − 1 ) ⟩ ) |
| 90 |
81 89
|
preq12d |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 𝑁 − 1 ) ⟩ } ) |
| 91 |
90
|
ad2antrr |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 = 0 ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 𝑁 − 1 ) ⟩ } ) |
| 92 |
|
prcom |
⊢ { ⟨ 0 , ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 𝑁 − 1 ) ⟩ } = { ⟨ 0 , ( 𝑁 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ⟩ } |
| 93 |
91 92
|
eqtrdi |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 = 0 ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑁 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ⟩ } ) |
| 94 |
93
|
3mix1d |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 = 0 ) → ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑁 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑁 − 1 ) + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑁 − 1 ) ⟩ , ⟨ 1 , ( 𝑁 − 1 ) ⟩ } ∨ { ⟨ 0 , 0 ⟩ , ⟨ 0 , ( ( 0 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑁 − 1 ) ⟩ , ⟨ 1 , ( ( ( 𝑁 − 1 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) ) |
| 95 |
51 72 94
|
rspcedvd |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 = 0 ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) |
| 96 |
95
|
expcom |
⊢ ( 𝑦 = 0 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 97 |
|
elfzofz |
⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 𝑦 ∈ ( 1 ... 𝑁 ) ) |
| 98 |
|
fz1fzo0m1 |
⊢ ( 𝑦 ∈ ( 1 ... 𝑁 ) → ( 𝑦 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) |
| 99 |
97 98
|
syl |
⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( 𝑦 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) |
| 100 |
99
|
adantl |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝑦 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) |
| 101 |
|
opeq2 |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → ⟨ 0 , 𝑧 ⟩ = ⟨ 0 , ( 𝑦 − 1 ) ⟩ ) |
| 102 |
|
oveq1 |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → ( 𝑧 + 1 ) = ( ( 𝑦 − 1 ) + 1 ) ) |
| 103 |
102
|
oveq1d |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → ( ( 𝑧 + 1 ) mod 𝑁 ) = ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) ) |
| 104 |
103
|
opeq2d |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) ⟩ ) |
| 105 |
101 104
|
preq12d |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) ⟩ } ) |
| 106 |
105
|
eqeq2d |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) ⟩ } ) ) |
| 107 |
|
opeq2 |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → ⟨ 1 , 𝑧 ⟩ = ⟨ 1 , ( 𝑦 − 1 ) ⟩ ) |
| 108 |
101 107
|
preq12d |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } = { ⟨ 0 , ( 𝑦 − 1 ) ⟩ , ⟨ 1 , ( 𝑦 − 1 ) ⟩ } ) |
| 109 |
108
|
eqeq2d |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 1 ) ⟩ , ⟨ 1 , ( 𝑦 − 1 ) ⟩ } ) ) |
| 110 |
|
oveq1 |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → ( 𝑧 + 𝐾 ) = ( ( 𝑦 − 1 ) + 𝐾 ) ) |
| 111 |
110
|
oveq1d |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → ( ( 𝑧 + 𝐾 ) mod 𝑁 ) = ( ( ( 𝑦 − 1 ) + 𝐾 ) mod 𝑁 ) ) |
| 112 |
111
|
opeq2d |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( ( 𝑦 − 1 ) + 𝐾 ) mod 𝑁 ) ⟩ ) |
| 113 |
107 112
|
preq12d |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑦 − 1 ) ⟩ , ⟨ 1 , ( ( ( 𝑦 − 1 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) |
| 114 |
113
|
eqeq2d |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑦 − 1 ) ⟩ , ⟨ 1 , ( ( ( 𝑦 − 1 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) ) |
| 115 |
106 109 114
|
3orbi123d |
⊢ ( 𝑧 = ( 𝑦 − 1 ) → ( ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 1 ) ⟩ , ⟨ 1 , ( 𝑦 − 1 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑦 − 1 ) ⟩ , ⟨ 1 , ( ( ( 𝑦 − 1 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 116 |
115
|
adantl |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) ∧ 𝑧 = ( 𝑦 − 1 ) ) → ( ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 1 ) ⟩ , ⟨ 1 , ( 𝑦 − 1 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑦 − 1 ) ⟩ , ⟨ 1 , ( ( ( 𝑦 − 1 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 117 |
|
elfzoelz |
⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → 𝑦 ∈ ℤ ) |
| 118 |
|
zcn |
⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ ) |
| 119 |
|
npcan1 |
⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 − 1 ) + 1 ) = 𝑦 ) |
| 120 |
117 118 119
|
3syl |
⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( ( 𝑦 − 1 ) + 1 ) = 𝑦 ) |
| 121 |
120
|
oveq1d |
⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) = ( 𝑦 mod 𝑁 ) ) |
| 122 |
|
elfzo1 |
⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) ) |
| 123 |
|
nnre |
⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ ) |
| 124 |
123 77
|
anim12i |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ) |
| 125 |
124
|
3adant3 |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ) |
| 126 |
|
nnnn0 |
⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℕ0 ) |
| 127 |
126
|
nn0ge0d |
⊢ ( 𝑦 ∈ ℕ → 0 ≤ 𝑦 ) |
| 128 |
127
|
anim1i |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑦 < 𝑁 ) → ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) |
| 129 |
128
|
3adant2 |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) |
| 130 |
125 129
|
jca |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) ) |
| 131 |
122 130
|
sylbi |
⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) ) |
| 132 |
|
modid |
⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝑦 mod 𝑁 ) = 𝑦 ) |
| 133 |
131 132
|
syl |
⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( 𝑦 mod 𝑁 ) = 𝑦 ) |
| 134 |
121 133
|
eqtrd |
⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) = 𝑦 ) |
| 135 |
134
|
adantl |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) = 𝑦 ) |
| 136 |
135
|
eqcomd |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → 𝑦 = ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) ) |
| 137 |
136
|
opeq2d |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) ⟩ ) |
| 138 |
|
1red |
⊢ ( 𝑦 ∈ ℕ → 1 ∈ ℝ ) |
| 139 |
123 138
|
resubcld |
⊢ ( 𝑦 ∈ ℕ → ( 𝑦 − 1 ) ∈ ℝ ) |
| 140 |
139 77
|
anim12i |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑦 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ) |
| 141 |
140
|
3adant3 |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → ( ( 𝑦 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ) |
| 142 |
|
nnm1ge0 |
⊢ ( 𝑦 ∈ ℕ → 0 ≤ ( 𝑦 − 1 ) ) |
| 143 |
142
|
3ad2ant1 |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → 0 ≤ ( 𝑦 − 1 ) ) |
| 144 |
139
|
3ad2ant1 |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → ( 𝑦 − 1 ) ∈ ℝ ) |
| 145 |
123
|
3ad2ant1 |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → 𝑦 ∈ ℝ ) |
| 146 |
|
nnre |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ ) |
| 147 |
146
|
3ad2ant2 |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → 𝑁 ∈ ℝ ) |
| 148 |
123
|
ltm1d |
⊢ ( 𝑦 ∈ ℕ → ( 𝑦 − 1 ) < 𝑦 ) |
| 149 |
148
|
3ad2ant1 |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → ( 𝑦 − 1 ) < 𝑦 ) |
| 150 |
|
simp3 |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → 𝑦 < 𝑁 ) |
| 151 |
144 145 147 149 150
|
lttrd |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → ( 𝑦 − 1 ) < 𝑁 ) |
| 152 |
141 143 151
|
jca32 |
⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑦 < 𝑁 ) → ( ( ( 𝑦 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝑦 − 1 ) ∧ ( 𝑦 − 1 ) < 𝑁 ) ) ) |
| 153 |
122 152
|
sylbi |
⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( ( ( 𝑦 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝑦 − 1 ) ∧ ( 𝑦 − 1 ) < 𝑁 ) ) ) |
| 154 |
153
|
adantl |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( ( ( 𝑦 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝑦 − 1 ) ∧ ( 𝑦 − 1 ) < 𝑁 ) ) ) |
| 155 |
|
modid |
⊢ ( ( ( ( 𝑦 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝑦 − 1 ) ∧ ( 𝑦 − 1 ) < 𝑁 ) ) → ( ( 𝑦 − 1 ) mod 𝑁 ) = ( 𝑦 − 1 ) ) |
| 156 |
154 155
|
syl |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝑦 − 1 ) mod 𝑁 ) = ( 𝑦 − 1 ) ) |
| 157 |
156
|
opeq2d |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( 𝑦 − 1 ) ⟩ ) |
| 158 |
137 157
|
preq12d |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 𝑦 − 1 ) ⟩ } ) |
| 159 |
|
prcom |
⊢ { ⟨ 0 , ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , ( 𝑦 − 1 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) ⟩ } |
| 160 |
158 159
|
eqtrdi |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) ⟩ } ) |
| 161 |
160
|
3mix1d |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 1 ) ⟩ , ⟨ 0 , ( ( ( 𝑦 − 1 ) + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( 𝑦 − 1 ) ⟩ , ⟨ 1 , ( 𝑦 − 1 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , ( 𝑦 − 1 ) ⟩ , ⟨ 1 , ( ( ( 𝑦 − 1 ) + 𝐾 ) mod 𝑁 ) ⟩ } ) ) |
| 162 |
100 116 161
|
rspcedvd |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) |
| 163 |
162
|
expcom |
⊢ ( 𝑦 ∈ ( 1 ..^ 𝑁 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 164 |
96 163
|
jaoi |
⊢ ( ( 𝑦 = 0 ∨ 𝑦 ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 165 |
47 164
|
syl |
⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 166 |
165
|
impcom |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) |
| 167 |
5 1 2 4
|
gpgedgel |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 168 |
5 1 2 4
|
gpgedgel |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ↔ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 169 |
5 1 2 4
|
gpgedgel |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) |
| 170 |
167 168 169
|
3anbi123d |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ ( ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ∧ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ∧ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) ) |
| 171 |
170
|
adantr |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ ( ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ∧ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ∧ ∃ 𝑧 ∈ ( 0 ..^ 𝑁 ) ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 0 , ( ( 𝑧 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑧 ⟩ , ⟨ 1 , 𝑧 ⟩ } ∨ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑧 ⟩ , ⟨ 1 , ( ( 𝑧 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) ) |
| 172 |
37 46 166 171
|
mpbir3and |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) |
| 173 |
172
|
adantrl |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) |
| 174 |
|
id |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → 𝑋 = ⟨ 0 , 𝑦 ⟩ ) |
| 175 |
|
c0ex |
⊢ 0 ∈ V |
| 176 |
175 10
|
op2ndd |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 2nd ‘ 𝑋 ) = 𝑦 ) |
| 177 |
176
|
oveq1d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( 2nd ‘ 𝑋 ) + 1 ) = ( 𝑦 + 1 ) ) |
| 178 |
177
|
oveq1d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) = ( ( 𝑦 + 1 ) mod 𝑁 ) ) |
| 179 |
178
|
opeq2d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ ) |
| 180 |
174 179
|
preq12d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ) |
| 181 |
180
|
eleq1d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) |
| 182 |
176
|
opeq2d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ = ⟨ 1 , 𝑦 ⟩ ) |
| 183 |
174 182
|
preq12d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → { 𝑋 , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) |
| 184 |
183
|
eleq1d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( { 𝑋 , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ) ) |
| 185 |
176
|
oveq1d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( 2nd ‘ 𝑋 ) − 1 ) = ( 𝑦 − 1 ) ) |
| 186 |
185
|
oveq1d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) = ( ( 𝑦 − 1 ) mod 𝑁 ) ) |
| 187 |
186
|
opeq2d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ ) |
| 188 |
174 187
|
preq12d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } ) |
| 189 |
188
|
eleq1d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) |
| 190 |
181 184 189
|
3anbi123d |
⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑦 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) ) |
| 191 |
173 190
|
syl5ibrcom |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) ) |
| 192 |
191
|
adantr |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑥 = 0 ) → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) ) |
| 193 |
16 192
|
sylbid |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑥 = 0 ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) ) |
| 194 |
193
|
impancom |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑥 = 0 → ( { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) ) |
| 195 |
13 194
|
sylbid |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) ∧ 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 1st ‘ 𝑋 ) = 0 → ( { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) ) |
| 196 |
195
|
ex |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 𝑁 ) ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1st ‘ 𝑋 ) = 0 → ( { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) ) ) |
| 197 |
196
|
rexlimdvva |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1st ‘ 𝑋 ) = 0 → ( { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) ) ) |
| 198 |
6 197
|
sylbid |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑋 ∈ 𝑉 → ( ( 1st ‘ 𝑋 ) = 0 → ( { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) ) ) |
| 199 |
198
|
imp32 |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ } ∈ 𝐸 ∧ { 𝑋 , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) |