Step | Hyp | Ref
| Expression |
1 | | modval 13782 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (๐ด mod ๐ต) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
2 | 1 | adantr 482 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ด mod ๐ต) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
3 | | rerpdivcl 12950 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (๐ด / ๐ต) โ
โ) |
4 | 3 | adantr 482 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ด / ๐ต) โ โ) |
5 | 4 | recnd 11188 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ด / ๐ต) โ โ) |
6 | | addid2 11343 |
. . . . . . . . 9
โข ((๐ด / ๐ต) โ โ โ (0 + (๐ด / ๐ต)) = (๐ด / ๐ต)) |
7 | 6 | fveq2d 6847 |
. . . . . . . 8
โข ((๐ด / ๐ต) โ โ โ (โโ(0 +
(๐ด / ๐ต))) = (โโ(๐ด / ๐ต))) |
8 | 5, 7 | syl 17 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (โโ(0 + (๐ด / ๐ต))) = (โโ(๐ด / ๐ต))) |
9 | | rpregt0 12934 |
. . . . . . . . . . 11
โข (๐ต โ โ+
โ (๐ต โ โ
โง 0 < ๐ต)) |
10 | | divge0 12029 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 โค (๐ด / ๐ต)) |
11 | 9, 10 | sylan2 594 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ 0 โค
(๐ด / ๐ต)) |
12 | 11 | an32s 651 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง 0 โค ๐ด) โ 0
โค (๐ด / ๐ต)) |
13 | 12 | adantrr 716 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ 0 โค (๐ด / ๐ต)) |
14 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ต โ โ+
โง ๐ด < ๐ต) โ ๐ด < ๐ต) |
15 | | rpcn 12930 |
. . . . . . . . . . . . 13
โข (๐ต โ โ+
โ ๐ต โ
โ) |
16 | 15 | mulid1d 11177 |
. . . . . . . . . . . 12
โข (๐ต โ โ+
โ (๐ต ยท 1) =
๐ต) |
17 | 16 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ต โ โ+
โง ๐ด < ๐ต) โ (๐ต ยท 1) = ๐ต) |
18 | 14, 17 | breqtrrd 5134 |
. . . . . . . . . 10
โข ((๐ต โ โ+
โง ๐ด < ๐ต) โ ๐ด < (๐ต ยท 1)) |
19 | 18 | ad2ant2l 745 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ ๐ด < (๐ต ยท 1)) |
20 | | simpll 766 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ ๐ด โ โ) |
21 | 9 | ad2antlr 726 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ต โ โ โง 0 < ๐ต)) |
22 | | 1re 11160 |
. . . . . . . . . . 11
โข 1 โ
โ |
23 | | ltdivmul 12035 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 1 โ
โ โง (๐ต โ
โ โง 0 < ๐ต))
โ ((๐ด / ๐ต) < 1 โ ๐ด < (๐ต ยท 1))) |
24 | 22, 23 | mp3an2 1450 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ต โ โ โง 0 <
๐ต)) โ ((๐ด / ๐ต) < 1 โ ๐ด < (๐ต ยท 1))) |
25 | 20, 21, 24 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ ((๐ด / ๐ต) < 1 โ ๐ด < (๐ต ยท 1))) |
26 | 19, 25 | mpbird 257 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ด / ๐ต) < 1) |
27 | | 0z 12515 |
. . . . . . . . 9
โข 0 โ
โค |
28 | | flbi2 13728 |
. . . . . . . . 9
โข ((0
โ โค โง (๐ด /
๐ต) โ โ) โ
((โโ(0 + (๐ด /
๐ต))) = 0 โ (0 โค
(๐ด / ๐ต) โง (๐ด / ๐ต) < 1))) |
29 | 27, 4, 28 | sylancr 588 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ ((โโ(0 + (๐ด / ๐ต))) = 0 โ (0 โค (๐ด / ๐ต) โง (๐ด / ๐ต) < 1))) |
30 | 13, 26, 29 | mpbir2and 712 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (โโ(0 + (๐ด / ๐ต))) = 0) |
31 | 8, 30 | eqtr3d 2775 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (โโ(๐ด / ๐ต)) = 0) |
32 | 31 | oveq2d 7374 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ต ยท (โโ(๐ด / ๐ต))) = (๐ต ยท 0)) |
33 | 15 | mul01d 11359 |
. . . . . 6
โข (๐ต โ โ+
โ (๐ต ยท 0) =
0) |
34 | 33 | ad2antlr 726 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ต ยท 0) = 0) |
35 | 32, 34 | eqtrd 2773 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ต ยท (โโ(๐ด / ๐ต))) = 0) |
36 | 35 | oveq2d 7374 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต)))) = (๐ด โ 0)) |
37 | | recn 11146 |
. . . . 5
โข (๐ด โ โ โ ๐ด โ
โ) |
38 | 37 | subid1d 11506 |
. . . 4
โข (๐ด โ โ โ (๐ด โ 0) = ๐ด) |
39 | 38 | ad2antrr 725 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ด โ 0) = ๐ด) |
40 | 36, 39 | eqtrd 2773 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต)))) = ๐ด) |
41 | 2, 40 | eqtrd 2773 |
1
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ด mod ๐ต) = ๐ด) |