Metamath Proof Explorer


Theorem dvds1

Description: The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015)

Ref Expression
Assertion dvds1 M0M1M=1

Proof

Step Hyp Ref Expression
1 simpl M0M1M0
2 1nn0 10
3 2 a1i M0M110
4 simpr M0M1M1
5 nn0z M0M
6 1dvds M1M
7 5 6 syl M01M
8 7 adantr M0M11M
9 dvdseq M010M11MM=1
10 1 3 4 8 9 syl22anc M0M1M=1
11 10 ex M0M1M=1
12 id M=1M=1
13 1z 1
14 iddvds 111
15 13 14 ax-mp 11
16 12 15 eqbrtrdi M=1M1
17 11 16 impbid1 M0M1M=1