Metamath Proof Explorer

Theorem gpgvtxedg1

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

Ref Expression
Hypotheses gpgedgvtx0.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgedgvtx0.g 
|- G = ( N gPetersenGr K )
gpgedgvtx0.v 
|- V = ( Vtx ` G )
gpgedgvtx0.e 
|- E = ( Edg ` G )
Assertion gpgvtxedg1 
|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ { X , Y } e. E ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) )

Proof

Step Hyp Ref Expression
1 gpgedgvtx0.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 gpgedgvtx0.g 
 |-  G = ( N gPetersenGr K )
3 gpgedgvtx0.v 
 |-  V = ( Vtx ` G )
4 gpgedgvtx0.e 
 |-  E = ( Edg ` G )
5 gpgusgra 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) -> ( N gPetersenGr K ) e. USGraph )
6 1 eleq2i 
 |-  ( K e. J <-> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
7 6 anbi2i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) <-> ( N e. ( ZZ>= ` 3 ) /\ K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) ) )
8 2 eleq1i 
 |-  ( G e. USGraph <-> ( N gPetersenGr K ) e. USGraph )
9 5 7 8 3imtr4i 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> G e. USGraph )
10 9 3ad2ant1 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ { X , Y } e. E ) -> G e. USGraph )
11 simp3 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ { X , Y } e. E ) -> { X , Y } e. E )
12 4 3 usgrpredgv 
 |-  ( ( G e. USGraph /\ { X , Y } e. E ) -> ( X e. V /\ Y e. V ) )
13 10 11 12 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ { X , Y } e. E ) -> ( X e. V /\ Y e. V ) )
14 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
15 14 1 2 4 gpgedgel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( { X , Y } e. E <-> E. y e. ( 0 ..^ N ) ( { X , Y } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { X , Y } = { <. 0 , y >. , <. 1 , y >. } \/ { X , Y } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) ) )
16 15 3ad2ant1 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) -> ( { X , Y } e. E <-> E. y e. ( 0 ..^ N ) ( { X , Y } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { X , Y } = { <. 0 , y >. , <. 1 , y >. } \/ { X , Y } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) ) )
17 simp3 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) -> ( X e. V /\ Y e. V ) )
18 17 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( X e. V /\ Y e. V ) )
19 opex 
 |-  <. 0 , y >. e. _V
20 opex 
 |-  <. 0 , ( ( y + 1 ) mod N ) >. e. _V
21 19 20 pm3.2i 
 |-  ( <. 0 , y >. e. _V /\ <. 0 , ( ( y + 1 ) mod N ) >. e. _V )
22 preq12bg 
 |-  ( ( ( X e. V /\ Y e. V ) /\ ( <. 0 , y >. e. _V /\ <. 0 , ( ( y + 1 ) mod N ) >. e. _V ) ) -> ( { X , Y } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } <-> ( ( X = <. 0 , y >. /\ Y = <. 0 , ( ( y + 1 ) mod N ) >. ) \/ ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) ) ) )
23 18 21 22 sylancl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( { X , Y } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } <-> ( ( X = <. 0 , y >. /\ Y = <. 0 , ( ( y + 1 ) mod N ) >. ) \/ ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) ) ) )
24 c0ex 
 |-  0 e. _V
25 vex 
 |-  y e. _V
26 24 25 op1std 
 |-  ( X = <. 0 , y >. -> ( 1st ` X ) = 0 )
27 26 eqeq1d 
 |-  ( X = <. 0 , y >. -> ( ( 1st ` X ) = 1 <-> 0 = 1 ) )
28 eqcom 
 |-  ( 0 = 1 <-> 1 = 0 )
29 27 28 bitrdi 
 |-  ( X = <. 0 , y >. -> ( ( 1st ` X ) = 1 <-> 1 = 0 ) )
30 ax-1ne0 
 |-  1 =/= 0
