Description: Constant multiplication in a modulo operation, see theorem 5.3 in ApostolNT p. 108. (Contributed by AV, 21-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | modmulconst | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnz | |
|
2 | 1 | adantl | |
3 | zsubcl | |
|
4 | 3 | 3adant3 | |
5 | 4 | adantr | |
6 | nnz | |
|
7 | nnne0 | |
|
8 | 6 7 | jca | |
9 | 8 | 3ad2ant3 | |
10 | 9 | adantr | |
11 | dvdscmulr | |
|
12 | 11 | bicomd | |
13 | 2 5 10 12 | syl3anc | |
14 | zcn | |
|
15 | zcn | |
|
16 | nncn | |
|
17 | 14 15 16 | 3anim123i | |
18 | 3anrot | |
|
19 | 17 18 | sylibr | |
20 | subdi | |
|
21 | 19 20 | syl | |
22 | 21 | adantr | |
23 | 22 | breq2d | |
24 | 13 23 | bitrd | |
25 | simpr | |
|
26 | simp1 | |
|
27 | 26 | adantr | |
28 | simp2 | |
|
29 | 28 | adantr | |
30 | moddvds | |
|
31 | 25 27 29 30 | syl3anc | |
32 | simpl3 | |
|
33 | 32 25 | nnmulcld | |
34 | 6 | 3ad2ant3 | |
35 | 34 26 | zmulcld | |
36 | 35 | adantr | |
37 | 34 28 | zmulcld | |
38 | 37 | adantr | |
39 | moddvds | |
|
40 | 33 36 38 39 | syl3anc | |
41 | 24 31 40 | 3bitr4d | |