Description: No number between 1 and M - 1 divides M . (Contributed by Mario Carneiro, 24-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fzm1ndvds | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzle2 | |
|
2 | 1 | adantl | |
3 | elfzelz | |
|
4 | 3 | adantl | |
5 | nnz | |
|
6 | 5 | adantr | |
7 | zltlem1 | |
|
8 | 4 6 7 | syl2anc | |
9 | 2 8 | mpbird | |
10 | elfznn | |
|
11 | 10 | adantl | |
12 | 11 | nnred | |
13 | nnre | |
|
14 | 13 | adantr | |
15 | 12 14 | ltnled | |
16 | 9 15 | mpbid | |
17 | dvdsle | |
|
18 | 6 11 17 | syl2anc | |
19 | 16 18 | mtod | |