Proof of Theorem lgsdir2lem5
Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. . . . . . 7
|
2 | 1 | elpr 4198 |
. . . . . 6
|
3 | | ovex 6678 |
. . . . . . 7
|
4 | 3 | elpr 4198 |
. . . . . 6
|
5 | 2, 4 | anbi12i 733 |
. . . . 5
|
6 | | simpll 790 |
. . . . . . . . 9
|
7 | | 3z 11410 |
. . . . . . . . . 10
|
8 | 7 | a1i 11 |
. . . . . . . . 9
|
9 | | simplr 792 |
. . . . . . . . 9
|
10 | | 8re 11105 |
. . . . . . . . . . 11
|
11 | | 8pos 11121 |
. . . . . . . . . . 11
|
12 | 10, 11 | elrpii 11835 |
. . . . . . . . . 10
|
13 | 12 | a1i 11 |
. . . . . . . . 9
|
14 | | simprl 794 |
. . . . . . . . . 10
|
15 | | lgsdir2lem1 25050 |
. . . . . . . . . . . 12
|
16 | 15 | simpri 478 |
. . . . . . . . . . 11
|
17 | 16 | simpli 474 |
. . . . . . . . . 10
|
18 | 14, 17 | syl6eqr 2674 |
. . . . . . . . 9
|
19 | | simprr 796 |
. . . . . . . . . 10
|
20 | 19, 17 | syl6eqr 2674 |
. . . . . . . . 9
|
21 | 6, 8, 9, 8, 13, 18, 20 | modmul12d 12724 |
. . . . . . . 8
|
22 | 21 | orcd 407 |
. . . . . . 7
|
23 | 22 | ex 450 |
. . . . . 6
|
24 | | simpll 790 |
. . . . . . . . . 10
|
25 | | znegcl 11412 |
. . . . . . . . . . 11
|
26 | 7, 25 | mp1i 13 |
. . . . . . . . . 10
|
27 | | simplr 792 |
. . . . . . . . . 10
|
28 | 7 | a1i 11 |
. . . . . . . . . 10
|
29 | 12 | a1i 11 |
. . . . . . . . . 10
|
30 | | simprl 794 |
. . . . . . . . . . 11
|
31 | 16 | simpri 478 |
. . . . . . . . . . 11
|
32 | 30, 31 | syl6eqr 2674 |
. . . . . . . . . 10
|
33 | | simprr 796 |
. . . . . . . . . . 11
|
34 | 33, 17 | syl6eqr 2674 |
. . . . . . . . . 10
|
35 | 24, 26, 27, 28, 29, 32, 34 | modmul12d 12724 |
. . . . . . . . 9
|
36 | | 3cn 11095 |
. . . . . . . . . . 11
|
37 | 36, 36 | mulneg1i 10476 |
. . . . . . . . . 10
|
38 | 37 | oveq1i 6660 |
. . . . . . . . 9
|
39 | 35, 38 | syl6eq 2672 |
. . . . . . . 8
|
40 | 39 | olcd 408 |
. . . . . . 7
|
41 | 40 | ex 450 |
. . . . . 6
|
42 | | simpll 790 |
. . . . . . . . . 10
|
43 | 7 | a1i 11 |
. . . . . . . . . 10
|
44 | | simplr 792 |
. . . . . . . . . 10
|
45 | 7, 25 | mp1i 13 |
. . . . . . . . . 10
|
46 | 12 | a1i 11 |
. . . . . . . . . 10
|
47 | | simprl 794 |
. . . . . . . . . . 11
|
48 | 47, 17 | syl6eqr 2674 |
. . . . . . . . . 10
|
49 | | simprr 796 |
. . . . . . . . . . 11
|
50 | 49, 31 | syl6eqr 2674 |
. . . . . . . . . 10
|
51 | 42, 43, 44, 45, 46, 48, 50 | modmul12d 12724 |
. . . . . . . . 9
|
52 | 36, 36 | mulneg2i 10477 |
. . . . . . . . . 10
|
53 | 52 | oveq1i 6660 |
. . . . . . . . 9
|
54 | 51, 53 | syl6eq 2672 |
. . . . . . . 8
|
55 | 54 | olcd 408 |
. . . . . . 7
|
56 | 55 | ex 450 |
. . . . . 6
|
57 | | simpll 790 |
. . . . . . . . . 10
|
58 | 7, 25 | mp1i 13 |
. . . . . . . . . 10
|
59 | | simplr 792 |
. . . . . . . . . 10
|
60 | 12 | a1i 11 |
. . . . . . . . . 10
|
61 | | simprl 794 |
. . . . . . . . . . 11
|
62 | 61, 31 | syl6eqr 2674 |
. . . . . . . . . 10
|
63 | | simprr 796 |
. . . . . . . . . . 11
|
64 | 63, 31 | syl6eqr 2674 |
. . . . . . . . . 10
|
65 | 57, 58, 59, 58, 60, 62, 64 | modmul12d 12724 |
. . . . . . . . 9
|
66 | 36, 36 | mul2negi 10478 |
. . . . . . . . . 10
|
67 | 66 | oveq1i 6660 |
. . . . . . . . 9
|
68 | 65, 67 | syl6eq 2672 |
. . . . . . . 8
|
69 | 68 | orcd 407 |
. . . . . . 7
|
70 | 69 | ex 450 |
. . . . . 6
|
71 | 23, 41, 56, 70 | ccased 988 |
. . . . 5
|
72 | 5, 71 | syl5bi 232 |
. . . 4
|
73 | 72 | imp 445 |
. . 3
|
74 | | ovex 6678 |
. . . 4
|
75 | 74 | elpr 4198 |
. . 3
|
76 | 73, 75 | sylibr 224 |
. 2
|
77 | | df-9 11086 |
. . . . . . . 8
|
78 | | 8cn 11106 |
. . . . . . . . 9
|
79 | | ax-1cn 9994 |
. . . . . . . . 9
|
80 | 78, 79 | addcomi 10227 |
. . . . . . . 8
|
81 | 77, 80 | eqtri 2644 |
. . . . . . 7
|
82 | | 3t3e9 11180 |
. . . . . . 7
|
83 | 78 | mulid2i 10043 |
. . . . . . . 8
|
84 | 83 | oveq2i 6661 |
. . . . . . 7
|
85 | 81, 82, 84 | 3eqtr4i 2654 |
. . . . . 6
|
86 | 85 | oveq1i 6660 |
. . . . 5
|
87 | | 1re 10039 |
. . . . . 6
|
88 | | 1z 11407 |
. . . . . 6
|
89 | | modcyc 12705 |
. . . . . 6
|
90 | 87, 12, 88, 89 | mp3an 1424 |
. . . . 5
|
91 | 86, 90 | eqtri 2644 |
. . . 4
|
92 | 15 | simpli 474 |
. . . . 5
|
93 | 92 | simpli 474 |
. . . 4
|
94 | 91, 93 | eqtri 2644 |
. . 3
|
95 | | znegcl 11412 |
. . . . . . . 8
|
96 | 88, 95 | mp1i 13 |
. . . . . . 7
|
97 | | 3nn 11186 |
. . . . . . . . . 10
|
98 | 97, 97 | nnmulcli 11044 |
. . . . . . . . 9
|
99 | 98 | nnzi 11401 |
. . . . . . . 8
|
100 | 99 | a1i 11 |
. . . . . . 7
|
101 | 88 | a1i 11 |
. . . . . . 7
|
102 | 12 | a1i 11 |
. . . . . . 7
|
103 | | eqidd 2623 |
. . . . . . 7
|
104 | 91 | a1i 11 |
. . . . . . 7
|
105 | 96, 96, 100, 101, 102, 103, 104 | modmul12d 12724 |
. . . . . 6
|
106 | 105 | trud 1493 |
. . . . 5
|
107 | 36, 36 | mulcli 10045 |
. . . . . . 7
|
108 | 107 | mulm1i 10475 |
. . . . . 6
|
109 | 108 | oveq1i 6660 |
. . . . 5
|
110 | 79 | mulm1i 10475 |
. . . . . 6
|
111 | 110 | oveq1i 6660 |
. . . . 5
|
112 | 106, 109,
111 | 3eqtr3i 2652 |
. . . 4
|
113 | 92 | simpri 478 |
. . . 4
|
114 | 112, 113 | eqtri 2644 |
. . 3
|
115 | 94, 114 | preq12i 4273 |
. 2
|
116 | 76, 115 | syl6eleq 2711 |
1
|