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

Metamath Proof Explorer

Theorem modmulconst

Description: Constant multiplication in a modulo operation, see theorem 5.3 in ApostolNT p. 108. (Contributed by AV, 21-Jul-2021)

Ref Expression
Assertion modmulconst 
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( ( A mod M ) = ( B mod M ) <-> ( ( C x. A ) mod ( C x. M ) ) = ( ( C x. B ) mod ( C x. M ) ) ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( M e. NN -> M e. ZZ )
2 1 adantl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> M e. ZZ )
3 zsubcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A - B ) e. ZZ )
4 3 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( A - B ) e. ZZ )
5 4 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( A - B ) e. ZZ )
6 nnz 
 |-  ( C e. NN -> C e. ZZ )
7 nnne0 
 |-  ( C e. NN -> C =/= 0 )
8 6 7 jca 
 |-  ( C e. NN -> ( C e. ZZ /\ C =/= 0 ) )
9 8 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( C e. ZZ /\ C =/= 0 ) )
10 9 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( C e. ZZ /\ C =/= 0 ) )
11 dvdscmulr 
 |-  ( ( M e. ZZ /\ ( A - B ) e. ZZ /\ ( C e. ZZ /\ C =/= 0 ) ) -> ( ( C x. M ) || ( C x. ( A - B ) ) <-> M || ( A - B ) ) )
12 11 bicomd 
 |-  ( ( M e. ZZ /\ ( A - B ) e. ZZ /\ ( C e. ZZ /\ C =/= 0 ) ) -> ( M || ( A - B ) <-> ( C x. M ) || ( C x. ( A - B ) ) ) )
13 2 5 10 12 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( M || ( A - B ) <-> ( C x. M ) || ( C x. ( A - B ) ) ) )
14 zcn 
 |-  ( A e. ZZ -> A e. CC )
15 zcn 
 |-  ( B e. ZZ -> B e. CC )
16 nncn 
 |-  ( C e. NN -> C e. CC )
17 14 15 16 3anim123i 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( A e. CC /\ B e. CC /\ C e. CC ) )
18 3anrot 
 |-  ( ( C e. CC /\ A e. CC /\ B e. CC ) <-> ( A e. CC /\ B e. CC /\ C e. CC ) )
19 17 18 sylibr 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( C e. CC /\ A e. CC /\ B e. CC ) )
20 subdi 
 |-  ( ( C e. CC /\ A e. CC /\ B e. CC ) -> ( C x. ( A - B ) ) = ( ( C x. A ) - ( C x. B ) ) )
21 19 20 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( C x. ( A - B ) ) = ( ( C x. A ) - ( C x. B ) ) )
22 21 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( C x. ( A - B ) ) = ( ( C x. A ) - ( C x. B ) ) )
23 22 breq2d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( ( C x. M ) || ( C x. ( A - B ) ) <-> ( C x. M ) || ( ( C x. A ) - ( C x. B ) ) ) )
24 13 23 bitrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( M || ( A - B ) <-> ( C x. M ) || ( ( C x. A ) - ( C x. B ) ) ) )
25 simpr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> M e. NN )
26 simp1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> A e. ZZ )
27 26 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> A e. ZZ )
28 simp2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> B e. ZZ )
29 28 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> B e. ZZ )
30 moddvds 
 |-  ( ( M e. NN /\ A e. ZZ /\ B e. ZZ ) -> ( ( A mod M ) = ( B mod M ) <-> M || ( A - B ) ) )
31 25 27 29 30 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( ( A mod M ) = ( B mod M ) <-> M || ( A - B ) ) )
32 simpl3 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> C e. NN )
33 32 25 nnmulcld 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( C x. M ) e. NN )
34 6 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> C e. ZZ )
35 34 26 zmulcld 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( C x. A ) e. ZZ )
36 35 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( C x. A ) e. ZZ )
37 34 28 zmulcld 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( C x. B ) e. ZZ )
38 37 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( C x. B ) e. ZZ )
39 moddvds 
 |-  ( ( ( C x. M ) e. NN /\ ( C x. A ) e. ZZ /\ ( C x. B ) e. ZZ ) -> ( ( ( C x. A ) mod ( C x. M ) ) = ( ( C x. B ) mod ( C x. M ) ) <-> ( C x. M ) || ( ( C x. A ) - ( C x. B ) ) ) )
40 33 36 38 39 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( ( ( C x. A ) mod ( C x. M ) ) = ( ( C x. B ) mod ( C x. M ) ) <-> ( C x. M ) || ( ( C x. A ) - ( C x. B ) ) ) )
41 24 31 40 3bitr4d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( ( A mod M ) = ( B mod M ) <-> ( ( C x. A ) mod ( C x. M ) ) = ( ( C x. B ) mod ( C x. M ) ) ) )