Metamath Proof Explorer

Theorem lgsdir2lem1

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

Ref Expression
Assertion lgsdir2lem1 
|- ( ( ( 1 mod 8 ) = 1 /\ ( -u 1 mod 8 ) = 7 ) /\ ( ( 3 mod 8 ) = 3 /\ ( -u 3 mod 8 ) = 5 ) )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 8re 
 |-  8 e. RR
3 8pos 
 |-  0 < 8
4 2 3 elrpii 
 |-  8 e. RR+
5 0le1 
 |-  0 <_ 1
6 1lt8 
 |-  1 < 8
7 modid 
 |-  ( ( ( 1 e. RR /\ 8 e. RR+ ) /\ ( 0 <_ 1 /\ 1 < 8 ) ) -> ( 1 mod 8 ) = 1 )
8 1 4 5 6 7 mp4an 
 |-  ( 1 mod 8 ) = 1
9 8cn 
 |-  8 e. CC
10 9 mulid2i 
 |-  ( 1 x. 8 ) = 8
11 10 oveq2i 
 |-  ( -u 1 + ( 1 x. 8 ) ) = ( -u 1 + 8 )
12 ax-1cn 
 |-  1 e. CC
13 12 negcli 
 |-  -u 1 e. CC
14 9 12 negsubi 
 |-  ( 8 + -u 1 ) = ( 8 - 1 )
15 8m1e7 
 |-  ( 8 - 1 ) = 7
16 14 15 eqtri 
 |-  ( 8 + -u 1 ) = 7
17 9 13 16 addcomli 
 |-  ( -u 1 + 8 ) = 7
18 11 17 eqtri 
 |-  ( -u 1 + ( 1 x. 8 ) ) = 7
19 18 oveq1i 
 |-  ( ( -u 1 + ( 1 x. 8 ) ) mod 8 ) = ( 7 mod 8 )
20 1 renegcli 
 |-  -u 1 e. RR
21 1z 
 |-  1 e. ZZ
22 modcyc 
 |-  ( ( -u 1 e. RR /\ 8 e. RR+ /\ 1 e. ZZ ) -> ( ( -u 1 + ( 1 x. 8 ) ) mod 8 ) = ( -u 1 mod 8 ) )
23 20 4 21 22 mp3an 
 |-  ( ( -u 1 + ( 1 x. 8 ) ) mod 8 ) = ( -u 1 mod 8 )
24 7re 
 |-  7 e. RR
25 0re 
 |-  0 e. RR
26 7pos 
 |-  0 < 7
27 25 24 26 ltleii 
 |-  0 <_ 7
28 7lt8 
 |-  7 < 8
29 modid 
 |-  ( ( ( 7 e. RR /\ 8 e. RR+ ) /\ ( 0 <_ 7 /\ 7 < 8 ) ) -> ( 7 mod 8 ) = 7 )
30 24 4 27 28 29 mp4an 
 |-  ( 7 mod 8 ) = 7
31 19 23 30 3eqtr3i 
 |-  ( -u 1 mod 8 ) = 7
32 8 31 pm3.2i 
 |-  ( ( 1 mod 8 ) = 1 /\ ( -u 1 mod 8 ) = 7 )
33 3re 
 |-  3 e. RR
34 3pos 
 |-  0 < 3
35 25 33 34 ltleii 
 |-  0 <_ 3
36 3lt8 
 |-  3 < 8
37 modid 
 |-  ( ( ( 3 e. RR /\ 8 e. RR+ ) /\ ( 0 <_ 3 /\ 3 < 8 ) ) -> ( 3 mod 8 ) = 3 )
38 33 4 35 36 37 mp4an 
 |-  ( 3 mod 8 ) = 3
39 10 oveq2i 
 |-  ( -u 3 + ( 1 x. 8 ) ) = ( -u 3 + 8 )
40 3cn 
 |-  3 e. CC
41 40 negcli 
 |-  -u 3 e. CC
42 9 40 negsubi 
 |-  ( 8 + -u 3 ) = ( 8 - 3 )
43 5cn 
 |-  5 e. CC
44 5p3e8 
 |-  ( 5 + 3 ) = 8
45 43 40 44 addcomli 
 |-  ( 3 + 5 ) = 8
46 9 40 43 45 subaddrii 
 |-  ( 8 - 3 ) = 5
47 42 46 eqtri 
 |-  ( 8 + -u 3 ) = 5
48 9 41 47 addcomli 
 |-  ( -u 3 + 8 ) = 5
49 39 48 eqtri 
 |-  ( -u 3 + ( 1 x. 8 ) ) = 5
50 49 oveq1i 
 |-  ( ( -u 3 + ( 1 x. 8 ) ) mod 8 ) = ( 5 mod 8 )
51 33 renegcli 
 |-  -u 3 e. RR
52 modcyc 
 |-  ( ( -u 3 e. RR /\ 8 e. RR+ /\ 1 e. ZZ ) -> ( ( -u 3 + ( 1 x. 8 ) ) mod 8 ) = ( -u 3 mod 8 ) )
53 51 4 21 52 mp3an 
 |-  ( ( -u 3 + ( 1 x. 8 ) ) mod 8 ) = ( -u 3 mod 8 )
54 5re 
 |-  5 e. RR
55 5pos 
 |-  0 < 5
56 25 54 55 ltleii 
 |-  0 <_ 5
57 5lt8 
 |-  5 < 8
58 modid 
 |-  ( ( ( 5 e. RR /\ 8 e. RR+ ) /\ ( 0 <_ 5 /\ 5 < 8 ) ) -> ( 5 mod 8 ) = 5 )
59 54 4 56 57 58 mp4an 
 |-  ( 5 mod 8 ) = 5
60 50 53 59 3eqtr3i 
 |-  ( -u 3 mod 8 ) = 5
61 38 60 pm3.2i 
 |-  ( ( 3 mod 8 ) = 3 /\ ( -u 3 mod 8 ) = 5 )
62 32 61 pm3.2i 
 |-  ( ( ( 1 mod 8 ) = 1 /\ ( -u 1 mod 8 ) = 7 ) /\ ( ( 3 mod 8 ) = 3 /\ ( -u 3 mod 8 ) = 5 ) )