Metamath Proof Explorer


Theorem fzm1ndvds

Description: No number between 1 and M - 1 divides M . (Contributed by Mario Carneiro, 24-Jan-2015)

Ref Expression
Assertion fzm1ndvds MN1M1¬MN

Proof

Step Hyp Ref Expression
1 elfzle2 N1M1NM1
2 1 adantl MN1M1NM1
3 elfzelz N1M1N
4 3 adantl MN1M1N
5 nnz MM
6 5 adantr MN1M1M
7 zltlem1 NMN<MNM1
8 4 6 7 syl2anc MN1M1N<MNM1
9 2 8 mpbird MN1M1N<M
10 elfznn N1M1N
11 10 adantl MN1M1N
12 11 nnred MN1M1N
13 nnre MM
14 13 adantr MN1M1M
15 12 14 ltnled MN1M1N<M¬MN
16 9 15 mpbid MN1M1¬MN
17 dvdsle MNMNMN
18 6 11 17 syl2anc MN1M1MNMN
19 16 18 mtod MN1M1¬MN