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