Step | Hyp | Ref
| Expression |
1 | | nnre 12218 |
. . . . . . 7
โข (๐ต โ โ โ ๐ต โ
โ) |
2 | | nnnn0 12478 |
. . . . . . 7
โข (๐พ โ โ โ ๐พ โ
โ0) |
3 | | reexpcl 14043 |
. . . . . . 7
โข ((๐ต โ โ โง ๐พ โ โ0)
โ (๐ตโ๐พ) โ
โ) |
4 | 1, 2, 3 | syl2an 596 |
. . . . . 6
โข ((๐ต โ โ โง ๐พ โ โ) โ (๐ตโ๐พ) โ โ) |
5 | | remulcl 11194 |
. . . . . 6
โข (((๐ตโ๐พ) โ โ โง ๐ด โ โ) โ ((๐ตโ๐พ) ยท ๐ด) โ โ) |
6 | 4, 5 | stoic3 1778 |
. . . . 5
โข ((๐ต โ โ โง ๐พ โ โ โง ๐ด โ โ) โ ((๐ตโ๐พ) ยท ๐ด) โ โ) |
7 | 6 | 3comr 1125 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ((๐ตโ๐พ) ยท ๐ด) โ โ) |
8 | | reflcl 13760 |
. . . 4
โข (((๐ตโ๐พ) ยท ๐ด) โ โ โ
(โโ((๐ตโ๐พ) ยท ๐ด)) โ โ) |
9 | 7, 8 | syl 17 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
(โโ((๐ตโ๐พ) ยท ๐ด)) โ โ) |
10 | | nnrp 12984 |
. . . 4
โข (๐ต โ โ โ ๐ต โ
โ+) |
11 | 10 | 3ad2ant2 1134 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ๐ต โ
โ+) |
12 | | modval 13835 |
. . 3
โข
(((โโ((๐ตโ๐พ) ยท ๐ด)) โ โ โง ๐ต โ โ+) โ
((โโ((๐ตโ๐พ) ยท ๐ด)) mod ๐ต) = ((โโ((๐ตโ๐พ) ยท ๐ด)) โ (๐ต ยท
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต))))) |
13 | 9, 11, 12 | syl2anc 584 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
((โโ((๐ตโ๐พ) ยท ๐ด)) mod ๐ต) = ((โโ((๐ตโ๐พ) ยท ๐ด)) โ (๐ต ยท
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต))))) |
14 | | simp2 1137 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ๐ต โ
โ) |
15 | | fldiv 13824 |
. . . . . 6
โข ((((๐ตโ๐พ) ยท ๐ด) โ โ โง ๐ต โ โ) โ
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต)) = (โโ(((๐ตโ๐พ) ยท ๐ด) / ๐ต))) |
16 | 7, 14, 15 | syl2anc 584 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต)) = (โโ(((๐ตโ๐พ) ยท ๐ด) / ๐ต))) |
17 | | nncn 12219 |
. . . . . . . . . 10
โข (๐ต โ โ โ ๐ต โ
โ) |
18 | | expcl 14044 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐พ โ โ0)
โ (๐ตโ๐พ) โ
โ) |
19 | 17, 2, 18 | syl2an 596 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐พ โ โ) โ (๐ตโ๐พ) โ โ) |
20 | 19 | 3adant1 1130 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ (๐ตโ๐พ) โ โ) |
21 | | recn 11199 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด โ
โ) |
22 | 21 | 3ad2ant1 1133 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ๐ด โ
โ) |
23 | | nnne0 12245 |
. . . . . . . . . 10
โข (๐ต โ โ โ ๐ต โ 0) |
24 | 17, 23 | jca 512 |
. . . . . . . . 9
โข (๐ต โ โ โ (๐ต โ โ โง ๐ต โ 0)) |
25 | 24 | 3ad2ant2 1134 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ (๐ต โ โ โง ๐ต โ 0)) |
26 | | div23 11890 |
. . . . . . . 8
โข (((๐ตโ๐พ) โ โ โง ๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ (((๐ตโ๐พ) ยท ๐ด) / ๐ต) = (((๐ตโ๐พ) / ๐ต) ยท ๐ด)) |
27 | 20, 22, 25, 26 | syl3anc 1371 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ (((๐ตโ๐พ) ยท ๐ด) / ๐ต) = (((๐ตโ๐พ) / ๐ต) ยท ๐ด)) |
28 | | nnz 12578 |
. . . . . . . . . 10
โข (๐พ โ โ โ ๐พ โ
โค) |
29 | | expm1 14077 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ต โ 0 โง ๐พ โ โค) โ (๐ตโ(๐พ โ 1)) = ((๐ตโ๐พ) / ๐ต)) |
30 | 17, 23, 28, 29 | syl2an3an 1422 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐พ โ โ) โ (๐ตโ(๐พ โ 1)) = ((๐ตโ๐พ) / ๐ต)) |
31 | 30 | 3adant1 1130 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ (๐ตโ(๐พ โ 1)) = ((๐ตโ๐พ) / ๐ต)) |
32 | 31 | oveq1d 7423 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ((๐ตโ(๐พ โ 1)) ยท ๐ด) = (((๐ตโ๐พ) / ๐ต) ยท ๐ด)) |
33 | 27, 32 | eqtr4d 2775 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ (((๐ตโ๐พ) ยท ๐ด) / ๐ต) = ((๐ตโ(๐พ โ 1)) ยท ๐ด)) |
34 | 33 | fveq2d 6895 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
(โโ(((๐ตโ๐พ) ยท ๐ด) / ๐ต)) = (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด))) |
35 | 16, 34 | eqtrd 2772 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต)) = (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด))) |
36 | 35 | oveq2d 7424 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ (๐ต ยท
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต))) = (๐ต ยท (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด)))) |
37 | 36 | oveq2d 7424 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
((โโ((๐ตโ๐พ) ยท ๐ด)) โ (๐ต ยท
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต)))) = ((โโ((๐ตโ๐พ) ยท ๐ด)) โ (๐ต ยท (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด))))) |
38 | 13, 37 | eqtrd 2772 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
((โโ((๐ตโ๐พ) ยท ๐ด)) mod ๐ต) = ((โโ((๐ตโ๐พ) ยท ๐ด)) โ (๐ต ยท (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด))))) |