Metamath Proof Explorer


Theorem lgsdir2lem2

Description: Lemma for lgsdir2 . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypotheses lgsdir2lem2.1
|- ( K e. ZZ /\ 2 || ( K + 1 ) /\ ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... K ) -> ( A mod 8 ) e. S ) ) )
lgsdir2lem2.2
|- M = ( K + 1 )
lgsdir2lem2.3
|- N = ( M + 1 )
lgsdir2lem2.4
|- N e. S
Assertion lgsdir2lem2
|- ( N e. ZZ /\ 2 || ( N + 1 ) /\ ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... N ) -> ( A mod 8 ) e. S ) ) )

Proof

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 ) ) )