31 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( Y = <. 0 , ( ( y + 1 ) mod N ) >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
32 31 com12 
 |-  ( 1 =/= 0 -> ( 1 = 0 -> ( Y = <. 0 , ( ( y + 1 ) mod N ) >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
33 30 32 mp1i 
 |-  ( X = <. 0 , y >. -> ( 1 = 0 -> ( Y = <. 0 , ( ( y + 1 ) mod N ) >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
34 29 33 sylbid 
 |-  ( X = <. 0 , y >. -> ( ( 1st ` X ) = 1 -> ( Y = <. 0 , ( ( y + 1 ) mod N ) >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
35 34 com12 
 |-  ( ( 1st ` X ) = 1 -> ( X = <. 0 , y >. -> ( Y = <. 0 , ( ( y + 1 ) mod N ) >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
36 35 impd 
 |-  ( ( 1st ` X ) = 1 -> ( ( X = <. 0 , y >. /\ Y = <. 0 , ( ( y + 1 ) mod N ) >. ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
37 ovex 
 |-  ( ( y + 1 ) mod N ) e. _V
38 24 37 op1std 
 |-  ( X = <. 0 , ( ( y + 1 ) mod N ) >. -> ( 1st ` X ) = 0 )
39 38 eqeq1d 
 |-  ( X = <. 0 , ( ( y + 1 ) mod N ) >. -> ( ( 1st ` X ) = 1 <-> 0 = 1 ) )
40 39 28 bitrdi 
 |-  ( X = <. 0 , ( ( y + 1 ) mod N ) >. -> ( ( 1st ` X ) = 1 <-> 1 = 0 ) )
41 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( Y = <. 0 , y >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
42 41 com12 
 |-  ( 1 =/= 0 -> ( 1 = 0 -> ( Y = <. 0 , y >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
43 30 42 mp1i 
 |-  ( X = <. 0 , ( ( y + 1 ) mod N ) >. -> ( 1 = 0 -> ( Y = <. 0 , y >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
44 40 43 sylbid 
 |-  ( X = <. 0 , ( ( y + 1 ) mod N ) >. -> ( ( 1st ` X ) = 1 -> ( Y = <. 0 , y >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
45 44 com12 
 |-  ( ( 1st ` X ) = 1 -> ( X = <. 0 , ( ( y + 1 ) mod N ) >. -> ( Y = <. 0 , y >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
46 45 impd 
 |-  ( ( 1st ` X ) = 1 -> ( ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
47 36 46 jaod 
 |-  ( ( 1st ` X ) = 1 -> ( ( ( X = <. 0 , y >. /\ Y = <. 0 , ( ( y + 1 ) mod N ) >. ) \/ ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
48 47 3ad2ant2 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) -> ( ( ( X = <. 0 , y >. /\ Y = <. 0 , ( ( y + 1 ) mod N ) >. ) \/ ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
49 48 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( X = <. 0 , y >. /\ Y = <. 0 , ( ( y + 1 ) mod N ) >. ) \/ ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
50 23 49 sylbid 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( { X , Y } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
51 opex 
 |-  <. 1 , y >. e. _V
52 19 51 pm3.2i 
 |-  ( <. 0 , y >. e. _V /\ <. 1 , y >. e. _V )
53 preq12bg 
 |-  ( ( ( X e. V /\ Y e. V ) /\ ( <. 0 , y >. e. _V /\ <. 1 , y >. e. _V ) ) -> ( { X , Y } = { <. 0 , y >. , <. 1 , y >. } <-> ( ( X = <. 0 , y >. /\ Y = <. 1 , y >. ) \/ ( X = <. 1 , y >. /\ Y = <. 0 , y >. ) ) ) )
54 18 52 53 sylancl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( { X , Y } = { <. 0 , y >. , <. 1 , y >. } <-> ( ( X = <. 0 , y >. /\ Y = <. 1 , y >. ) \/ ( X = <. 1 , y >. /\ Y = <. 0 , y >. ) ) ) )
55 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( Y = <. 1 , y >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
56 55 com12 
 |-  ( 1 =/= 0 -> ( 1 = 0 -> ( Y = <. 1 , y >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
57 30 56 mp1i 
 |-  ( X = <. 0 , y >. -> ( 1 = 0 -> ( Y = <. 1 , y >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
58 29 57 sylbid 
 |-  ( X = <. 0 , y >. -> ( ( 1st ` X ) = 1 -> ( Y = <. 1 , y >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
59 58 com12 
 |-  ( ( 1st ` X ) = 1 -> ( X = <. 0 , y >. -> ( Y = <. 1 , y >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
60 59 3ad2ant2 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) -> ( X = <. 0 , y >. -> ( Y = <. 1 , y >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
61 60 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( X = <. 0 , y >. -> ( Y = <. 1 , y >. -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) )
62 61 impd 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( X = <. 0 , y >. /\ Y = <. 1 , y >. ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
63 simpr 
 |-  ( ( X = <. 1 , y >. /\ Y = <. 0 , y >. ) -> Y = <. 0 , y >. )
64 1ex 
 |-  1 e. _V
65 64 25 op2ndd 
 |-  ( X = <. 1 , y >. -> ( 2nd ` X ) = y )
66 65 eqcomd 
 |-  ( X = <. 1 , y >. -> y = ( 2nd ` X ) )
67 66 adantr 
 |-  ( ( X = <. 1 , y >. /\ Y = <. 0 , y >. ) -> y = ( 2nd ` X ) )
68 67 opeq2d 
 |-  ( ( X = <. 1 , y >. /\ Y = <. 0 , y >. ) -> <. 0 , y >. = <. 0 , ( 2nd ` X ) >. )
69 63 68 eqtrd 
 |-  ( ( X = <. 1 , y >. /\ Y = <. 0 , y >. ) -> Y = <. 0 , ( 2nd ` X ) >. )
70 69 adantl 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 1 , y >. /\ Y = <. 0 , y >. ) ) -> Y = <. 0 , ( 2nd ` X ) >. )
71 70 3mix2d 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 1 , y >. /\ Y = <. 0 , y >. ) ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) )
72 71 ex 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( X = <. 1 , y >. /\ Y = <. 0 , y >. ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
73 62 72 jaod 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( X = <. 0 , y >. /\ Y = <. 1 , y >. ) \/ ( X = <. 1 , y >. /\ Y = <. 0 , y >. ) ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
74 54 73 sylbid 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( { X , Y } = { <. 0 , y >. , <. 1 , y >. } -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
75 opex 
 |-  <. 1 , ( ( y + K ) mod N ) >. e. _V
76 51 75 pm3.2i 
 |-  ( <. 1 , y >. e. _V /\ <. 1 , ( ( y + K ) mod N ) >. e. _V )
77 preq12bg 
 |-  ( ( ( X e. V /\ Y e. V ) /\ ( <. 1 , y >. e. _V /\ <. 1 , ( ( y + K ) mod N ) >. e. _V ) ) -> ( { X , Y } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } <-> ( ( X = <. 1 , y >. /\ Y = <. 1 , ( ( y + K ) mod N ) >. ) \/ ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) ) ) )
78 18 76 77 sylancl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( { X , Y } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } <-> ( ( X = <. 1 , y >. /\ Y = <. 1 , ( ( y + K ) mod N ) >. ) \/ ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) ) ) )
79 simpr 
 |-  ( ( X = <. 1 , y >. /\ Y = <. 1 , ( ( y + K ) mod N ) >. ) -> Y = <. 1 , ( ( y + K ) mod N ) >. )
80 66 oveq1d 
 |-  ( X = <. 1 , y >. -> ( y + K ) = ( ( 2nd ` X ) + K ) )
81 80 oveq1d 
 |-  ( X = <. 1 , y >. -> ( ( y + K ) mod N ) = ( ( ( 2nd ` X ) + K ) mod N ) )
82 81 adantr 
 |-  ( ( X = <. 1 , y >. /\ Y = <. 1 , ( ( y + K ) mod N ) >. ) -> ( ( y + K ) mod N ) = ( ( ( 2nd ` X ) + K ) mod N ) )
83 82 opeq2d 
 |-  ( ( X = <. 1 , y >. /\ Y = <. 1 , ( ( y + K ) mod N ) >. ) -> <. 1 , ( ( y + K ) mod N ) >. = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. )
84 79 83 eqtrd 
 |-  ( ( X = <. 1 , y >. /\ Y = <. 1 , ( ( y + K ) mod N ) >. ) -> Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. )
85 84 3mix1d 
 |-  ( ( X = <. 1 , y >. /\ Y = <. 1 , ( ( y + K ) mod N ) >. ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) )
86 85 a1i 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( X = <. 1 , y >. /\ Y = <. 1 , ( ( y + K ) mod N ) >. ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
87 elfzoelz 
 |-  ( y e. ( 0 ..^ N ) -> y e. ZZ )
88 87 zred 
 |-  ( y e. ( 0 ..^ N ) -> y e. RR )
89 88 adantl 
 |-  ( ( K e. J /\ y e. ( 0 ..^ N ) ) -> y e. RR )
90 elfzoelz 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. ZZ )
91 90 zred 
 |-  ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. RR )
92 6 91 sylbi 
 |-  ( K e. J -> K e. RR )
93 92 adantr 
 |-  ( ( K e. J /\ y e. ( 0 ..^ N ) ) -> K e. RR )
94 89 93 readdcld 
 |-  ( ( K e. J /\ y e. ( 0 ..^ N ) ) -> ( y + K ) e. RR )
95 elfzo0 
 |-  ( y e. ( 0 ..^ N ) <-> ( y e. NN0 /\ N e. NN /\ y < N ) )
96 nnrp 
 |-  ( N e. NN -> N e. RR+ )
97 96 3ad2ant2 
 |-  ( ( y e. NN0 /\ N e. NN /\ y < N ) -> N e. RR+ )
98 95 97 sylbi 
 |-  ( y e. ( 0 ..^ N ) -> N e. RR+ )
99 98 adantl 
 |-  ( ( K e. J /\ y e. ( 0 ..^ N ) ) -> N e. RR+ )
100 modsubmod 
 |-  ( ( ( y + K ) e. RR /\ K e. RR /\ N e. RR+ ) -> ( ( ( ( y + K ) mod N ) - K ) mod N ) = ( ( ( y + K ) - K ) mod N ) )
101 94 93 99 100 syl3anc 
 |-  ( ( K e. J /\ y e. ( 0 ..^ N ) ) -> ( ( ( ( y + K ) mod N ) - K ) mod N ) = ( ( ( y + K ) - K ) mod N ) )
102 87 zcnd 
 |-  ( y e. ( 0 ..^ N ) -> y e. CC )
103 102 adantl 
 |-  ( ( K e. J /\ y e. ( 0 ..^ N ) ) -> y e. CC )
104 93 recnd 
 |-  ( ( K e. J /\ y e. ( 0 ..^ N ) ) -> K e. CC )
105 103 104 pncand 
 |-  ( ( K e. J /\ y e. ( 0 ..^ N ) ) -> ( ( y + K ) - K ) = y )
106 105 oveq1d 
 |-  ( ( K e. J /\ y e. ( 0 ..^ N ) ) -> ( ( ( y + K ) - K ) mod N ) = ( y mod N ) )
107 zmodidfzoimp 
 |-  ( y e. ( 0 ..^ N ) -> ( y mod N ) = y )
108 107 adantl 
 |-  ( ( K e. J /\ y e. ( 0 ..^ N ) ) -> ( y mod N ) = y )
109 101 106 108 3eqtrrd 
 |-  ( ( K e. J /\ y e. ( 0 ..^ N ) ) -> y = ( ( ( ( y + K ) mod N ) - K ) mod N ) )
110 109 ex 
 |-  ( K e. J -> ( y e. ( 0 ..^ N ) -> y = ( ( ( ( y + K ) mod N ) - K ) mod N ) ) )
111 110 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( y e. ( 0 ..^ N ) -> y = ( ( ( ( y + K ) mod N ) - K ) mod N ) ) )
112 111 3ad2ant1 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) -> ( y e. ( 0 ..^ N ) -> y = ( ( ( ( y + K ) mod N ) - K ) mod N ) ) )
113 112 imp 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> y = ( ( ( ( y + K ) mod N ) - K ) mod N ) )
114 113 adantr 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) ) -> y = ( ( ( ( y + K ) mod N ) - K ) mod N ) )
115 114 opeq2d 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) ) -> <. 1 , y >. = <. 1 , ( ( ( ( y + K ) mod N ) - K ) mod N ) >. )
116 simpr 
 |-  ( ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) -> Y = <. 1 , y >. )
117 ovex 
 |-  ( ( y + K ) mod N ) e. _V
118 64 117 op2ndd 
 |-  ( X = <. 1 , ( ( y + K ) mod N ) >. -> ( 2nd ` X ) = ( ( y + K ) mod N ) )
119 118 oveq1d 
 |-  ( X = <. 1 , ( ( y + K ) mod N ) >. -> ( ( 2nd ` X ) - K ) = ( ( ( y + K ) mod N ) - K ) )
120 119 oveq1d 
 |-  ( X = <. 1 , ( ( y + K ) mod N ) >. -> ( ( ( 2nd ` X ) - K ) mod N ) = ( ( ( ( y + K ) mod N ) - K ) mod N ) )
121 120 opeq2d 
 |-  ( X = <. 1 , ( ( y + K ) mod N ) >. -> <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. = <. 1 , ( ( ( ( y + K ) mod N ) - K ) mod N ) >. )
122 121 adantr 
 |-  ( ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) -> <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. = <. 1 , ( ( ( ( y + K ) mod N ) - K ) mod N ) >. )
123 116 122 eqeq12d 
 |-  ( ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. <-> <. 1 , y >. = <. 1 , ( ( ( ( y + K ) mod N ) - K ) mod N ) >. ) )
124 123 adantl 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. <-> <. 1 , y >. = <. 1 , ( ( ( ( y + K ) mod N ) - K ) mod N ) >. ) )
125 115 124 mpbird 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) ) -> Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. )
126 125 3mix3d 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) )
127 126 ex 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
128 86 127 jaod 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( X = <. 1 , y >. /\ Y = <. 1 , ( ( y + K ) mod N ) >. ) \/ ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
129 78 128 sylbid 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( { X , Y } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
130 50 74 129 3jaod 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( { X , Y } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { X , Y } = { <. 0 , y >. , <. 1 , y >. } \/ { X , Y } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
131 130 rexlimdva 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) -> ( E. y e. ( 0 ..^ N ) ( { X , Y } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } \/ { X , Y } = { <. 0 , y >. , <. 1 , y >. } \/ { X , Y } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
132 16 131 sylbid 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ ( X e. V /\ Y e. V ) ) -> ( { X , Y } e. E -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
133 132 3exp 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( ( 1st ` X ) = 1 -> ( ( X e. V /\ Y e. V ) -> ( { X , Y } e. E -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) ) )
134 133 com34 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( ( 1st ` X ) = 1 -> ( { X , Y } e. E -> ( ( X e. V /\ Y e. V ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) ) ) )
135 134 3imp 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ { X , Y } e. E ) -> ( ( X e. V /\ Y e. V ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) ) )
136 13 135 mpd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 1 /\ { X , Y } e. E ) -> ( Y = <. 1 , ( ( ( 2nd ` X ) + K ) mod N ) >. \/ Y = <. 0 , ( 2nd ` X ) >. \/ Y = <. 1 , ( ( ( 2nd ` X ) - K ) mod N ) >. ) )