Description: Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | alzdvds | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnssz | |
|
2 | zcn | |
|
3 | 2 | abscld | |
4 | arch | |
|
5 | 3 4 | syl | |
6 | ssrexv | |
|
7 | 1 5 6 | mpsyl | |
8 | zre | |
|
9 | ltnle | |
|
10 | 3 8 9 | syl2an | |
11 | 10 | rexbidva | |
12 | rexnal | |
|
13 | 11 12 | bitrdi | |
14 | 7 13 | mpbid | |
15 | 14 | adantl | |
16 | ralim | |
|
17 | dvdsleabs | |
|
18 | 17 | 3expb | |
19 | 18 | expcom | |
20 | 19 | ralrimiv | |
21 | 16 20 | syl11 | |
22 | 21 | expdimp | |
23 | 15 22 | mtod | |
24 | nne | |
|
25 | 23 24 | sylib | |
26 | 25 | expcom | |
27 | dvds0 | |
|
28 | breq2 | |
|
29 | 27 28 | syl5ibr | |
30 | 29 | ralrimiv | |
31 | 26 30 | impbid1 | |