Step |
Hyp |
Ref |
Expression |
1 |
|
lgsdir2lem2.1 |
|- ( K e. ZZ /\ 2 || ( K + 1 ) /\ ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... K ) -> ( A mod 8 ) e. S ) ) ) |
2 |
|
lgsdir2lem2.2 |
|- M = ( K + 1 ) |
3 |
|
lgsdir2lem2.3 |
|- N = ( M + 1 ) |
4 |
|
lgsdir2lem2.4 |
|- N e. S |
5 |
1
|
simp1i |
|- K e. ZZ |
6 |
|
peano2z |
|- ( K e. ZZ -> ( K + 1 ) e. ZZ ) |
7 |
5 6
|
ax-mp |
|- ( K + 1 ) e. ZZ |
8 |
2 7
|
eqeltri |
|- M e. ZZ |
9 |
|
peano2z |
|- ( M e. ZZ -> ( M + 1 ) e. ZZ ) |
10 |
8 9
|
ax-mp |
|- ( M + 1 ) e. ZZ |
11 |
3 10
|
eqeltri |
|- N e. ZZ |
12 |
1
|
simp2i |
|- 2 || ( K + 1 ) |
13 |
|
2z |
|- 2 e. ZZ |
14 |
|
dvdsadd |
|- ( ( 2 e. ZZ /\ ( K + 1 ) e. ZZ ) -> ( 2 || ( K + 1 ) <-> 2 || ( 2 + ( K + 1 ) ) ) ) |
15 |
13 7 14
|
mp2an |
|- ( 2 || ( K + 1 ) <-> 2 || ( 2 + ( K + 1 ) ) ) |
16 |
12 15
|
mpbi |
|- 2 || ( 2 + ( K + 1 ) ) |
17 |
|
zcn |
|- ( K e. ZZ -> K e. CC ) |
18 |
5 17
|
ax-mp |
|- K e. CC |
19 |
|
ax-1cn |
|- 1 e. CC |
20 |
18 19
|
addcomi |
|- ( K + 1 ) = ( 1 + K ) |
21 |
2 20
|
eqtri |
|- M = ( 1 + K ) |
22 |
21
|
oveq1i |
|- ( M + 1 ) = ( ( 1 + K ) + 1 ) |
23 |
3 22
|
eqtri |
|- N = ( ( 1 + K ) + 1 ) |
24 |
|
df-2 |
|- 2 = ( 1 + 1 ) |
25 |
24
|
oveq1i |
|- ( 2 + K ) = ( ( 1 + 1 ) + K ) |
26 |
19 18 19
|
add32i |
|- ( ( 1 + K ) + 1 ) = ( ( 1 + 1 ) + K ) |
27 |
25 26
|
eqtr4i |
|- ( 2 + K ) = ( ( 1 + K ) + 1 ) |
28 |
23 27
|
eqtr4i |
|- N = ( 2 + K ) |
29 |
28
|
oveq1i |
|- ( N + 1 ) = ( ( 2 + K ) + 1 ) |
30 |
|
2cn |
|- 2 e. CC |
31 |
30 18 19
|
addassi |
|- ( ( 2 + K ) + 1 ) = ( 2 + ( K + 1 ) ) |
32 |
29 31
|
eqtri |
|- ( N + 1 ) = ( 2 + ( K + 1 ) ) |
33 |
16 32
|
breqtrri |
|- 2 || ( N + 1 ) |
34 |
|
elfzuz2 |
|- ( ( A mod 8 ) e. ( 0 ... N ) -> N e. ( ZZ>= ` 0 ) ) |
35 |
|
fzm1 |
|- ( N e. ( ZZ>= ` 0 ) -> ( ( A mod 8 ) e. ( 0 ... N ) <-> ( ( A mod 8 ) e. ( 0 ... ( N - 1 ) ) \/ ( A mod 8 ) = N ) ) ) |
36 |
34 35
|
syl |
|- ( ( A mod 8 ) e. ( 0 ... N ) -> ( ( A mod 8 ) e. ( 0 ... N ) <-> ( ( A mod 8 ) e. ( 0 ... ( N - 1 ) ) \/ ( A mod 8 ) = N ) ) ) |
37 |
36
|
ibi |
|- ( ( A mod 8 ) e. ( 0 ... N ) -> ( ( A mod 8 ) e. ( 0 ... ( N - 1 ) ) \/ ( A mod 8 ) = N ) ) |
38 |
|
elfzuz2 |
|- ( ( A mod 8 ) e. ( 0 ... M ) -> M e. ( ZZ>= ` 0 ) ) |
39 |
|
fzm1 |
|- ( M e. ( ZZ>= ` 0 ) -> ( ( A mod 8 ) e. ( 0 ... M ) <-> ( ( A mod 8 ) e. ( 0 ... ( M - 1 ) ) \/ ( A mod 8 ) = M ) ) ) |
40 |
38 39
|
syl |
|- ( ( A mod 8 ) e. ( 0 ... M ) -> ( ( A mod 8 ) e. ( 0 ... M ) <-> ( ( A mod 8 ) e. ( 0 ... ( M - 1 ) ) \/ ( A mod 8 ) = M ) ) ) |
41 |
40
|
ibi |
|- ( ( A mod 8 ) e. ( 0 ... M ) -> ( ( A mod 8 ) e. ( 0 ... ( M - 1 ) ) \/ ( A mod 8 ) = M ) ) |
42 |
|
zcn |
|- ( M e. ZZ -> M e. CC ) |
43 |
8 42
|
ax-mp |
|- M e. CC |
44 |
43 19 3
|
mvrraddi |
|- ( N - 1 ) = M |
45 |
44
|
oveq2i |
|- ( 0 ... ( N - 1 ) ) = ( 0 ... M ) |
46 |
41 45
|
eleq2s |
|- ( ( A mod 8 ) e. ( 0 ... ( N - 1 ) ) -> ( ( A mod 8 ) e. ( 0 ... ( M - 1 ) ) \/ ( A mod 8 ) = M ) ) |
47 |
18 19 2
|
mvrraddi |
|- ( M - 1 ) = K |
48 |
47
|
oveq2i |
|- ( 0 ... ( M - 1 ) ) = ( 0 ... K ) |
49 |
48
|
eleq2i |
|- ( ( A mod 8 ) e. ( 0 ... ( M - 1 ) ) <-> ( A mod 8 ) e. ( 0 ... K ) ) |
50 |
1
|
simp3i |
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... K ) -> ( A mod 8 ) e. S ) ) |
51 |
49 50
|
syl5bi |
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... ( M - 1 ) ) -> ( A mod 8 ) e. S ) ) |
52 |
|
2nn |
|- 2 e. NN |
53 |
|
8nn |
|- 8 e. NN |
54 |
|
4z |
|- 4 e. ZZ |
55 |
|
dvdsmul2 |
|- ( ( 4 e. ZZ /\ 2 e. ZZ ) -> 2 || ( 4 x. 2 ) ) |
56 |
54 13 55
|
mp2an |
|- 2 || ( 4 x. 2 ) |
57 |
|
4t2e8 |
|- ( 4 x. 2 ) = 8 |
58 |
56 57
|
breqtri |
|- 2 || 8 |
59 |
|
dvdsmod |
|- ( ( ( 2 e. NN /\ 8 e. NN /\ A e. ZZ ) /\ 2 || 8 ) -> ( 2 || ( A mod 8 ) <-> 2 || A ) ) |
60 |
58 59
|
mpan2 |
|- ( ( 2 e. NN /\ 8 e. NN /\ A e. ZZ ) -> ( 2 || ( A mod 8 ) <-> 2 || A ) ) |
61 |
52 53 60
|
mp3an12 |
|- ( A e. ZZ -> ( 2 || ( A mod 8 ) <-> 2 || A ) ) |
62 |
61
|
notbid |
|- ( A e. ZZ -> ( -. 2 || ( A mod 8 ) <-> -. 2 || A ) ) |
63 |
62
|
biimpar |
|- ( ( A e. ZZ /\ -. 2 || A ) -> -. 2 || ( A mod 8 ) ) |
64 |
12 2
|
breqtrri |
|- 2 || M |
65 |
|
id |
|- ( ( A mod 8 ) = M -> ( A mod 8 ) = M ) |
66 |
64 65
|
breqtrrid |
|- ( ( A mod 8 ) = M -> 2 || ( A mod 8 ) ) |
67 |
63 66
|
nsyl |
|- ( ( A e. ZZ /\ -. 2 || A ) -> -. ( A mod 8 ) = M ) |
68 |
67
|
pm2.21d |
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) = M -> ( A mod 8 ) e. S ) ) |
69 |
51 68
|
jaod |
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( ( ( A mod 8 ) e. ( 0 ... ( M - 1 ) ) \/ ( A mod 8 ) = M ) -> ( A mod 8 ) e. S ) ) |
70 |
46 69
|
syl5 |
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... ( N - 1 ) ) -> ( A mod 8 ) e. S ) ) |
71 |
|
eleq1 |
|- ( ( A mod 8 ) = N -> ( ( A mod 8 ) e. S <-> N e. S ) ) |
72 |
4 71
|
mpbiri |
|- ( ( A mod 8 ) = N -> ( A mod 8 ) e. S ) |
73 |
72
|
a1i |
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) = N -> ( A mod 8 ) e. S ) ) |
74 |
70 73
|
jaod |
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( ( ( A mod 8 ) e. ( 0 ... ( N - 1 ) ) \/ ( A mod 8 ) = N ) -> ( A mod 8 ) e. S ) ) |
75 |
37 74
|
syl5 |
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... N ) -> ( A mod 8 ) e. S ) ) |
76 |
11 33 75
|
3pm3.2i |
|- ( N e. ZZ /\ 2 || ( N + 1 ) /\ ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... N ) -> ( A mod 8 ) e. S ) ) ) |