Metamath Proof Explorer


Theorem lgsdir2lem1

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

Ref Expression
Assertion lgsdir2lem1 1mod8=1-1mod8=73mod8=3-3mod8=5

Proof

Step Hyp Ref Expression
1 1re 1
2 8re 8
3 8pos 0<8
4 2 3 elrpii 8+
5 0le1 01
6 1lt8 1<8
7 modid 18+011<81mod8=1
8 1 4 5 6 7 mp4an 1mod8=1
9 8cn 8
10 9 mulid2i 18=8
11 10 oveq2i -1+18=-1+8
12 ax-1cn 1
13 12 negcli 1
14 9 12 negsubi 8+-1=81
15 8m1e7 81=7
16 14 15 eqtri 8+-1=7
17 9 13 16 addcomli -1+8=7
18 11 17 eqtri -1+18=7
19 18 oveq1i -1+18mod8=7mod8
20 1 renegcli 1
21 1z 1
22 modcyc 18+1-1+18mod8=-1mod8
23 20 4 21 22 mp3an -1+18mod8=-1mod8
24 7re 7
25 0re 0
26 7pos 0<7
27 25 24 26 ltleii 07
28 7lt8 7<8
29 modid 78+077<87mod8=7
30 24 4 27 28 29 mp4an 7mod8=7
31 19 23 30 3eqtr3i -1mod8=7
32 8 31 pm3.2i 1mod8=1-1mod8=7
33 3re 3
34 3pos 0<3
35 25 33 34 ltleii 03
36 3lt8 3<8
37 modid 38+033<83mod8=3
38 33 4 35 36 37 mp4an 3mod8=3
39 10 oveq2i -3+18=-3+8
40 3cn 3
41 40 negcli 3
42 9 40 negsubi 8+-3=83
43 5cn 5
44 5p3e8 5+3=8
45 43 40 44 addcomli 3+5=8
46 9 40 43 45 subaddrii 83=5
47 42 46 eqtri 8+-3=5
48 9 41 47 addcomli -3+8=5
49 39 48 eqtri -3+18=5
50 49 oveq1i -3+18mod8=5mod8
51 33 renegcli 3
52 modcyc 38+1-3+18mod8=-3mod8
53 51 4 21 52 mp3an -3+18mod8=-3mod8
54 5re 5
55 5pos 0<5
56 25 54 55 ltleii 05
57 5lt8 5<8
58 modid 58+055<85mod8=5
59 54 4 56 57 58 mp4an 5mod8=5
60 50 53 59 3eqtr3i -3mod8=5
61 38 60 pm3.2i 3mod8=3-3mod8=5
62 32 61 pm3.2i 1mod8=1-1mod8=73mod8=3-3mod8=5