This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0dvds

Description: Only 0 is divisible by 0. Theorem 1.1(h) in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion 0dvds 
|- ( N e. ZZ -> ( 0 || N <-> N = 0 ) )

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 divides 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( 0 || N <-> E. n e. ZZ ( n x. 0 ) = N ) )
3 1 2 mpan 
 |-  ( N e. ZZ -> ( 0 || N <-> E. n e. ZZ ( n x. 0 ) = N ) )
4 zcn 
 |-  ( n e. ZZ -> n e. CC )
5 4 mul01d 
 |-  ( n e. ZZ -> ( n x. 0 ) = 0 )
6 eqtr2 
 |-  ( ( ( n x. 0 ) = N /\ ( n x. 0 ) = 0 ) -> N = 0 )
7 5 6 sylan2 
 |-  ( ( ( n x. 0 ) = N /\ n e. ZZ ) -> N = 0 )
8 7 ancoms 
 |-  ( ( n e. ZZ /\ ( n x. 0 ) = N ) -> N = 0 )
9 8 rexlimiva 
 |-  ( E. n e. ZZ ( n x. 0 ) = N -> N = 0 )
10 3 9 biimtrdi 
 |-  ( N e. ZZ -> ( 0 || N -> N = 0 ) )
11 dvds0 
 |-  ( 0 e. ZZ -> 0 || 0 )
12 1 11 ax-mp 
 |-  0 || 0
13 breq2 
 |-  ( N = 0 -> ( 0 || N <-> 0 || 0 ) )
14 12 13 mpbiri 
 |-  ( N = 0 -> 0 || N )
15 10 14 impbid1 
 |-  ( N e. ZZ -> ( 0 || N <-> N = 0 ) )