Step | Hyp | Ref
| Expression |
1 | | nnre 12226 |
. . . . . . 7
โข (๐ต โ โ โ ๐ต โ
โ) |
2 | | nnnn0 12486 |
. . . . . . 7
โข (๐พ โ โ โ ๐พ โ
โ0) |
3 | | reexpcl 14051 |
. . . . . . 7
โข ((๐ต โ โ โง ๐พ โ โ0)
โ (๐ตโ๐พ) โ
โ) |
4 | 1, 2, 3 | syl2an 595 |
. . . . . 6
โข ((๐ต โ โ โง ๐พ โ โ) โ (๐ตโ๐พ) โ โ) |
5 | | remulcl 11201 |
. . . . . 6
โข (((๐ตโ๐พ) โ โ โง ๐ด โ โ) โ ((๐ตโ๐พ) ยท ๐ด) โ โ) |
6 | 4, 5 | stoic3 1777 |
. . . . 5
โข ((๐ต โ โ โง ๐พ โ โ โง ๐ด โ โ) โ ((๐ตโ๐พ) ยท ๐ด) โ โ) |
7 | 6 | 3comr 1124 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ((๐ตโ๐พ) ยท ๐ด) โ โ) |
8 | | reflcl 13768 |
. . . 4
โข (((๐ตโ๐พ) ยท ๐ด) โ โ โ
(โโ((๐ตโ๐พ) ยท ๐ด)) โ โ) |
9 | 7, 8 | syl 17 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
(โโ((๐ตโ๐พ) ยท ๐ด)) โ โ) |
10 | | nnrp 12992 |
. . . 4
โข (๐ต โ โ โ ๐ต โ
โ+) |
11 | 10 | 3ad2ant2 1133 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ๐ต โ
โ+) |
12 | | modval 13843 |
. . 3
โข
(((โโ((๐ตโ๐พ) ยท ๐ด)) โ โ โง ๐ต โ โ+) โ
((โโ((๐ตโ๐พ) ยท ๐ด)) mod ๐ต) = ((โโ((๐ตโ๐พ) ยท ๐ด)) โ (๐ต ยท
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต))))) |
13 | 9, 11, 12 | syl2anc 583 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
((โโ((๐ตโ๐พ) ยท ๐ด)) mod ๐ต) = ((โโ((๐ตโ๐พ) ยท ๐ด)) โ (๐ต ยท
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต))))) |
14 | | simp2 1136 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ๐ต โ
โ) |
15 | | fldiv 13832 |
. . . . . 6
โข ((((๐ตโ๐พ) ยท ๐ด) โ โ โง ๐ต โ โ) โ
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต)) = (โโ(((๐ตโ๐พ) ยท ๐ด) / ๐ต))) |
16 | 7, 14, 15 | syl2anc 583 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต)) = (โโ(((๐ตโ๐พ) ยท ๐ด) / ๐ต))) |
17 | | nncn 12227 |
. . . . . . . . . 10
โข (๐ต โ โ โ ๐ต โ
โ) |
18 | | expcl 14052 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐พ โ โ0)
โ (๐ตโ๐พ) โ
โ) |
19 | 17, 2, 18 | syl2an 595 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐พ โ โ) โ (๐ตโ๐พ) โ โ) |
20 | 19 | 3adant1 1129 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ (๐ตโ๐พ) โ โ) |
21 | | recn 11206 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด โ
โ) |
22 | 21 | 3ad2ant1 1132 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ๐ด โ
โ) |
23 | | nnne0 12253 |
. . . . . . . . . 10
โข (๐ต โ โ โ ๐ต โ 0) |
24 | 17, 23 | jca 511 |
. . . . . . . . 9
โข (๐ต โ โ โ (๐ต โ โ โง ๐ต โ 0)) |
25 | 24 | 3ad2ant2 1133 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ (๐ต โ โ โง ๐ต โ 0)) |
26 | | div23 11898 |
. . . . . . . 8
โข (((๐ตโ๐พ) โ โ โง ๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ (((๐ตโ๐พ) ยท ๐ด) / ๐ต) = (((๐ตโ๐พ) / ๐ต) ยท ๐ด)) |
27 | 20, 22, 25, 26 | syl3anc 1370 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ (((๐ตโ๐พ) ยท ๐ด) / ๐ต) = (((๐ตโ๐พ) / ๐ต) ยท ๐ด)) |
28 | | nnz 12586 |
. . . . . . . . . 10
โข (๐พ โ โ โ ๐พ โ
โค) |
29 | | expm1 14085 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ต โ 0 โง ๐พ โ โค) โ (๐ตโ(๐พ โ 1)) = ((๐ตโ๐พ) / ๐ต)) |
30 | 17, 23, 28, 29 | syl2an3an 1421 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐พ โ โ) โ (๐ตโ(๐พ โ 1)) = ((๐ตโ๐พ) / ๐ต)) |
31 | 30 | 3adant1 1129 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ (๐ตโ(๐พ โ 1)) = ((๐ตโ๐พ) / ๐ต)) |
32 | 31 | oveq1d 7427 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ((๐ตโ(๐พ โ 1)) ยท ๐ด) = (((๐ตโ๐พ) / ๐ต) ยท ๐ด)) |
33 | 27, 32 | eqtr4d 2774 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ (((๐ตโ๐พ) ยท ๐ด) / ๐ต) = ((๐ตโ(๐พ โ 1)) ยท ๐ด)) |
34 | 33 | fveq2d 6895 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
(โโ(((๐ตโ๐พ) ยท ๐ด) / ๐ต)) = (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด))) |
35 | 16, 34 | eqtrd 2771 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต)) = (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด))) |
36 | 35 | oveq2d 7428 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ (๐ต ยท
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต))) = (๐ต ยท (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด)))) |
37 | 36 | oveq2d 7428 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
((โโ((๐ตโ๐พ) ยท ๐ด)) โ (๐ต ยท
(โโ((โโ((๐ตโ๐พ) ยท ๐ด)) / ๐ต)))) = ((โโ((๐ตโ๐พ) ยท ๐ด)) โ (๐ต ยท (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด))))) |
38 | 13, 37 | eqtrd 2771 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ
((โโ((๐ตโ๐พ) ยท ๐ด)) mod ๐ต) = ((โโ((๐ตโ๐พ) ยท ๐ด)) โ (๐ต ยท (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด))))) |