Description: Any number K whose mod base N is divisible by a divisor P of the base is also divisible by P . This means that primes will also be relatively prime to the base when reduced mod N for any base. (Contributed by Mario Carneiro, 13-Mar-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | dvdsmod | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl3 | |
|
2 | 1 | zred | |
3 | simpl2 | |
|
4 | 3 | nnrpd | |
5 | modval | |
|
6 | 2 4 5 | syl2anc | |
7 | 6 | breq2d | |
8 | simpl1 | |
|
9 | 8 | nnzd | |
10 | 3 | nnzd | |
11 | 2 3 | nndivred | |
12 | 11 | flcld | |
13 | simpr | |
|
14 | 9 10 12 13 | dvdsmultr1d | |
15 | 10 12 | zmulcld | |
16 | 15 | zcnd | |
17 | 16 | subid1d | |
18 | 14 17 | breqtrrd | |
19 | 0zd | |
|
20 | moddvds | |
|
21 | 8 15 19 20 | syl3anc | |
22 | 18 21 | mpbird | |
23 | 22 | eqeq2d | |
24 | moddvds | |
|
25 | 8 1 15 24 | syl3anc | |
26 | moddvds | |
|
27 | 8 1 19 26 | syl3anc | |
28 | 23 25 27 | 3bitr3d | |
29 | 1 | zcnd | |
30 | 29 | subid1d | |
31 | 30 | breq2d | |
32 | 7 28 31 | 3bitrd | |