Step | Hyp | Ref
| Expression |
1 | | rpcn 12984 |
. . . . 5
โข (๐ด โ โ+
โ ๐ด โ
โ) |
2 | 1 | 3ad2ant1 1134 |
. . . 4
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ ๐ด โ โ) |
3 | | recn 11200 |
. . . . 5
โข (๐ต โ โ โ ๐ต โ
โ) |
4 | 3 | 3ad2ant2 1135 |
. . . 4
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ ๐ต โ โ) |
5 | | rpre 12982 |
. . . . . . . 8
โข (๐ถ โ โ+
โ ๐ถ โ
โ) |
6 | 5 | adantl 483 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ถ โ โ+)
โ ๐ถ โ
โ) |
7 | | refldivcl 13788 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ถ โ โ+)
โ (โโ(๐ต /
๐ถ)) โ
โ) |
8 | 6, 7 | remulcld 11244 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ+)
โ (๐ถ ยท
(โโ(๐ต / ๐ถ))) โ
โ) |
9 | 8 | recnd 11242 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โ+)
โ (๐ถ ยท
(โโ(๐ต / ๐ถ))) โ
โ) |
10 | 9 | 3adant1 1131 |
. . . 4
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ (๐ถ ยท (โโ(๐ต / ๐ถ))) โ โ) |
11 | 2, 4, 10 | subdid 11670 |
. . 3
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ (๐ด ยท (๐ต โ (๐ถ ยท (โโ(๐ต / ๐ถ))))) = ((๐ด ยท ๐ต) โ (๐ด ยท (๐ถ ยท (โโ(๐ต / ๐ถ)))))) |
12 | | rpcnne0 12992 |
. . . . . . . . 9
โข (๐ถ โ โ+
โ (๐ถ โ โ
โง ๐ถ โ
0)) |
13 | 12 | 3ad2ant3 1136 |
. . . . . . . 8
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ (๐ถ โ โ โง ๐ถ โ 0)) |
14 | | rpcnne0 12992 |
. . . . . . . . 9
โข (๐ด โ โ+
โ (๐ด โ โ
โง ๐ด โ
0)) |
15 | 14 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ (๐ด โ โ โง ๐ด โ 0)) |
16 | | divcan5 11916 |
. . . . . . . 8
โข ((๐ต โ โ โง (๐ถ โ โ โง ๐ถ โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ ((๐ด ยท ๐ต) / (๐ด ยท ๐ถ)) = (๐ต / ๐ถ)) |
17 | 4, 13, 15, 16 | syl3anc 1372 |
. . . . . . 7
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ ((๐ด ยท ๐ต) / (๐ด ยท ๐ถ)) = (๐ต / ๐ถ)) |
18 | 17 | fveq2d 6896 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ (โโ((๐ด ยท ๐ต) / (๐ด ยท ๐ถ))) = (โโ(๐ต / ๐ถ))) |
19 | 18 | oveq2d 7425 |
. . . . 5
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ ((๐ด ยท ๐ถ) ยท (โโ((๐ด ยท ๐ต) / (๐ด ยท ๐ถ)))) = ((๐ด ยท ๐ถ) ยท (โโ(๐ต / ๐ถ)))) |
20 | | rpcn 12984 |
. . . . . . 7
โข (๐ถ โ โ+
โ ๐ถ โ
โ) |
21 | 20 | 3ad2ant3 1136 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ ๐ถ โ โ) |
22 | | rerpdivcl 13004 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ถ โ โ+)
โ (๐ต / ๐ถ) โ
โ) |
23 | | reflcl 13761 |
. . . . . . . . 9
โข ((๐ต / ๐ถ) โ โ โ
(โโ(๐ต / ๐ถ)) โ
โ) |
24 | 23 | recnd 11242 |
. . . . . . . 8
โข ((๐ต / ๐ถ) โ โ โ
(โโ(๐ต / ๐ถ)) โ
โ) |
25 | 22, 24 | syl 17 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ถ โ โ+)
โ (โโ(๐ต /
๐ถ)) โ
โ) |
26 | 25 | 3adant1 1131 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ (โโ(๐ต / ๐ถ)) โ โ) |
27 | 2, 21, 26 | mulassd 11237 |
. . . . 5
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ ((๐ด ยท ๐ถ) ยท (โโ(๐ต / ๐ถ))) = (๐ด ยท (๐ถ ยท (โโ(๐ต / ๐ถ))))) |
28 | 19, 27 | eqtr2d 2774 |
. . . 4
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ (๐ด ยท (๐ถ ยท (โโ(๐ต / ๐ถ)))) = ((๐ด ยท ๐ถ) ยท (โโ((๐ด ยท ๐ต) / (๐ด ยท ๐ถ))))) |
29 | 28 | oveq2d 7425 |
. . 3
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ ((๐ด ยท ๐ต) โ (๐ด ยท (๐ถ ยท (โโ(๐ต / ๐ถ))))) = ((๐ด ยท ๐ต) โ ((๐ด ยท ๐ถ) ยท (โโ((๐ด ยท ๐ต) / (๐ด ยท ๐ถ)))))) |
30 | 11, 29 | eqtrd 2773 |
. 2
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ (๐ด ยท (๐ต โ (๐ถ ยท (โโ(๐ต / ๐ถ))))) = ((๐ด ยท ๐ต) โ ((๐ด ยท ๐ถ) ยท (โโ((๐ด ยท ๐ต) / (๐ด ยท ๐ถ)))))) |
31 | | modval 13836 |
. . . 4
โข ((๐ต โ โ โง ๐ถ โ โ+)
โ (๐ต mod ๐ถ) = (๐ต โ (๐ถ ยท (โโ(๐ต / ๐ถ))))) |
32 | 31 | 3adant1 1131 |
. . 3
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ (๐ต mod ๐ถ) = (๐ต โ (๐ถ ยท (โโ(๐ต / ๐ถ))))) |
33 | 32 | oveq2d 7425 |
. 2
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ (๐ด ยท (๐ต mod ๐ถ)) = (๐ด ยท (๐ต โ (๐ถ ยท (โโ(๐ต / ๐ถ)))))) |
34 | | rpre 12982 |
. . . . 5
โข (๐ด โ โ+
โ ๐ด โ
โ) |
35 | | remulcl 11195 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
36 | 34, 35 | sylan 581 |
. . . 4
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ (๐ด ยท ๐ต) โ
โ) |
37 | 36 | 3adant3 1133 |
. . 3
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ (๐ด ยท ๐ต) โ โ) |
38 | | rpmulcl 12997 |
. . 3
โข ((๐ด โ โ+
โง ๐ถ โ
โ+) โ (๐ด ยท ๐ถ) โ
โ+) |
39 | | modval 13836 |
. . 3
โข (((๐ด ยท ๐ต) โ โ โง (๐ด ยท ๐ถ) โ โ+) โ ((๐ด ยท ๐ต) mod (๐ด ยท ๐ถ)) = ((๐ด ยท ๐ต) โ ((๐ด ยท ๐ถ) ยท (โโ((๐ด ยท ๐ต) / (๐ด ยท ๐ถ)))))) |
40 | 37, 38, 39 | 3imp3i2an 1346 |
. 2
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ ((๐ด ยท ๐ต) mod (๐ด ยท ๐ถ)) = ((๐ด ยท ๐ต) โ ((๐ด ยท ๐ถ) ยท (โโ((๐ด ยท ๐ต) / (๐ด ยท ๐ถ)))))) |
41 | 30, 33, 40 | 3eqtr4d 2783 |
1
โข ((๐ด โ โ+
โง ๐ต โ โ
โง ๐ถ โ
โ+) โ (๐ด ยท (๐ต mod ๐ถ)) = ((๐ด ยท ๐ต) mod (๐ด ยท ๐ถ))) |