Step | Hyp | Ref
| Expression |
1 | | zmodcl 12690 |
. . . . . . . . . . . . . . . 16
|
2 | 1 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
|
3 | 2 | nn0zd 11480 |
. . . . . . . . . . . . . 14
|
4 | 3 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
5 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
6 | 5 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
7 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . . 19
|
8 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
|
9 | 8 | notbid 308 |
. . . . . . . . . . . . . . . . . . 19
|
10 | 7, 9 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . 18
|
11 | 10 | necon2ad 2809 |
. . . . . . . . . . . . . . . . 17
|
12 | 11 | imp 445 |
. . . . . . . . . . . . . . . 16
|
13 | | eldifsn 4317 |
. . . . . . . . . . . . . . . 16
|
14 | 6, 12, 13 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
|
15 | | oddprm 15515 |
. . . . . . . . . . . . . . 15
|
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . 14
|
17 | 16 | nnnn0d 11351 |
. . . . . . . . . . . . 13
|
18 | | zexpcl 12875 |
. . . . . . . . . . . . 13
|
19 | 4, 17, 18 | syl2anc 693 |
. . . . . . . . . . . 12
|
20 | 19 | zred 11482 |
. . . . . . . . . . 11
|
21 | | simpll1 1100 |
. . . . . . . . . . . . 13
|
22 | | zexpcl 12875 |
. . . . . . . . . . . . 13
|
23 | 21, 17, 22 | syl2anc 693 |
. . . . . . . . . . . 12
|
24 | 23 | zred 11482 |
. . . . . . . . . . 11
|
25 | | 1red 10055 |
. . . . . . . . . . 11
|
26 | | prmnn 15388 |
. . . . . . . . . . . . 13
|
27 | 26 | ad2antlr 763 |
. . . . . . . . . . . 12
|
28 | 27 | nnrpd 11870 |
. . . . . . . . . . 11
|
29 | | simpr 477 |
. . . . . . . . . . . . . 14
|
30 | 21 | zred 11482 |
. . . . . . . . . . . . . . . 16
|
31 | | simp2 1062 |
. . . . . . . . . . . . . . . . . 18
|
32 | 31 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
33 | 32 | nnrpd 11870 |
. . . . . . . . . . . . . . . 16
|
34 | | modabs2 12704 |
. . . . . . . . . . . . . . . 16
|
35 | 30, 33, 34 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
36 | | moddvds 14991 |
. . . . . . . . . . . . . . . 16
|
37 | 32, 4, 21, 36 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
38 | 35, 37 | mpbid 222 |
. . . . . . . . . . . . . 14
|
39 | | prmz 15389 |
. . . . . . . . . . . . . . . 16
|
40 | 39 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
|
41 | 32 | nnzd 11481 |
. . . . . . . . . . . . . . 15
|
42 | 4, 21 | zsubcld 11487 |
. . . . . . . . . . . . . . 15
|
43 | | dvdstr 15018 |
. . . . . . . . . . . . . . 15
|
44 | 40, 41, 42, 43 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
45 | 29, 38, 44 | mp2and 715 |
. . . . . . . . . . . . 13
|
46 | | moddvds 14991 |
. . . . . . . . . . . . . 14
|
47 | 27, 4, 21, 46 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
48 | 45, 47 | mpbird 247 |
. . . . . . . . . . . 12
|
49 | | modexp 12999 |
. . . . . . . . . . . 12
|
50 | 4, 21, 17, 28, 48, 49 | syl221anc 1337 |
. . . . . . . . . . 11
|
51 | | modadd1 12707 |
. . . . . . . . . . 11
|
52 | 20, 24, 25, 28, 50, 51 | syl221anc 1337 |
. . . . . . . . . 10
|
53 | 52 | oveq1d 6665 |
. . . . . . . . 9
|
54 | | lgsval3 25040 |
. . . . . . . . . 10
|
55 | 4, 14, 54 | syl2anc 693 |
. . . . . . . . 9
|
56 | | lgsval3 25040 |
. . . . . . . . . 10
|
57 | 21, 14, 56 | syl2anc 693 |
. . . . . . . . 9
|
58 | 53, 55, 57 | 3eqtr4d 2666 |
. . . . . . . 8
|
59 | 58 | oveq1d 6665 |
. . . . . . 7
|
60 | 3 | ad2antrr 762 |
. . . . . . . . . . . 12
|
61 | 39 | ad2antlr 763 |
. . . . . . . . . . . 12
|
62 | | lgscl 25036 |
. . . . . . . . . . . 12
|
63 | 60, 61, 62 | syl2anc 693 |
. . . . . . . . . . 11
|
64 | 63 | zcnd 11483 |
. . . . . . . . . 10
|
65 | 64 | exp0d 13002 |
. . . . . . . . 9
|
66 | | simpll1 1100 |
. . . . . . . . . . . 12
|
67 | | lgscl 25036 |
. . . . . . . . . . . 12
|
68 | 66, 61, 67 | syl2anc 693 |
. . . . . . . . . . 11
|
69 | 68 | zcnd 11483 |
. . . . . . . . . 10
|
70 | 69 | exp0d 13002 |
. . . . . . . . 9
|
71 | 65, 70 | eqtr4d 2659 |
. . . . . . . 8
|
72 | 31 | adantr 481 |
. . . . . . . . . . 11
|
73 | | pceq0 15575 |
. . . . . . . . . . 11
|
74 | 5, 72, 73 | syl2anc 693 |
. . . . . . . . . 10
|
75 | 74 | biimpar 502 |
. . . . . . . . 9
|
76 | 75 | oveq2d 6666 |
. . . . . . . 8
|
77 | 75 | oveq2d 6666 |
. . . . . . . 8
|
78 | 71, 76, 77 | 3eqtr4d 2666 |
. . . . . . 7
|
79 | 59, 78 | pm2.61dan 832 |
. . . . . 6
|
80 | 79 | ifeq1da 4116 |
. . . . 5
|
81 | 80 | mpteq2dv 4745 |
. . . 4
|
82 | 81 | seqeq3d 12809 |
. . 3
|
83 | 82 | fveq1d 6193 |
. 2
|
84 | | eqid 2622 |
. . . 4
|
85 | 84 | lgsval4a 25044 |
. . 3
|
86 | 3, 31, 85 | syl2anc 693 |
. 2
|
87 | | eqid 2622 |
. . . 4
|
88 | 87 | lgsval4a 25044 |
. . 3
|
89 | 88 | 3adant3 1081 |
. 2
|
90 | 83, 86, 89 | 3eqtr4d 2666 |
1
|