Description: The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | dvds1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | |
|
2 | 1nn0 | |
|
3 | 2 | a1i | |
4 | simpr | |
|
5 | nn0z | |
|
6 | 1dvds | |
|
7 | 5 6 | syl | |
8 | 7 | adantr | |
9 | dvdseq | |
|
10 | 1 3 4 8 9 | syl22anc | |
11 | 10 | ex | |
12 | id | |
|
13 | 1z | |
|
14 | iddvds | |
|
15 | 13 14 | ax-mp | |
16 | 12 15 | eqbrtrdi | |
17 | 11 16 | impbid1 | |