Metamath Proof Explorer

Theorem modremain

Description: The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021)

Ref Expression
Assertion modremain 
|- ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> ( ( N mod D ) = R <-> E. z e. ZZ ( ( z x. D ) + R ) = N ) )

Proof

Step Hyp Ref Expression
1 eqcom 
 |-  ( ( N mod D ) = R <-> R = ( N mod D ) )
2 divalgmodcl 
 |-  ( ( N e. ZZ /\ D e. NN /\ R e. NN0 ) -> ( R = ( N mod D ) <-> ( R < D /\ D || ( N - R ) ) ) )
3 2 3adant3r 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> ( R = ( N mod D ) <-> ( R < D /\ D || ( N - R ) ) ) )
4 ibar 
 |-  ( R < D -> ( D || ( N - R ) <-> ( R < D /\ D || ( N - R ) ) ) )
5 4 adantl 
 |-  ( ( R e. NN0 /\ R < D ) -> ( D || ( N - R ) <-> ( R < D /\ D || ( N - R ) ) ) )
6 5 3ad2ant3 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> ( D || ( N - R ) <-> ( R < D /\ D || ( N - R ) ) ) )
7 nnz 
 |-  ( D e. NN -> D e. ZZ )
8 7 3ad2ant2 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> D e. ZZ )
9 simp1 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> N e. ZZ )
10 nn0z 
 |-  ( R e. NN0 -> R e. ZZ )
11 10 adantr 
 |-  ( ( R e. NN0 /\ R < D ) -> R e. ZZ )
12 11 3ad2ant3 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> R e. ZZ )
13 9 12 zsubcld 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> ( N - R ) e. ZZ )
14 divides 
 |-  ( ( D e. ZZ /\ ( N - R ) e. ZZ ) -> ( D || ( N - R ) <-> E. z e. ZZ ( z x. D ) = ( N - R ) ) )
15 8 13 14 syl2anc 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> ( D || ( N - R ) <-> E. z e. ZZ ( z x. D ) = ( N - R ) ) )
16 eqcom 
 |-  ( ( z x. D ) = ( N - R ) <-> ( N - R ) = ( z x. D ) )
17 zcn 
 |-  ( N e. ZZ -> N e. CC )
18 17 3ad2ant1 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> N e. CC )
19 18 adantr 
 |-  ( ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) /\ z e. ZZ ) -> N e. CC )
20 nn0cn 
 |-  ( R e. NN0 -> R e. CC )
21 20 adantr 
 |-  ( ( R e. NN0 /\ R < D ) -> R e. CC )
22 21 3ad2ant3 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> R e. CC )
23 22 adantr 
 |-  ( ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) /\ z e. ZZ ) -> R e. CC )
24 simpr 
 |-  ( ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) /\ z e. ZZ ) -> z e. ZZ )
25 8 adantr 
 |-  ( ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) /\ z e. ZZ ) -> D e. ZZ )
26 24 25 zmulcld 
 |-  ( ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) /\ z e. ZZ ) -> ( z x. D ) e. ZZ )
27 26 zcnd 
 |-  ( ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) /\ z e. ZZ ) -> ( z x. D ) e. CC )
28 19 23 27 subadd2d 
 |-  ( ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) /\ z e. ZZ ) -> ( ( N - R ) = ( z x. D ) <-> ( ( z x. D ) + R ) = N ) )
29 16 28 syl5bb 
 |-  ( ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) /\ z e. ZZ ) -> ( ( z x. D ) = ( N - R ) <-> ( ( z x. D ) + R ) = N ) )
30 29 rexbidva 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> ( E. z e. ZZ ( z x. D ) = ( N - R ) <-> E. z e. ZZ ( ( z x. D ) + R ) = N ) )
31 15 30 bitrd 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> ( D || ( N - R ) <-> E. z e. ZZ ( ( z x. D ) + R ) = N ) )
32 3 6 31 3bitr2d 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> ( R = ( N mod D ) <-> E. z e. ZZ ( ( z x. D ) + R ) = N ) )
33 1 32 syl5bb 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> ( ( N mod D ) = R <-> E. z e. ZZ ( ( z x. D ) + R ) = N ) )