Step | Hyp | Ref
| Expression |
1 | | simpl1 1000 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ๐ด โ
โ) |
2 | | qcn 9633 |
. . . . 5
โข (๐ด โ โ โ ๐ด โ
โ) |
3 | 1, 2 | syl 14 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ๐ด โ
โ) |
4 | | simpl2 1001 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ๐ต โ
โ) |
5 | | simprl 529 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ๐ โ
โ) |
6 | | simprr 531 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ 0 < ๐) |
7 | 4, 5, 6 | modqcld 10327 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ (๐ต mod ๐) โ โ) |
8 | | simpl3 1002 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ๐ถ โ
โค) |
9 | | zq 9625 |
. . . . . . 7
โข (๐ถ โ โค โ ๐ถ โ
โ) |
10 | 8, 9 | syl 14 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ๐ถ โ
โ) |
11 | | qmulcl 9636 |
. . . . . 6
โข (((๐ต mod ๐) โ โ โง ๐ถ โ โ) โ ((๐ต mod ๐) ยท ๐ถ) โ โ) |
12 | 7, 10, 11 | syl2anc 411 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ((๐ต mod ๐) ยท ๐ถ) โ โ) |
13 | | qcn 9633 |
. . . . 5
โข (((๐ต mod ๐) ยท ๐ถ) โ โ โ ((๐ต mod ๐) ยท ๐ถ) โ โ) |
14 | 12, 13 | syl 14 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ((๐ต mod ๐) ยท ๐ถ) โ โ) |
15 | 3, 14 | addcomd 8107 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ (๐ด + ((๐ต mod ๐) ยท ๐ถ)) = (((๐ต mod ๐) ยท ๐ถ) + ๐ด)) |
16 | 15 | oveq1d 5889 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ((๐ด + ((๐ต mod ๐) ยท ๐ถ)) mod ๐) = ((((๐ต mod ๐) ยท ๐ถ) + ๐ด) mod ๐)) |
17 | 9 | 3ad2ant3 1020 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โ ๐ถ โ
โ) |
18 | 17 | adantr 276 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ๐ถ โ
โ) |
19 | 7, 18, 11 | syl2anc 411 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ((๐ต mod ๐) ยท ๐ถ) โ โ) |
20 | | qmulcl 9636 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยท ๐ถ) โ โ) |
21 | 4, 18, 20 | syl2anc 411 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ (๐ต ยท ๐ถ) โ โ) |
22 | 21, 5, 6 | modqcld 10327 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ((๐ต ยท ๐ถ) mod ๐) โ โ) |
23 | | modqmulmod 10388 |
. . . . 5
โข (((๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ (((๐ต mod ๐) ยท ๐ถ) mod ๐) = ((๐ต ยท ๐ถ) mod ๐)) |
24 | 23 | 3adantl1 1153 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ (((๐ต mod ๐) ยท ๐ถ) mod ๐) = ((๐ต ยท ๐ถ) mod ๐)) |
25 | | modqabs2 10357 |
. . . . 5
โข (((๐ต ยท ๐ถ) โ โ โง ๐ โ โ โง 0 < ๐) โ (((๐ต ยท ๐ถ) mod ๐) mod ๐) = ((๐ต ยท ๐ถ) mod ๐)) |
26 | 21, 5, 6, 25 | syl3anc 1238 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ (((๐ต ยท ๐ถ) mod ๐) mod ๐) = ((๐ต ยท ๐ถ) mod ๐)) |
27 | 24, 26 | eqtr4d 2213 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ (((๐ต mod ๐) ยท ๐ถ) mod ๐) = (((๐ต ยท ๐ถ) mod ๐) mod ๐)) |
28 | 19, 22, 1, 5, 6, 27 | modqadd1 10360 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ((((๐ต mod ๐) ยท ๐ถ) + ๐ด) mod ๐) = ((((๐ต ยท ๐ถ) mod ๐) + ๐ด) mod ๐)) |
29 | | modqaddmod 10362 |
. . . 4
โข ((((๐ต ยท ๐ถ) โ โ โง ๐ด โ โ) โง (๐ โ โ โง 0 < ๐)) โ ((((๐ต ยท ๐ถ) mod ๐) + ๐ด) mod ๐) = (((๐ต ยท ๐ถ) + ๐ด) mod ๐)) |
30 | 21, 1, 5, 6, 29 | syl22anc 1239 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ((((๐ต ยท ๐ถ) mod ๐) + ๐ด) mod ๐) = (((๐ต ยท ๐ถ) + ๐ด) mod ๐)) |
31 | | qcn 9633 |
. . . . . 6
โข ((๐ต ยท ๐ถ) โ โ โ (๐ต ยท ๐ถ) โ โ) |
32 | 21, 31 | syl 14 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ (๐ต ยท ๐ถ) โ โ) |
33 | 32, 3 | addcomd 8107 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ((๐ต ยท ๐ถ) + ๐ด) = (๐ด + (๐ต ยท ๐ถ))) |
34 | 33 | oveq1d 5889 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ (((๐ต ยท ๐ถ) + ๐ด) mod ๐) = ((๐ด + (๐ต ยท ๐ถ)) mod ๐)) |
35 | 30, 34 | eqtrd 2210 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ((((๐ต ยท ๐ถ) mod ๐) + ๐ด) mod ๐) = ((๐ด + (๐ต ยท ๐ถ)) mod ๐)) |
36 | 16, 28, 35 | 3eqtrd 2214 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ((๐ด + ((๐ต mod ๐) ยท ๐ถ)) mod ๐) = ((๐ด + (๐ต ยท ๐ถ)) mod ๐)) |