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 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgedgvtx0.g 
|- G = ( N gPetersenGr K )
gpgedgvtx0.v 
|- V = ( Vtx ` G )
gpgedgvtx0.e 
|- E = ( Edg ` G )
Assertion gpgvtxedg0 
|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ { X , Y } e. E ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) 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 ) = 0 /\ { X , Y } e. E ) -> G e. USGraph )
11 simp3 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ { 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 ) = 0 /\ { 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 ) = 0 /\ ( 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 ) = 0 /\ ( X e. V /\ Y e. V ) ) -> ( X e. V /\ Y e. V ) )
18 17 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( 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 ) = 0 /\ ( 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 simpr 
 |-  ( ( X = <. 0 , y >. /\ Y = <. 0 , ( ( y + 1 ) mod N ) >. ) -> Y = <. 0 , ( ( y + 1 ) mod N ) >. )
25 c0ex 
 |-  0 e. _V
26 vex 
 |-  y e. _V
27 25 26 op2ndd 
 |-  ( X = <. 0 , y >. -> ( 2nd ` X ) = y )
28 27 eqcomd 
 |-  ( X = <. 0 , y >. -> y = ( 2nd ` X ) )
29 28 oveq1d 
 |-  ( X = <. 0 , y >. -> ( y + 1 ) = ( ( 2nd ` X ) + 1 ) )
30 29 oveq1d 
 |-  ( X = <. 0 , y >. -> ( ( y + 1 ) mod N ) = ( ( ( 2nd ` X ) + 1 ) mod N ) )
31 30 adantr 
 |-  ( ( X = <. 0 , y >. /\ Y = <. 0 , ( ( y + 1 ) mod N ) >. ) -> ( ( y + 1 ) mod N ) = ( ( ( 2nd ` X ) + 1 ) mod N ) )
32 31 opeq2d 
 |-  ( ( X = <. 0 , y >. /\ Y = <. 0 , ( ( y + 1 ) mod N ) >. ) -> <. 0 , ( ( y + 1 ) mod N ) >. = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. )
33 24 32 eqtrd 
 |-  ( ( X = <. 0 , y >. /\ Y = <. 0 , ( ( y + 1 ) mod N ) >. ) -> Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. )
34 33 3mix1d 
 |-  ( ( X = <. 0 , y >. /\ Y = <. 0 , ( ( y + 1 ) mod N ) >. ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) )
35 34 a1i 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( X = <. 0 , y >. /\ Y = <. 0 , ( ( y + 1 ) mod N ) >. ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
36 elfzoelz 
 |-  ( y e. ( 0 ..^ N ) -> y e. ZZ )
37 36 zred 
 |-  ( y e. ( 0 ..^ N ) -> y e. RR )
38 1red 
 |-  ( y e. ( 0 ..^ N ) -> 1 e. RR )
39 37 38 readdcld 
 |-  ( y e. ( 0 ..^ N ) -> ( y + 1 ) e. RR )
40 elfzo0 
 |-  ( y e. ( 0 ..^ N ) <-> ( y e. NN0 /\ N e. NN /\ y < N ) )
41 nnrp 
 |-  ( N e. NN -> N e. RR+ )
42 41 3ad2ant2 
 |-  ( ( y e. NN0 /\ N e. NN /\ y < N ) -> N e. RR+ )
43 40 42 sylbi 
 |-  ( y e. ( 0 ..^ N ) -> N e. RR+ )
44 modsubmod 
 |-  ( ( ( y + 1 ) e. RR /\ 1 e. RR /\ N e. RR+ ) -> ( ( ( ( y + 1 ) mod N ) - 1 ) mod N ) = ( ( ( y + 1 ) - 1 ) mod N ) )
45 39 38 43 44 syl3anc 
 |-  ( y e. ( 0 ..^ N ) -> ( ( ( ( y + 1 ) mod N ) - 1 ) mod N ) = ( ( ( y + 1 ) - 1 ) mod N ) )
46 36 zcnd 
 |-  ( y e. ( 0 ..^ N ) -> y e. CC )
47 pncan1 
 |-  ( y e. CC -> ( ( y + 1 ) - 1 ) = y )
48 46 47 syl 
 |-  ( y e. ( 0 ..^ N ) -> ( ( y + 1 ) - 1 ) = y )
49 48 oveq1d 
 |-  ( y e. ( 0 ..^ N ) -> ( ( ( y + 1 ) - 1 ) mod N ) = ( y mod N ) )
50 zmodidfzoimp 
 |-  ( y e. ( 0 ..^ N ) -> ( y mod N ) = y )
51 45 49 50 3eqtrrd 
 |-  ( y e. ( 0 ..^ N ) -> y = ( ( ( ( y + 1 ) mod N ) - 1 ) mod N ) )
52 51 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> y = ( ( ( ( y + 1 ) mod N ) - 1 ) mod N ) )
53 52 adantr 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) ) -> y = ( ( ( ( y + 1 ) mod N ) - 1 ) mod N ) )
54 53 opeq2d 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) ) -> <. 0 , y >. = <. 0 , ( ( ( ( y + 1 ) mod N ) - 1 ) mod N ) >. )
55 simpr 
 |-  ( ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) -> Y = <. 0 , y >. )
56 ovex 
 |-  ( ( y + 1 ) mod N ) e. _V
57 25 56 op2ndd 
 |-  ( X = <. 0 , ( ( y + 1 ) mod N ) >. -> ( 2nd ` X ) = ( ( y + 1 ) mod N ) )
58 57 oveq1d 
 |-  ( X = <. 0 , ( ( y + 1 ) mod N ) >. -> ( ( 2nd ` X ) - 1 ) = ( ( ( y + 1 ) mod N ) - 1 ) )
59 58 oveq1d 
 |-  ( X = <. 0 , ( ( y + 1 ) mod N ) >. -> ( ( ( 2nd ` X ) - 1 ) mod N ) = ( ( ( ( y + 1 ) mod N ) - 1 ) mod N ) )
60 59 opeq2d 
 |-  ( X = <. 0 , ( ( y + 1 ) mod N ) >. -> <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. = <. 0 , ( ( ( ( y + 1 ) mod N ) - 1 ) mod N ) >. )
61 60 adantr 
 |-  ( ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) -> <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. = <. 0 , ( ( ( ( y + 1 ) mod N ) - 1 ) mod N ) >. )
