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

Metamath Proof Explorer

Theorem dvdsval3

Description: One nonzero integer divides another integer if and only if the remainder upon division is zero, see remark in ApostolNT p. 106. (Contributed by Mario Carneiro, 22-Feb-2014) (Revised by Mario Carneiro, 15-Jul-2014)

Ref Expression
Assertion dvdsval3 
|- ( ( M e. NN /\ N e. ZZ ) -> ( M || N <-> ( N mod M ) = 0 ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( M e. NN -> M e. ZZ )
2 nnne0 
 |-  ( M e. NN -> M =/= 0 )
3 1 2 jca 
 |-  ( M e. NN -> ( M e. ZZ /\ M =/= 0 ) )
4 dvdsval2 
 |-  ( ( M e. ZZ /\ M =/= 0 /\ N e. ZZ ) -> ( M || N <-> ( N / M ) e. ZZ ) )
5 4 3expa 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ N e. ZZ ) -> ( M || N <-> ( N / M ) e. ZZ ) )
6 3 5 sylan 
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( M || N <-> ( N / M ) e. ZZ ) )
7 zre 
 |-  ( N e. ZZ -> N e. RR )
8 nnrp 
 |-  ( M e. NN -> M e. RR+ )
9 mod0 
 |-  ( ( N e. RR /\ M e. RR+ ) -> ( ( N mod M ) = 0 <-> ( N / M ) e. ZZ ) )
10 7 8 9 syl2anr 
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( ( N mod M ) = 0 <-> ( N / M ) e. ZZ ) )
11 6 10 bitr4d 
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( M || N <-> ( N mod M ) = 0 ) )