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 ) )