Description: Lemma for lgsdir2 . (Contributed by Mario Carneiro, 4-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | lgsdir2lem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re | |
|
2 | 8re | |
|
3 | 8pos | |
|
4 | 2 3 | elrpii | |
5 | 0le1 | |
|
6 | 1lt8 | |
|
7 | modid | |
|
8 | 1 4 5 6 7 | mp4an | |
9 | 8cn | |
|
10 | 9 | mulid2i | |
11 | 10 | oveq2i | |
12 | ax-1cn | |
|
13 | 12 | negcli | |
14 | 9 12 | negsubi | |
15 | 8m1e7 | |
|
16 | 14 15 | eqtri | |
17 | 9 13 16 | addcomli | |
18 | 11 17 | eqtri | |
19 | 18 | oveq1i | |
20 | 1 | renegcli | |
21 | 1z | |
|
22 | modcyc | |
|
23 | 20 4 21 22 | mp3an | |
24 | 7re | |
|
25 | 0re | |
|
26 | 7pos | |
|
27 | 25 24 26 | ltleii | |
28 | 7lt8 | |
|
29 | modid | |
|
30 | 24 4 27 28 29 | mp4an | |
31 | 19 23 30 | 3eqtr3i | |
32 | 8 31 | pm3.2i | |
33 | 3re | |
|
34 | 3pos | |
|
35 | 25 33 34 | ltleii | |
36 | 3lt8 | |
|
37 | modid | |
|
38 | 33 4 35 36 37 | mp4an | |
39 | 10 | oveq2i | |
40 | 3cn | |
|
41 | 40 | negcli | |
42 | 9 40 | negsubi | |
43 | 5cn | |
|
44 | 5p3e8 | |
|
45 | 43 40 44 | addcomli | |
46 | 9 40 43 45 | subaddrii | |
47 | 42 46 | eqtri | |
48 | 9 41 47 | addcomli | |
49 | 39 48 | eqtri | |
50 | 49 | oveq1i | |
51 | 33 | renegcli | |
52 | modcyc | |
|
53 | 51 4 21 52 | mp3an | |
54 | 5re | |
|
55 | 5pos | |
|
56 | 25 54 55 | ltleii | |
57 | 5lt8 | |
|
58 | modid | |
|
59 | 54 4 56 57 58 | mp4an | |
60 | 50 53 59 | 3eqtr3i | |
61 | 38 60 | pm3.2i | |
62 | 32 61 | pm3.2i | |