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 ABCMAmodM=BmodMCAmodC M=CBmodC M

Proof

Step Hyp Ref Expression
1 nnz MM
2 1 adantl ABCMM
3 zsubcl ABAB
4 3 3adant3 ABCAB
5 4 adantr ABCMAB
6 nnz CC
7 nnne0 CC0
8 6 7 jca CCC0
9 8 3ad2ant3 ABCCC0
10 9 adantr ABCMCC0
11 dvdscmulr MABCC0C MCABMAB
12 11 bicomd MABCC0MABC MCAB
13 2 5 10 12 syl3anc ABCMMABC MCAB
14 zcn AA
15 zcn BB
16 nncn CC
17 14 15 16 3anim123i ABCABC
18 3anrot CABABC
19 17 18 sylibr ABCCAB
20 subdi CABCAB=CACB
21 19 20 syl ABCCAB=CACB
22 21 adantr ABCMCAB=CACB
23 22 breq2d ABCMC MCABC MCACB
24 13 23 bitrd ABCMMABC MCACB
25 simpr ABCMM
26 simp1 ABCA
27 26 adantr ABCMA
28 simp2 ABCB
29 28 adantr ABCMB
30 moddvds MABAmodM=BmodMMAB
31 25 27 29 30 syl3anc ABCMAmodM=BmodMMAB
32 simpl3 ABCMC
33 32 25 nnmulcld ABCMC M
34 6 3ad2ant3 ABCC
35 34 26 zmulcld ABCCA
36 35 adantr ABCMCA
37 34 28 zmulcld ABCCB
38 37 adantr ABCMCB
39 moddvds C MCACBCAmodC M=CBmodC MC MCACB
40 33 36 38 39 syl3anc ABCMCAmodC M=CBmodC MC MCACB
41 24 31 40 3bitr4d ABCMAmodM=BmodMCAmodC M=CBmodC M