Step | Hyp | Ref
| Expression |
1 | | simpll 527 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ๐ด โ
โ) |
2 | | zq 9626 |
. . . . . . 7
โข (๐ โ โค โ ๐ โ
โ) |
3 | 2 | ad2antlr 489 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ๐ โ
โ) |
4 | | simprl 529 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ๐ต โ
โ) |
5 | | qmulcl 9637 |
. . . . . 6
โข ((๐ โ โ โง ๐ต โ โ) โ (๐ ยท ๐ต) โ โ) |
6 | 3, 4, 5 | syl2anc 411 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ ยท ๐ต) โ โ) |
7 | | qaddcl 9635 |
. . . . 5
โข ((๐ด โ โ โง (๐ ยท ๐ต) โ โ) โ (๐ด + (๐ ยท ๐ต)) โ โ) |
8 | 1, 6, 7 | syl2anc 411 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ด + (๐ ยท ๐ต)) โ โ) |
9 | | simprr 531 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ 0 < ๐ต) |
10 | | modqval 10324 |
. . . 4
โข (((๐ด + (๐ ยท ๐ต)) โ โ โง ๐ต โ โ โง 0 < ๐ต) โ ((๐ด + (๐ ยท ๐ต)) mod ๐ต) = ((๐ด + (๐ ยท ๐ต)) โ (๐ต ยท (โโ((๐ด + (๐ ยท ๐ต)) / ๐ต))))) |
11 | 8, 4, 9, 10 | syl3anc 1238 |
. . 3
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ((๐ด + (๐ ยท ๐ต)) mod ๐ต) = ((๐ด + (๐ ยท ๐ต)) โ (๐ต ยท (โโ((๐ด + (๐ ยท ๐ต)) / ๐ต))))) |
12 | | qcn 9634 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ๐ด โ
โ) |
13 | 1, 12 | syl 14 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ๐ด โ
โ) |
14 | | qcn 9634 |
. . . . . . . . . . 11
โข ((๐ ยท ๐ต) โ โ โ (๐ ยท ๐ต) โ โ) |
15 | 6, 14 | syl 14 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ ยท ๐ต) โ โ) |
16 | | qcn 9634 |
. . . . . . . . . . 11
โข (๐ต โ โ โ ๐ต โ
โ) |
17 | 4, 16 | syl 14 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ๐ต โ
โ) |
18 | | qre 9625 |
. . . . . . . . . . . 12
โข (๐ต โ โ โ ๐ต โ
โ) |
19 | 4, 18 | syl 14 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ๐ต โ
โ) |
20 | 19, 9 | gt0ap0d 8586 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ๐ต # 0) |
21 | 13, 15, 17, 20 | divdirapd 8786 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ((๐ด + (๐ ยท ๐ต)) / ๐ต) = ((๐ด / ๐ต) + ((๐ ยท ๐ต) / ๐ต))) |
22 | | simplr 528 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ๐ โ
โค) |
23 | 22 | zcnd 9376 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ๐ โ
โ) |
24 | 23, 17, 20 | divcanap4d 8753 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ((๐ ยท ๐ต) / ๐ต) = ๐) |
25 | 24 | oveq2d 5891 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ((๐ด / ๐ต) + ((๐ ยท ๐ต) / ๐ต)) = ((๐ด / ๐ต) + ๐)) |
26 | 21, 25 | eqtrd 2210 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ((๐ด + (๐ ยท ๐ต)) / ๐ต) = ((๐ด / ๐ต) + ๐)) |
27 | 26 | fveq2d 5520 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ
(โโ((๐ด + (๐ ยท ๐ต)) / ๐ต)) = (โโ((๐ด / ๐ต) + ๐))) |
28 | 9 | gt0ne0d 8469 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ๐ต โ 0) |
29 | | qdivcl 9643 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด / ๐ต) โ โ) |
30 | 1, 4, 28, 29 | syl3anc 1238 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ด / ๐ต) โ โ) |
31 | | flqaddz 10297 |
. . . . . . . 8
โข (((๐ด / ๐ต) โ โ โง ๐ โ โค) โ
(โโ((๐ด / ๐ต) + ๐)) = ((โโ(๐ด / ๐ต)) + ๐)) |
32 | 30, 22, 31 | syl2anc 411 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ
(โโ((๐ด / ๐ต) + ๐)) = ((โโ(๐ด / ๐ต)) + ๐)) |
33 | 27, 32 | eqtrd 2210 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ
(โโ((๐ด + (๐ ยท ๐ต)) / ๐ต)) = ((โโ(๐ด / ๐ต)) + ๐)) |
34 | 33 | oveq2d 5891 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ต ยท (โโ((๐ด + (๐ ยท ๐ต)) / ๐ต))) = (๐ต ยท ((โโ(๐ด / ๐ต)) + ๐))) |
35 | 30 | flqcld 10277 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ
(โโ(๐ด / ๐ต)) โ
โค) |
36 | 35 | zcnd 9376 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ
(โโ(๐ด / ๐ต)) โ
โ) |
37 | 17, 36, 23 | adddid 7982 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ต ยท ((โโ(๐ด / ๐ต)) + ๐)) = ((๐ต ยท (โโ(๐ด / ๐ต))) + (๐ต ยท ๐))) |
38 | 17, 23 | mulcomd 7979 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ต ยท ๐) = (๐ ยท ๐ต)) |
39 | 38 | oveq2d 5891 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ((๐ต ยท (โโ(๐ด / ๐ต))) + (๐ต ยท ๐)) = ((๐ต ยท (โโ(๐ด / ๐ต))) + (๐ ยท ๐ต))) |
40 | 34, 37, 39 | 3eqtrd 2214 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ต ยท (โโ((๐ด + (๐ ยท ๐ต)) / ๐ต))) = ((๐ต ยท (โโ(๐ด / ๐ต))) + (๐ ยท ๐ต))) |
41 | 40 | oveq2d 5891 |
. . 3
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ((๐ด + (๐ ยท ๐ต)) โ (๐ต ยท (โโ((๐ด + (๐ ยท ๐ต)) / ๐ต)))) = ((๐ด + (๐ ยท ๐ต)) โ ((๐ต ยท (โโ(๐ด / ๐ต))) + (๐ ยท ๐ต)))) |
42 | 17, 36 | mulcld 7978 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ต ยท (โโ(๐ด / ๐ต))) โ โ) |
43 | 13, 42, 15 | pnpcan2d 8306 |
. . 3
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ((๐ด + (๐ ยท ๐ต)) โ ((๐ต ยท (โโ(๐ด / ๐ต))) + (๐ ยท ๐ต))) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
44 | 11, 41, 43 | 3eqtrd 2214 |
. 2
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ((๐ด + (๐ ยท ๐ต)) mod ๐ต) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
45 | | modqval 10324 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โ (๐ด mod ๐ต) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
46 | 1, 4, 9, 45 | syl3anc 1238 |
. 2
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ด mod ๐ต) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
47 | 44, 46 | eqtr4d 2213 |
1
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ต โ โ โง 0 <
๐ต)) โ ((๐ด + (๐ ยท ๐ต)) mod ๐ต) = (๐ด mod ๐ต)) |