Step | Hyp | Ref
| Expression |
1 | | zre 12562 |
. . . . . . . 8
โข (๐ โ โค โ ๐ โ
โ) |
2 | | rpre 12982 |
. . . . . . . 8
โข (๐ต โ โ+
โ ๐ต โ
โ) |
3 | | remulcl 11195 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ต โ โ) โ (๐ ยท ๐ต) โ โ) |
4 | 1, 2, 3 | syl2an 597 |
. . . . . . 7
โข ((๐ โ โค โง ๐ต โ โ+)
โ (๐ ยท ๐ต) โ
โ) |
5 | | readdcl 11193 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ ยท ๐ต) โ โ) โ (๐ด + (๐ ยท ๐ต)) โ โ) |
6 | 4, 5 | sylan2 594 |
. . . . . 6
โข ((๐ด โ โ โง (๐ โ โค โง ๐ต โ โ+))
โ (๐ด + (๐ ยท ๐ต)) โ โ) |
7 | 6 | 3impb 1116 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (๐ด + (๐ ยท ๐ต)) โ โ) |
8 | | simp3 1139 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ๐ต โ
โ+) |
9 | | modval 13836 |
. . . . 5
โข (((๐ด + (๐ ยท ๐ต)) โ โ โง ๐ต โ โ+) โ ((๐ด + (๐ ยท ๐ต)) mod ๐ต) = ((๐ด + (๐ ยท ๐ต)) โ (๐ต ยท (โโ((๐ด + (๐ ยท ๐ต)) / ๐ต))))) |
10 | 7, 8, 9 | syl2anc 585 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ((๐ด + (๐ ยท ๐ต)) mod ๐ต) = ((๐ด + (๐ ยท ๐ต)) โ (๐ต ยท (โโ((๐ด + (๐ ยท ๐ต)) / ๐ต))))) |
11 | | recn 11200 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ ๐ด โ
โ) |
12 | 11 | 3ad2ant1 1134 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ๐ด โ
โ) |
13 | 4 | recnd 11242 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ต โ โ+)
โ (๐ ยท ๐ต) โ
โ) |
14 | 13 | 3adant1 1131 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (๐ ยท ๐ต) โ
โ) |
15 | | rpcnne0 12992 |
. . . . . . . . . . . 12
โข (๐ต โ โ+
โ (๐ต โ โ
โง ๐ต โ
0)) |
16 | 15 | 3ad2ant3 1136 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (๐ต โ โ
โง ๐ต โ
0)) |
17 | | divdir 11897 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง (๐ ยท ๐ต) โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ด + (๐ ยท ๐ต)) / ๐ต) = ((๐ด / ๐ต) + ((๐ ยท ๐ต) / ๐ต))) |
18 | 12, 14, 16, 17 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ((๐ด + (๐ ยท ๐ต)) / ๐ต) = ((๐ด / ๐ต) + ((๐ ยท ๐ต) / ๐ต))) |
19 | | zcn 12563 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ๐ โ
โ) |
20 | | divcan4 11899 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ((๐ ยท ๐ต) / ๐ต) = ๐) |
21 | 20 | 3expb 1121 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ ยท ๐ต) / ๐ต) = ๐) |
22 | 19, 15, 21 | syl2an 597 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ต โ โ+)
โ ((๐ ยท ๐ต) / ๐ต) = ๐) |
23 | 22 | 3adant1 1131 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ((๐ ยท ๐ต) / ๐ต) = ๐) |
24 | 23 | oveq2d 7425 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ((๐ด / ๐ต) + ((๐ ยท ๐ต) / ๐ต)) = ((๐ด / ๐ต) + ๐)) |
25 | 18, 24 | eqtrd 2773 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ((๐ด + (๐ ยท ๐ต)) / ๐ต) = ((๐ด / ๐ต) + ๐)) |
26 | 25 | fveq2d 6896 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (โโ((๐ด +
(๐ ยท ๐ต)) / ๐ต)) = (โโ((๐ด / ๐ต) + ๐))) |
27 | | rerpdivcl 13004 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (๐ด / ๐ต) โ
โ) |
28 | 27 | 3adant2 1132 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (๐ด / ๐ต) โ
โ) |
29 | | simp2 1138 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ๐ โ
โค) |
30 | | fladdz 13790 |
. . . . . . . . 9
โข (((๐ด / ๐ต) โ โ โง ๐ โ โค) โ
(โโ((๐ด / ๐ต) + ๐)) = ((โโ(๐ด / ๐ต)) + ๐)) |
31 | 28, 29, 30 | syl2anc 585 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (โโ((๐ด /
๐ต) + ๐)) = ((โโ(๐ด / ๐ต)) + ๐)) |
32 | 26, 31 | eqtrd 2773 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (โโ((๐ด +
(๐ ยท ๐ต)) / ๐ต)) = ((โโ(๐ด / ๐ต)) + ๐)) |
33 | 32 | oveq2d 7425 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (๐ต ยท
(โโ((๐ด + (๐ ยท ๐ต)) / ๐ต))) = (๐ต ยท ((โโ(๐ด / ๐ต)) + ๐))) |
34 | | rpcn 12984 |
. . . . . . . 8
โข (๐ต โ โ+
โ ๐ต โ
โ) |
35 | 34 | 3ad2ant3 1136 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ๐ต โ
โ) |
36 | | reflcl 13761 |
. . . . . . . . . 10
โข ((๐ด / ๐ต) โ โ โ
(โโ(๐ด / ๐ต)) โ
โ) |
37 | 36 | recnd 11242 |
. . . . . . . . 9
โข ((๐ด / ๐ต) โ โ โ
(โโ(๐ด / ๐ต)) โ
โ) |
38 | 27, 37 | syl 17 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (โโ(๐ด /
๐ต)) โ
โ) |
39 | 38 | 3adant2 1132 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (โโ(๐ด /
๐ต)) โ
โ) |
40 | 19 | 3ad2ant2 1135 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ๐ โ
โ) |
41 | 35, 39, 40 | adddid 11238 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (๐ต ยท
((โโ(๐ด / ๐ต)) + ๐)) = ((๐ต ยท (โโ(๐ด / ๐ต))) + (๐ต ยท ๐))) |
42 | | mulcom 11196 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ต โ โ) โ (๐ ยท ๐ต) = (๐ต ยท ๐)) |
43 | 19, 34, 42 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ต โ โ+)
โ (๐ ยท ๐ต) = (๐ต ยท ๐)) |
44 | 43 | 3adant1 1131 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (๐ ยท ๐ต) = (๐ต ยท ๐)) |
45 | 44 | eqcomd 2739 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (๐ต ยท ๐) = (๐ ยท ๐ต)) |
46 | 45 | oveq2d 7425 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ((๐ต ยท
(โโ(๐ด / ๐ต))) + (๐ต ยท ๐)) = ((๐ต ยท (โโ(๐ด / ๐ต))) + (๐ ยท ๐ต))) |
47 | 33, 41, 46 | 3eqtrd 2777 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (๐ต ยท
(โโ((๐ด + (๐ ยท ๐ต)) / ๐ต))) = ((๐ต ยท (โโ(๐ด / ๐ต))) + (๐ ยท ๐ต))) |
48 | 47 | oveq2d 7425 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ((๐ด + (๐ ยท ๐ต)) โ (๐ต ยท (โโ((๐ด + (๐ ยท ๐ต)) / ๐ต)))) = ((๐ด + (๐ ยท ๐ต)) โ ((๐ต ยท (โโ(๐ด / ๐ต))) + (๐ ยท ๐ต)))) |
49 | 34 | adantl 483 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ+)
โ ๐ต โ
โ) |
50 | 49, 38 | mulcld 11234 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (๐ต ยท
(โโ(๐ด / ๐ต))) โ
โ) |
51 | 50 | 3adant2 1132 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (๐ต ยท
(โโ(๐ด / ๐ต))) โ
โ) |
52 | 12, 51, 14 | pnpcan2d 11609 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ((๐ด + (๐ ยท ๐ต)) โ ((๐ต ยท (โโ(๐ด / ๐ต))) + (๐ ยท ๐ต))) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
53 | 10, 48, 52 | 3eqtrd 2777 |
. . 3
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ((๐ด + (๐ ยท ๐ต)) mod ๐ต) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
54 | | modval 13836 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (๐ด mod ๐ต) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
55 | 54 | 3adant2 1132 |
. . 3
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ (๐ด mod ๐ต) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
56 | 53, 55 | eqtr4d 2776 |
. 2
โข ((๐ด โ โ โง ๐ โ โค โง ๐ต โ โ+)
โ ((๐ด + (๐ ยท ๐ต)) mod ๐ต) = (๐ด mod ๐ต)) |
57 | 56 | 3com23 1127 |
1
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ โ โค)
โ ((๐ด + (๐ ยท ๐ต)) mod ๐ต) = (๐ด mod ๐ต)) |