Step | Hyp | Ref
| Expression |
1 | | modqmul1.ab |
. 2
โข (๐ โ (๐ด mod ๐ท) = (๐ต mod ๐ท)) |
2 | | modqmul1.a |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
3 | | modqmul1.d |
. . . . . . 7
โข (๐ โ ๐ท โ โ) |
4 | | modqmul1.dgt0 |
. . . . . . 7
โข (๐ โ 0 < ๐ท) |
5 | | modqval 10323 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ท โ โ โง 0 <
๐ท) โ (๐ด mod ๐ท) = (๐ด โ (๐ท ยท (โโ(๐ด / ๐ท))))) |
6 | 2, 3, 4, 5 | syl3anc 1238 |
. . . . . 6
โข (๐ โ (๐ด mod ๐ท) = (๐ด โ (๐ท ยท (โโ(๐ด / ๐ท))))) |
7 | | modqmul1.b |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
8 | | modqval 10323 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ท โ โ โง 0 <
๐ท) โ (๐ต mod ๐ท) = (๐ต โ (๐ท ยท (โโ(๐ต / ๐ท))))) |
9 | 7, 3, 4, 8 | syl3anc 1238 |
. . . . . 6
โข (๐ โ (๐ต mod ๐ท) = (๐ต โ (๐ท ยท (โโ(๐ต / ๐ท))))) |
10 | 6, 9 | eqeq12d 2192 |
. . . . 5
โข (๐ โ ((๐ด mod ๐ท) = (๐ต mod ๐ท) โ (๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) = (๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))))) |
11 | | oveq1 5881 |
. . . . 5
โข ((๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) = (๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))) โ ((๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) ยท ๐ถ) = ((๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))) ยท ๐ถ)) |
12 | 10, 11 | syl6bi 163 |
. . . 4
โข (๐ โ ((๐ด mod ๐ท) = (๐ต mod ๐ท) โ ((๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) ยท ๐ถ) = ((๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))) ยท ๐ถ))) |
13 | | qcn 9633 |
. . . . . . . . . 10
โข (๐ท โ โ โ ๐ท โ
โ) |
14 | 3, 13 | syl 14 |
. . . . . . . . 9
โข (๐ โ ๐ท โ โ) |
15 | | modqmul1.c |
. . . . . . . . . 10
โข (๐ โ ๐ถ โ โค) |
16 | 15 | zcnd 9375 |
. . . . . . . . 9
โข (๐ โ ๐ถ โ โ) |
17 | 4 | gt0ne0d 8468 |
. . . . . . . . . . . 12
โข (๐ โ ๐ท โ 0) |
18 | | qdivcl 9642 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ท โ โ โง ๐ท โ 0) โ (๐ด / ๐ท) โ โ) |
19 | 2, 3, 17, 18 | syl3anc 1238 |
. . . . . . . . . . 11
โข (๐ โ (๐ด / ๐ท) โ โ) |
20 | 19 | flqcld 10276 |
. . . . . . . . . 10
โข (๐ โ (โโ(๐ด / ๐ท)) โ โค) |
21 | 20 | zcnd 9375 |
. . . . . . . . 9
โข (๐ โ (โโ(๐ด / ๐ท)) โ โ) |
22 | 14, 16, 21 | mulassd 7980 |
. . . . . . . 8
โข (๐ โ ((๐ท ยท ๐ถ) ยท (โโ(๐ด / ๐ท))) = (๐ท ยท (๐ถ ยท (โโ(๐ด / ๐ท))))) |
23 | 14, 16, 21 | mul32d 8109 |
. . . . . . . 8
โข (๐ โ ((๐ท ยท ๐ถ) ยท (โโ(๐ด / ๐ท))) = ((๐ท ยท (โโ(๐ด / ๐ท))) ยท ๐ถ)) |
24 | 22, 23 | eqtr3d 2212 |
. . . . . . 7
โข (๐ โ (๐ท ยท (๐ถ ยท (โโ(๐ด / ๐ท)))) = ((๐ท ยท (โโ(๐ด / ๐ท))) ยท ๐ถ)) |
25 | 24 | oveq2d 5890 |
. . . . . 6
โข (๐ โ ((๐ด ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ด / ๐ท))))) = ((๐ด ยท ๐ถ) โ ((๐ท ยท (โโ(๐ด / ๐ท))) ยท ๐ถ))) |
26 | | qcn 9633 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ
โ) |
27 | 2, 26 | syl 14 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
28 | 14, 21 | mulcld 7977 |
. . . . . . 7
โข (๐ โ (๐ท ยท (โโ(๐ด / ๐ท))) โ โ) |
29 | 27, 28, 16 | subdird 8371 |
. . . . . 6
โข (๐ โ ((๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) ยท ๐ถ) = ((๐ด ยท ๐ถ) โ ((๐ท ยท (โโ(๐ด / ๐ท))) ยท ๐ถ))) |
30 | 25, 29 | eqtr4d 2213 |
. . . . 5
โข (๐ โ ((๐ด ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ด / ๐ท))))) = ((๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) ยท ๐ถ)) |
31 | | qdivcl 9642 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง ๐ท โ โ โง ๐ท โ 0) โ (๐ต / ๐ท) โ โ) |
32 | 7, 3, 17, 31 | syl3anc 1238 |
. . . . . . . . . . 11
โข (๐ โ (๐ต / ๐ท) โ โ) |
33 | 32 | flqcld 10276 |
. . . . . . . . . 10
โข (๐ โ (โโ(๐ต / ๐ท)) โ โค) |
34 | 33 | zcnd 9375 |
. . . . . . . . 9
โข (๐ โ (โโ(๐ต / ๐ท)) โ โ) |
35 | 14, 16, 34 | mulassd 7980 |
. . . . . . . 8
โข (๐ โ ((๐ท ยท ๐ถ) ยท (โโ(๐ต / ๐ท))) = (๐ท ยท (๐ถ ยท (โโ(๐ต / ๐ท))))) |
36 | 14, 16, 34 | mul32d 8109 |
. . . . . . . 8
โข (๐ โ ((๐ท ยท ๐ถ) ยท (โโ(๐ต / ๐ท))) = ((๐ท ยท (โโ(๐ต / ๐ท))) ยท ๐ถ)) |
37 | 35, 36 | eqtr3d 2212 |
. . . . . . 7
โข (๐ โ (๐ท ยท (๐ถ ยท (โโ(๐ต / ๐ท)))) = ((๐ท ยท (โโ(๐ต / ๐ท))) ยท ๐ถ)) |
38 | 37 | oveq2d 5890 |
. . . . . 6
โข (๐ โ ((๐ต ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ต / ๐ท))))) = ((๐ต ยท ๐ถ) โ ((๐ท ยท (โโ(๐ต / ๐ท))) ยท ๐ถ))) |
39 | | qcn 9633 |
. . . . . . . 8
โข (๐ต โ โ โ ๐ต โ
โ) |
40 | 7, 39 | syl 14 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
41 | 14, 34 | mulcld 7977 |
. . . . . . 7
โข (๐ โ (๐ท ยท (โโ(๐ต / ๐ท))) โ โ) |
42 | 40, 41, 16 | subdird 8371 |
. . . . . 6
โข (๐ โ ((๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))) ยท ๐ถ) = ((๐ต ยท ๐ถ) โ ((๐ท ยท (โโ(๐ต / ๐ท))) ยท ๐ถ))) |
43 | 38, 42 | eqtr4d 2213 |
. . . . 5
โข (๐ โ ((๐ต ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ต / ๐ท))))) = ((๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))) ยท ๐ถ)) |
44 | 30, 43 | eqeq12d 2192 |
. . . 4
โข (๐ โ (((๐ด ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ด / ๐ท))))) = ((๐ต ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ต / ๐ท))))) โ ((๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) ยท ๐ถ) = ((๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))) ยท ๐ถ))) |
45 | 12, 44 | sylibrd 169 |
. . 3
โข (๐ โ ((๐ด mod ๐ท) = (๐ต mod ๐ท) โ ((๐ด ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ด / ๐ท))))) = ((๐ต ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ต / ๐ท))))))) |
46 | | oveq1 5881 |
. . . 4
โข (((๐ด ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ด / ๐ท))))) = ((๐ต ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ต / ๐ท))))) โ (((๐ด ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ด / ๐ท))))) mod ๐ท) = (((๐ต ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ต / ๐ท))))) mod ๐ท)) |
47 | | zq 9625 |
. . . . . . . 8
โข (๐ถ โ โค โ ๐ถ โ
โ) |
48 | 15, 47 | syl 14 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
49 | | qmulcl 9636 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด ยท ๐ถ) โ โ) |
50 | 2, 48, 49 | syl2anc 411 |
. . . . . 6
โข (๐ โ (๐ด ยท ๐ถ) โ โ) |
51 | 15, 20 | zmulcld 9380 |
. . . . . 6
โข (๐ โ (๐ถ ยท (โโ(๐ด / ๐ท))) โ โค) |
52 | | modqcyc2 10359 |
. . . . . 6
โข ((((๐ด ยท ๐ถ) โ โ โง (๐ถ ยท (โโ(๐ด / ๐ท))) โ โค) โง (๐ท โ โ โง 0 < ๐ท)) โ (((๐ด ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ด / ๐ท))))) mod ๐ท) = ((๐ด ยท ๐ถ) mod ๐ท)) |
53 | 50, 51, 3, 4, 52 | syl22anc 1239 |
. . . . 5
โข (๐ โ (((๐ด ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ด / ๐ท))))) mod ๐ท) = ((๐ด ยท ๐ถ) mod ๐ท)) |
54 | | qmulcl 9636 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยท ๐ถ) โ โ) |
55 | 7, 48, 54 | syl2anc 411 |
. . . . . 6
โข (๐ โ (๐ต ยท ๐ถ) โ โ) |
56 | 15, 33 | zmulcld 9380 |
. . . . . 6
โข (๐ โ (๐ถ ยท (โโ(๐ต / ๐ท))) โ โค) |
57 | | modqcyc2 10359 |
. . . . . 6
โข ((((๐ต ยท ๐ถ) โ โ โง (๐ถ ยท (โโ(๐ต / ๐ท))) โ โค) โง (๐ท โ โ โง 0 < ๐ท)) โ (((๐ต ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ต / ๐ท))))) mod ๐ท) = ((๐ต ยท ๐ถ) mod ๐ท)) |
58 | 55, 56, 3, 4, 57 | syl22anc 1239 |
. . . . 5
โข (๐ โ (((๐ต ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ต / ๐ท))))) mod ๐ท) = ((๐ต ยท ๐ถ) mod ๐ท)) |
59 | 53, 58 | eqeq12d 2192 |
. . . 4
โข (๐ โ ((((๐ด ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ด / ๐ท))))) mod ๐ท) = (((๐ต ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ต / ๐ท))))) mod ๐ท) โ ((๐ด ยท ๐ถ) mod ๐ท) = ((๐ต ยท ๐ถ) mod ๐ท))) |
60 | 46, 59 | imbitrid 154 |
. . 3
โข (๐ โ (((๐ด ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ด / ๐ท))))) = ((๐ต ยท ๐ถ) โ (๐ท ยท (๐ถ ยท (โโ(๐ต / ๐ท))))) โ ((๐ด ยท ๐ถ) mod ๐ท) = ((๐ต ยท ๐ถ) mod ๐ท))) |
61 | 45, 60 | syld 45 |
. 2
โข (๐ โ ((๐ด mod ๐ท) = (๐ต mod ๐ท) โ ((๐ด ยท ๐ถ) mod ๐ท) = ((๐ต ยท ๐ถ) mod ๐ท))) |
62 | 1, 61 | mpd 13 |
1
โข (๐ โ ((๐ด ยท ๐ถ) mod ๐ท) = ((๐ต ยท ๐ถ) mod ๐ท)) |