Description: Zero is the only one of the first A nonnegative integers that is divisible by A . (Contributed by Stefan O'Rear, 6-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fzo0dvdseq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzolt2 | |
|
2 | elfzoelz | |
|
3 | 2 | zred | |
4 | elfzoel2 | |
|
5 | 4 | zred | |
6 | 3 5 | ltnled | |
7 | 1 6 | mpbid | |
8 | 7 | adantr | |
9 | elfzonn0 | |
|
10 | 9 | adantr | |
11 | simpr | |
|
12 | eldifsn | |
|
13 | 10 11 12 | sylanbrc | |
14 | dfn2 | |
|
15 | 13 14 | eleqtrrdi | |
16 | dvdsle | |
|
17 | 4 15 16 | syl2an2r | |
18 | 8 17 | mtod | |
19 | 18 | ex | |
20 | 19 | necon4ad | |
21 | dvds0 | |
|
22 | 4 21 | syl | |
23 | breq2 | |
|
24 | 22 23 | syl5ibrcom | |
25 | 20 24 | impbid | |