62 55 61 eqeq12d 
 |-  ( ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. <-> <. 0 , y >. = <. 0 , ( ( ( ( y + 1 ) mod N ) - 1 ) mod N ) >. ) )
63 62 adantl 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. <-> <. 0 , y >. = <. 0 , ( ( ( ( y + 1 ) mod N ) - 1 ) mod N ) >. ) )
64 54 63 mpbird 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) ) -> Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. )
65 64 3mix3d 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) )
66 65 ex 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( X = <. 0 , ( ( y + 1 ) mod N ) >. /\ Y = <. 0 , y >. ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
67 35 66 jaod 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( 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 = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
68 23 67 sylbid 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( { X , Y } = { <. 0 , y >. , <. 0 , ( ( y + 1 ) mod N ) >. } -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
69 opex 
 |-  <. 1 , y >. e. _V
70 19 69 pm3.2i 
 |-  ( <. 0 , y >. e. _V /\ <. 1 , y >. e. _V )
71 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 >. ) ) ) )
72 18 70 71 sylancl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( 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 >. ) ) ) )
73 simpr 
 |-  ( ( X = <. 0 , y >. /\ Y = <. 1 , y >. ) -> Y = <. 1 , y >. )
74 28 adantr 
 |-  ( ( X = <. 0 , y >. /\ Y = <. 1 , y >. ) -> y = ( 2nd ` X ) )
75 74 opeq2d 
 |-  ( ( X = <. 0 , y >. /\ Y = <. 1 , y >. ) -> <. 1 , y >. = <. 1 , ( 2nd ` X ) >. )
76 73 75 eqtrd 
 |-  ( ( X = <. 0 , y >. /\ Y = <. 1 , y >. ) -> Y = <. 1 , ( 2nd ` X ) >. )
77 76 adantl 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 0 , y >. /\ Y = <. 1 , y >. ) ) -> Y = <. 1 , ( 2nd ` X ) >. )
78 77 3mix2d 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) /\ ( X = <. 0 , y >. /\ Y = <. 1 , y >. ) ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) )
79 78 ex 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( X = <. 0 , y >. /\ Y = <. 1 , y >. ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
80 1ex 
 |-  1 e. _V
81 80 26 op1std 
 |-  ( X = <. 1 , y >. -> ( 1st ` X ) = 1 )
82 81 eqeq1d 
 |-  ( X = <. 1 , y >. -> ( ( 1st ` X ) = 0 <-> 1 = 0 ) )
83 ax-1ne0 
 |-  1 =/= 0
