Metamath Proof Explorer

Theorem alzdvds

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

Ref Expression
Assertion alzdvds 
|- ( N e. ZZ -> ( A. x e. ZZ x || N <-> N = 0 ) )

Proof

Step Hyp Ref Expression
1 nnssz 
 |-  NN C_ ZZ
2 zcn 
 |-  ( N e. ZZ -> N e. CC )
3 2 abscld 
 |-  ( N e. ZZ -> ( abs ` N ) e. RR )
4 arch 
 |-  ( ( abs ` N ) e. RR -> E. x e. NN ( abs ` N ) < x )
5 3 4 syl 
 |-  ( N e. ZZ -> E. x e. NN ( abs ` N ) < x )
6 ssrexv 
 |-  ( NN C_ ZZ -> ( E. x e. NN ( abs ` N ) < x -> E. x e. ZZ ( abs ` N ) < x ) )
7 1 5 6 mpsyl 
 |-  ( N e. ZZ -> E. x e. ZZ ( abs ` N ) < x )
8 zre 
 |-  ( x e. ZZ -> x e. RR )
9 ltnle 
 |-  ( ( ( abs ` N ) e. RR /\ x e. RR ) -> ( ( abs ` N ) < x <-> -. x <_ ( abs ` N ) ) )
10 3 8 9 syl2an 
 |-  ( ( N e. ZZ /\ x e. ZZ ) -> ( ( abs ` N ) < x <-> -. x <_ ( abs ` N ) ) )
11 10 rexbidva 
 |-  ( N e. ZZ -> ( E. x e. ZZ ( abs ` N ) < x <-> E. x e. ZZ -. x <_ ( abs ` N ) ) )
12 rexnal 
 |-  ( E. x e. ZZ -. x <_ ( abs ` N ) <-> -. A. x e. ZZ x <_ ( abs ` N ) )
13 11 12 bitrdi 
 |-  ( N e. ZZ -> ( E. x e. ZZ ( abs ` N ) < x <-> -. A. x e. ZZ x <_ ( abs ` N ) ) )
14 7 13 mpbid 
 |-  ( N e. ZZ -> -. A. x e. ZZ x <_ ( abs ` N ) )
15 14 adantl 
 |-  ( ( A. x e. ZZ x || N /\ N e. ZZ ) -> -. A. x e. ZZ x <_ ( abs ` N ) )
16 ralim 
 |-  ( A. x e. ZZ ( x || N -> x <_ ( abs ` N ) ) -> ( A. x e. ZZ x || N -> A. x e. ZZ x <_ ( abs ` N ) ) )
17 dvdsleabs 
 |-  ( ( x e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( x || N -> x <_ ( abs ` N ) ) )
18 17 3expb 
 |-  ( ( x e. ZZ /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( x || N -> x <_ ( abs ` N ) ) )
19 18 expcom 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( x e. ZZ -> ( x || N -> x <_ ( abs ` N ) ) ) )
20 19 ralrimiv 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> A. x e. ZZ ( x || N -> x <_ ( abs ` N ) ) )
21 16 20 syl11 
 |-  ( A. x e. ZZ x || N -> ( ( N e. ZZ /\ N =/= 0 ) -> A. x e. ZZ x <_ ( abs ` N ) ) )
22 21 expdimp 
 |-  ( ( A. x e. ZZ x || N /\ N e. ZZ ) -> ( N =/= 0 -> A. x e. ZZ x <_ ( abs ` N ) ) )
23 15 22 mtod 
 |-  ( ( A. x e. ZZ x || N /\ N e. ZZ ) -> -. N =/= 0 )
24 nne 
 |-  ( -. N =/= 0 <-> N = 0 )
25 23 24 sylib 
 |-  ( ( A. x e. ZZ x || N /\ N e. ZZ ) -> N = 0 )
26 25 expcom 
 |-  ( N e. ZZ -> ( A. x e. ZZ x || N -> N = 0 ) )
27 dvds0 
 |-  ( x e. ZZ -> x || 0 )
28 breq2 
 |-  ( N = 0 -> ( x || N <-> x || 0 ) )
29 27 28 syl5ibr 
 |-  ( N = 0 -> ( x e. ZZ -> x || N ) )
30 29 ralrimiv 
 |-  ( N = 0 -> A. x e. ZZ x || N )
31 26 30 impbid1 
 |-  ( N e. ZZ -> ( A. x e. ZZ x || N <-> N = 0 ) )