Metamath Proof Explorer

Theorem divalgmodcl

Description: The result of the mod operator satisfies the requirements for the remainder R in the division algorithm for a positive divisor. Variant of divalgmod . (Contributed by Stefan O'Rear, 17-Oct-2014) (Proof shortened by AV, 21-Aug-2021)

		Ref	Expression
	Assertion	divalgmodcl	\|- ( ( N e. ZZ /\ D e. NN /\ R e. NN0 ) -> ( R = ( N mod D ) <-> ( R < D /\ D \|\| ( N - R ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		divalgmod	\|- ( ( N e. ZZ /\ D e. NN ) -> ( R = ( N mod D ) <-> ( R e. NN0 /\ ( R < D /\ D \|\| ( N - R ) ) ) ) )
2	1	baibd	\|- ( ( ( N e. ZZ /\ D e. NN ) /\ R e. NN0 ) -> ( R = ( N mod D ) <-> ( R < D /\ D \|\| ( N - R ) ) ) )
3	2	3impa	\|- ( ( N e. ZZ /\ D e. NN /\ R e. NN0 ) -> ( R = ( N mod D ) <-> ( R < D /\ D \|\| ( N - R ) ) ) )

Step

Hyp

Ref

Expression

divalgmod

 |-  ( ( N e. ZZ /\ D e. NN ) -> ( R = ( N mod D ) <-> ( R e. NN0 /\ ( R < D /\ D || ( N - R ) ) ) ) )

baibd

 |-  ( ( ( N e. ZZ /\ D e. NN ) /\ R e. NN0 ) -> ( R = ( N mod D ) <-> ( R < D /\ D || ( N - R ) ) ) )

3impa

 |-  ( ( N e. ZZ /\ D e. NN /\ R e. NN0 ) -> ( R = ( N mod D ) <-> ( R < D /\ D || ( N - R ) ) ) )