84 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( Y = <. 0 , y >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
85 84 com12 
 |-  ( 1 =/= 0 -> ( 1 = 0 -> ( Y = <. 0 , y >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
86 83 85 mp1i 
 |-  ( X = <. 1 , y >. -> ( 1 = 0 -> ( Y = <. 0 , y >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
87 82 86 sylbid 
 |-  ( X = <. 1 , y >. -> ( ( 1st ` X ) = 0 -> ( Y = <. 0 , y >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
88 87 com12 
 |-  ( ( 1st ` X ) = 0 -> ( X = <. 1 , y >. -> ( Y = <. 0 , y >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
89 88 3ad2ant2 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) -> ( X = <. 1 , y >. -> ( Y = <. 0 , y >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
90 89 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( X = <. 1 , y >. -> ( Y = <. 0 , y >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
91 90 impd 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( X = <. 1 , y >. /\ Y = <. 0 , y >. ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
92 79 91 jaod 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( ( ( X = <. 0 , y >. /\ Y = <. 1 , y >. ) \/ ( X = <. 1 , y >. /\ Y = <. 0 , y >. ) ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
93 72 92 sylbid 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( { X , Y } = { <. 0 , y >. , <. 1 , y >. } -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
94 opex 
 |-  <. 1 , ( ( y + K ) mod N ) >. e. _V
95 69 94 pm3.2i 
 |-  ( <. 1 , y >. e. _V /\ <. 1 , ( ( y + K ) mod N ) >. e. _V )
96 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 >. ) ) ) )
97 18 95 96 sylancl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( 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 >. ) ) ) )
98 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( Y = <. 1 , ( ( y + K ) mod N ) >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
99 98 com12 
 |-  ( 1 =/= 0 -> ( 1 = 0 -> ( Y = <. 1 , ( ( y + K ) mod N ) >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
100 83 99 mp1i 
 |-  ( X = <. 1 , y >. -> ( 1 = 0 -> ( Y = <. 1 , ( ( y + K ) mod N ) >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
101 82 100 sylbid 
 |-  ( X = <. 1 , y >. -> ( ( 1st ` X ) = 0 -> ( Y = <. 1 , ( ( y + K ) mod N ) >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
102 101 com12 
 |-  ( ( 1st ` X ) = 0 -> ( X = <. 1 , y >. -> ( Y = <. 1 , ( ( y + K ) mod N ) >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
103 102 impd 
 |-  ( ( 1st ` X ) = 0 -> ( ( X = <. 1 , y >. /\ Y = <. 1 , ( ( y + K ) mod N ) >. ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
104 ovex 
 |-  ( ( y + K ) mod N ) e. _V
105 80 104 op1std 
 |-  ( X = <. 1 , ( ( y + K ) mod N ) >. -> ( 1st ` X ) = 1 )
106 105 eqeq1d 
 |-  ( X = <. 1 , ( ( y + K ) mod N ) >. -> ( ( 1st ` X ) = 0 <-> 1 = 0 ) )
107 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( Y = <. 1 , y >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
108 107 com12 
 |-  ( 1 =/= 0 -> ( 1 = 0 -> ( Y = <. 1 , y >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
109 83 108 mp1i 
 |-  ( X = <. 1 , ( ( y + K ) mod N ) >. -> ( 1 = 0 -> ( Y = <. 1 , y >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
110 106 109 sylbid 
 |-  ( X = <. 1 , ( ( y + K ) mod N ) >. -> ( ( 1st ` X ) = 0 -> ( Y = <. 1 , y >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
111 110 com12 
 |-  ( ( 1st ` X ) = 0 -> ( X = <. 1 , ( ( y + K ) mod N ) >. -> ( Y = <. 1 , y >. -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) )
112 111 impd 
 |-  ( ( 1st ` X ) = 0 -> ( ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
113 103 112 jaod 
 |-  ( ( 1st ` X ) = 0 -> ( ( ( X = <. 1 , y >. /\ Y = <. 1 , ( ( y + K ) mod N ) >. ) \/ ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
114 113 3ad2ant2 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) -> ( ( ( X = <. 1 , y >. /\ Y = <. 1 , ( ( y + K ) mod N ) >. ) \/ ( X = <. 1 , ( ( y + K ) mod N ) >. /\ Y = <. 1 , y >. ) ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
115 114 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( 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 = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
116 97 115 sylbid 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) /\ y e. ( 0 ..^ N ) ) -> ( { X , Y } = { <. 1 , y >. , <. 1 , ( ( y + K ) mod N ) >. } -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
117 68 93 116 3jaod 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( 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 = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
118 117 rexlimdva 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( 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 = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
119 16 118 sylbid 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ ( X e. V /\ Y e. V ) ) -> ( { X , Y } e. E -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
120 119 3exp 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( ( 1st ` X ) = 0 -> ( ( X e. V /\ Y e. V ) -> ( { X , Y } e. E -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) ) )
121 120 com34 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( ( 1st ` X ) = 0 -> ( { X , Y } e. E -> ( ( X e. V /\ Y e. V ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) ) ) )
122 121 3imp 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ { X , Y } e. E ) -> ( ( X e. V /\ Y e. V ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) ) )
123 13 122 mpd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` X ) = 0 /\ { X , Y } e. E ) -> ( Y = <. 0 , ( ( ( 2nd ` X ) + 1 ) mod N ) >. \/ Y = <. 1 , ( 2nd ` X ) >. \/ Y = <. 0 , ( ( ( 2nd ` X ) - 1 ) mod N ) >. ) )