Step | Hyp | Ref
| Expression |
1 | | modqmuladd.a |
. . . . . . 7
โข (๐ โ ๐ด โ โค) |
2 | | zq 9625 |
. . . . . . 7
โข (๐ด โ โค โ ๐ด โ
โ) |
3 | 1, 2 | syl 14 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
4 | | modqmuladd.m |
. . . . . 6
โข (๐ โ ๐ โ โ) |
5 | | modqmuladd.mgt0 |
. . . . . . 7
โข (๐ โ 0 < ๐) |
6 | 5 | gt0ne0d 8468 |
. . . . . 6
โข (๐ โ ๐ โ 0) |
7 | | qdivcl 9642 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ โง ๐ โ 0) โ (๐ด / ๐) โ โ) |
8 | 3, 4, 6, 7 | syl3anc 1238 |
. . . . 5
โข (๐ โ (๐ด / ๐) โ โ) |
9 | 8 | flqcld 10276 |
. . . 4
โข (๐ โ (โโ(๐ด / ๐)) โ โค) |
10 | | oveq1 5881 |
. . . . . . 7
โข (๐ = (โโ(๐ด / ๐)) โ (๐ ยท ๐) = ((โโ(๐ด / ๐)) ยท ๐)) |
11 | 10 | oveq1d 5889 |
. . . . . 6
โข (๐ = (โโ(๐ด / ๐)) โ ((๐ ยท ๐) + (๐ด mod ๐)) = (((โโ(๐ด / ๐)) ยท ๐) + (๐ด mod ๐))) |
12 | 11 | eqeq2d 2189 |
. . . . 5
โข (๐ = (โโ(๐ด / ๐)) โ (๐ด = ((๐ ยท ๐) + (๐ด mod ๐)) โ ๐ด = (((โโ(๐ด / ๐)) ยท ๐) + (๐ด mod ๐)))) |
13 | 12 | adantl 277 |
. . . 4
โข ((๐ โง ๐ = (โโ(๐ด / ๐))) โ (๐ด = ((๐ ยท ๐) + (๐ด mod ๐)) โ ๐ด = (((โโ(๐ด / ๐)) ยท ๐) + (๐ด mod ๐)))) |
14 | | flqpmodeq 10326 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ
(((โโ(๐ด / ๐)) ยท ๐) + (๐ด mod ๐)) = ๐ด) |
15 | 3, 4, 5, 14 | syl3anc 1238 |
. . . . 5
โข (๐ โ (((โโ(๐ด / ๐)) ยท ๐) + (๐ด mod ๐)) = ๐ด) |
16 | 15 | eqcomd 2183 |
. . . 4
โข (๐ โ ๐ด = (((โโ(๐ด / ๐)) ยท ๐) + (๐ด mod ๐))) |
17 | 9, 13, 16 | rspcedvd 2847 |
. . 3
โข (๐ โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + (๐ด mod ๐))) |
18 | | oveq2 5882 |
. . . . . 6
โข (๐ต = (๐ด mod ๐) โ ((๐ ยท ๐) + ๐ต) = ((๐ ยท ๐) + (๐ด mod ๐))) |
19 | 18 | eqeq2d 2189 |
. . . . 5
โข (๐ต = (๐ด mod ๐) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ ๐ด = ((๐ ยท ๐) + (๐ด mod ๐)))) |
20 | 19 | eqcoms 2180 |
. . . 4
โข ((๐ด mod ๐) = ๐ต โ (๐ด = ((๐ ยท ๐) + ๐ต) โ ๐ด = ((๐ ยท ๐) + (๐ด mod ๐)))) |
21 | 20 | rexbidv 2478 |
. . 3
โข ((๐ด mod ๐) = ๐ต โ (โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต) โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + (๐ด mod ๐)))) |
22 | 17, 21 | syl5ibrcom 157 |
. 2
โข (๐ โ ((๐ด mod ๐) = ๐ต โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต))) |
23 | | oveq1 5881 |
. . . . . 6
โข (๐ด = ((๐ ยท ๐) + ๐ต) โ (๐ด mod ๐) = (((๐ ยท ๐) + ๐ต) mod ๐)) |
24 | 23 | adantl 277 |
. . . . 5
โข (((๐ โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ (๐ด mod ๐) = (((๐ ยท ๐) + ๐ต) mod ๐)) |
25 | | simplr 528 |
. . . . . 6
โข (((๐ โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ โ โค) |
26 | 4 | ad2antrr 488 |
. . . . . 6
โข (((๐ โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ โ โ) |
27 | | modqmuladd.bq |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
28 | 27 | ad2antrr 488 |
. . . . . 6
โข (((๐ โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ต โ โ) |
29 | | modqmuladd.b |
. . . . . . 7
โข (๐ โ ๐ต โ (0[,)๐)) |
30 | 29 | ad2antrr 488 |
. . . . . 6
โข (((๐ โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ต โ (0[,)๐)) |
31 | | mulqaddmodid 10363 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ) โง (๐ต โ โ โง ๐ต โ (0[,)๐))) โ (((๐ ยท ๐) + ๐ต) mod ๐) = ๐ต) |
32 | 25, 26, 28, 30, 31 | syl22anc 1239 |
. . . . 5
โข (((๐ โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ (((๐ ยท ๐) + ๐ต) mod ๐) = ๐ต) |
33 | 24, 32 | eqtrd 2210 |
. . . 4
โข (((๐ โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ (๐ด mod ๐) = ๐ต) |
34 | 33 | ex 115 |
. . 3
โข ((๐ โง ๐ โ โค) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ (๐ด mod ๐) = ๐ต)) |
35 | 34 | rexlimdva 2594 |
. 2
โข (๐ โ (โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต) โ (๐ด mod ๐) = ๐ต)) |
36 | 22, 35 | impbid 129 |
1
โข (๐ โ ((๐ด mod ๐) = ๐ต โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต))) |