Step | Hyp | Ref
| Expression |
1 | | simpll 527 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ด โ โ) |
2 | | simplr 528 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ต โ โ) |
3 | | 0red 7957 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ 0 โ โ) |
4 | | qre 9624 |
. . . . 5
โข (๐ด โ โ โ ๐ด โ
โ) |
5 | 4 | ad2antrr 488 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ด โ โ) |
6 | | qre 9624 |
. . . . 5
โข (๐ต โ โ โ ๐ต โ
โ) |
7 | 6 | ad2antlr 489 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ต โ โ) |
8 | | simprl 529 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ 0 โค ๐ด) |
9 | | simprr 531 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ด < ๐ต) |
10 | 3, 5, 7, 8, 9 | lelttrd 8081 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ 0 < ๐ต) |
11 | | modqval 10323 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โ (๐ด mod ๐ต) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
12 | 1, 2, 10, 11 | syl3anc 1238 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ด mod ๐ต) = (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต))))) |
13 | 10 | gt0ne0d 8468 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ต โ 0) |
14 | | qdivcl 9642 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด / ๐ต) โ โ) |
15 | 1, 2, 13, 14 | syl3anc 1238 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ด / ๐ต) โ โ) |
16 | | qcn 9633 |
. . . . . . . 8
โข ((๐ด / ๐ต) โ โ โ (๐ด / ๐ต) โ โ) |
17 | | addlid 8095 |
. . . . . . . . 9
โข ((๐ด / ๐ต) โ โ โ (0 + (๐ด / ๐ต)) = (๐ด / ๐ต)) |
18 | 17 | fveq2d 5519 |
. . . . . . . 8
โข ((๐ด / ๐ต) โ โ โ (โโ(0 +
(๐ด / ๐ต))) = (โโ(๐ด / ๐ต))) |
19 | 15, 16, 18 | 3syl 17 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (โโ(0 + (๐ด / ๐ต))) = (โโ(๐ด / ๐ต))) |
20 | | divge0 8829 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 โค (๐ด / ๐ต)) |
21 | 5, 8, 7, 10, 20 | syl22anc 1239 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ 0 โค (๐ด / ๐ต)) |
22 | 7 | recnd 7985 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ต โ โ) |
23 | 22 | mulridd 7973 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ต ยท 1) = ๐ต) |
24 | 9, 23 | breqtrrd 4031 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ด < (๐ต ยท 1)) |
25 | | 1red 7971 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ 1 โ โ) |
26 | | ltdivmul 8832 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 1 โ
โ โง (๐ต โ
โ โง 0 < ๐ต))
โ ((๐ด / ๐ต) < 1 โ ๐ด < (๐ต ยท 1))) |
27 | 5, 25, 7, 10, 26 | syl112anc 1242 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ((๐ด / ๐ต) < 1 โ ๐ด < (๐ต ยท 1))) |
28 | 24, 27 | mpbird 167 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ด / ๐ต) < 1) |
29 | | 0z 9263 |
. . . . . . . . 9
โข 0 โ
โค |
30 | | flqbi2 10290 |
. . . . . . . . 9
โข ((0
โ โค โง (๐ด /
๐ต) โ โ) โ
((โโ(0 + (๐ด /
๐ต))) = 0 โ (0 โค
(๐ด / ๐ต) โง (๐ด / ๐ต) < 1))) |
31 | 29, 15, 30 | sylancr 414 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ((โโ(0 + (๐ด / ๐ต))) = 0 โ (0 โค (๐ด / ๐ต) โง (๐ด / ๐ต) < 1))) |
32 | 21, 28, 31 | mpbir2and 944 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (โโ(0 + (๐ด / ๐ต))) = 0) |
33 | 19, 32 | eqtr3d 2212 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (โโ(๐ด / ๐ต)) = 0) |
34 | 33 | oveq2d 5890 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ต ยท (โโ(๐ด / ๐ต))) = (๐ต ยท 0)) |
35 | 22 | mul01d 8349 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ต ยท 0) = 0) |
36 | 34, 35 | eqtrd 2210 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ต ยท (โโ(๐ด / ๐ต))) = 0) |
37 | 36 | oveq2d 5890 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต)))) = (๐ด โ 0)) |
38 | 5 | recnd 7985 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ ๐ด โ โ) |
39 | 38 | subid1d 8256 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ด โ 0) = ๐ด) |
40 | 37, 39 | eqtrd 2210 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ด โ (๐ต ยท (โโ(๐ด / ๐ต)))) = ๐ด) |
41 | 12, 40 | eqtrd 2210 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ด mod ๐ต) = ๐ด) |