Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  modmulconst Unicode version

Theorem modmulconst 10139
 Description: Constant multiplication in a modulo operation, see theorem 5.3 in [ApostolNT] p. 108. (Contributed by AV, 21-Jul-2021.)
Assertion
Ref Expression
modmulconst

Proof of Theorem modmulconst
StepHypRef Expression
1 nnz 8321 . . . . 5
21adantl 266 . . . 4
3 zsubcl 8343 . . . . . 6
433adant3 935 . . . . 5
54adantr 265 . . . 4
6 nnz 8321 . . . . . . 7
7 nnne0 8018 . . . . . . 7
86, 7jca 294 . . . . . 6
983ad2ant3 938 . . . . 5
109adantr 265 . . . 4
11 dvdscmulr 10136 . . . . 5
1211bicomd 133 . . . 4
132, 5, 10, 12syl3anc 1146 . . 3
14 zcn 8307 . . . . . . . 8
15 zcn 8307 . . . . . . . 8
16 nncn 7998 . . . . . . . 8
1714, 15, 163anim123i 1100 . . . . . . 7
18 3anrot 901 . . . . . . 7
1917, 18sylibr 141 . . . . . 6
20 subdi 7454 . . . . . 6
2119, 20syl 14 . . . . 5
2221adantr 265 . . . 4
2322breq2d 3804 . . 3
2413, 23bitrd 181 . 2
25 simpr 107 . . 3
26 simp1 915 . . . 4
28 simp2 916 . . . 4
30 moddvds 10117 . . 3
3125, 27, 29, 30syl3anc 1146 . 2
32 simpl3 920 . . . 4
3332, 25nnmulcld 8038 . . 3
3463ad2ant3 938 . . . . 5
3534, 26zmulcld 8425 . . . 4