Metamath Proof Explorer

Theorem lgsdir2lem3

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

Ref Expression
Assertion lgsdir2lem3 
|- ( ( A e. ZZ /\ -. 2 || A ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. ZZ /\ -. 2 || A ) -> A e. ZZ )
2 8nn 
 |-  8 e. NN
3 zmodfz 
 |-  ( ( A e. ZZ /\ 8 e. NN ) -> ( A mod 8 ) e. ( 0 ... ( 8 - 1 ) ) )
4 1 2 3 sylancl 
 |-  ( ( A e. ZZ /\ -. 2 || A ) -> ( A mod 8 ) e. ( 0 ... ( 8 - 1 ) ) )
5 8m1e7 
 |-  ( 8 - 1 ) = 7
6 5 oveq2i 
 |-  ( 0 ... ( 8 - 1 ) ) = ( 0 ... 7 )
7 4 6 eleqtrdi 
 |-  ( ( A e. ZZ /\ -. 2 || A ) -> ( A mod 8 ) e. ( 0 ... 7 ) )
8 neg1z 
 |-  -u 1 e. ZZ
9 z0even 
 |-  2 || 0
10 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
11 ax-1cn 
 |-  1 e. CC
12 neg1cn 
 |-  -u 1 e. CC
13 11 12 addcomi 
 |-  ( 1 + -u 1 ) = ( -u 1 + 1 )
14 10 13 eqtr3i 
 |-  0 = ( -u 1 + 1 )
15 9 14 breqtri 
 |-  2 || ( -u 1 + 1 )
16 noel 
 |-  -. ( A mod 8 ) e. (/)
17 16 pm2.21i 
 |-  ( ( A mod 8 ) e. (/) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) )
18 neg1lt0 
 |-  -u 1 < 0
19 0z 
 |-  0 e. ZZ
20 fzn 
 |-  ( ( 0 e. ZZ /\ -u 1 e. ZZ ) -> ( -u 1 < 0 <-> ( 0 ... -u 1 ) = (/) ) )
21 19 8 20 mp2an 
 |-  ( -u 1 < 0 <-> ( 0 ... -u 1 ) = (/) )
22 18 21 mpbi 
 |-  ( 0 ... -u 1 ) = (/)
23 17 22 eleq2s 
 |-  ( ( A mod 8 ) e. ( 0 ... -u 1 ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) )
24 23 a1i 
 |-  ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... -u 1 ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) ) )
25 8 15 24 3pm3.2i 
 |-  ( -u 1 e. ZZ /\ 2 || ( -u 1 + 1 ) /\ ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... -u 1 ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) ) ) )
26 1e0p1 
 |-  1 = ( 0 + 1 )
27 ssun1 
 |-  { 1 , 7 } C_ ( { 1 , 7 } u. { 3 , 5 } )
28 1ex 
 |-  1 e. _V
29 28 prid1 
 |-  1 e. { 1 , 7 }
30 27 29 sselii 
 |-  1 e. ( { 1 , 7 } u. { 3 , 5 } )
31 25 14 26 30 lgsdir2lem2 
 |-  ( 1 e. ZZ /\ 2 || ( 1 + 1 ) /\ ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... 1 ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) ) ) )
32 df-2 
 |-  2 = ( 1 + 1 )
33 df-3 
 |-  3 = ( 2 + 1 )
34 ssun2 
 |-  { 3 , 5 } C_ ( { 1 , 7 } u. { 3 , 5 } )
35 3ex 
 |-  3 e. _V
36 35 prid1 
 |-  3 e. { 3 , 5 }
37 34 36 sselii 
 |-  3 e. ( { 1 , 7 } u. { 3 , 5 } )
38 31 32 33 37 lgsdir2lem2 
 |-  ( 3 e. ZZ /\ 2 || ( 3 + 1 ) /\ ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... 3 ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) ) ) )
39 df-4 
 |-  4 = ( 3 + 1 )
40 df-5 
 |-  5 = ( 4 + 1 )
41 5nn 
 |-  5 e. NN
42 41 elexi 
 |-  5 e. _V
43 42 prid2 
 |-  5 e. { 3 , 5 }
44 34 43 sselii 
 |-  5 e. ( { 1 , 7 } u. { 3 , 5 } )
45 38 39 40 44 lgsdir2lem2 
 |-  ( 5 e. ZZ /\ 2 || ( 5 + 1 ) /\ ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... 5 ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) ) ) )
46 df-6 
 |-  6 = ( 5 + 1 )
47 df-7 
 |-  7 = ( 6 + 1 )
48 7nn 
 |-  7 e. NN
49 48 elexi 
 |-  7 e. _V
50 49 prid2 
 |-  7 e. { 1 , 7 }
51 27 50 sselii 
 |-  7 e. ( { 1 , 7 } u. { 3 , 5 } )
52 45 46 47 51 lgsdir2lem2 
 |-  ( 7 e. ZZ /\ 2 || ( 7 + 1 ) /\ ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... 7 ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) ) ) )
53 52 simp3i 
 |-  ( ( A e. ZZ /\ -. 2 || A ) -> ( ( A mod 8 ) e. ( 0 ... 7 ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) ) )
54 7 53 mpd 
 |-  ( ( A e. ZZ /\ -. 2 || A ) -> ( A mod 8 ) e. ( { 1 , 7 } u. { 3 , 5 } ) )