Metamath Proof Explorer


Theorem alzdvds

Description: Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion alzdvds NxxNN=0

Proof

Step Hyp Ref Expression
1 nnssz
2 zcn NN
3 2 abscld NN
4 arch NxN<x
5 3 4 syl NxN<x
6 ssrexv xN<xxN<x
7 1 5 6 mpsyl NxN<x
8 zre xx
9 ltnle NxN<x¬xN
10 3 8 9 syl2an NxN<x¬xN
11 10 rexbidva NxN<xx¬xN
12 rexnal x¬xN¬xxN
13 11 12 bitrdi NxN<x¬xxN
14 7 13 mpbid N¬xxN
15 14 adantl xxNN¬xxN
16 ralim xxNxNxxNxxN
17 dvdsleabs xNN0xNxN
18 17 3expb xNN0xNxN
19 18 expcom NN0xxNxN
20 19 ralrimiv NN0xxNxN
21 16 20 syl11 xxNNN0xxN
22 21 expdimp xxNNN0xxN
23 15 22 mtod xxNN¬N0
24 nne ¬N0N=0
25 23 24 sylib xxNNN=0
26 25 expcom NxxNN=0
27 dvds0 xx0
28 breq2 N=0xNx0
29 27 28 syl5ibr N=0xxN
30 29 ralrimiv N=0xxN
31 26 30 impbid1 NxxNN=0