Step | Hyp | Ref
| Expression |
1 | | qcn 9647 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
2 | 1 | 3ad2ant2 1020 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ ๐ โ โ) |
3 | | qcn 9647 |
. . . . . 6
โข (๐ด โ โ โ ๐ด โ
โ) |
4 | 3 | 3ad2ant1 1019 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ ๐ด โ โ) |
5 | 2, 4 | negsubd 8287 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ (๐ + -๐ด) = (๐ โ ๐ด)) |
6 | 5 | eqcomd 2193 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ (๐ โ ๐ด) = (๐ + -๐ด)) |
7 | 6 | oveq1d 5903 |
. 2
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ ((๐ โ ๐ด) mod ๐) = ((๐ + -๐ด) mod ๐)) |
8 | 2 | mulid2d 7989 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ (1 ยท ๐) = ๐) |
9 | 8 | oveq1d 5903 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ ((1 ยท
๐) + -๐ด) = (๐ + -๐ด)) |
10 | 9 | oveq1d 5903 |
. 2
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ (((1 ยท
๐) + -๐ด) mod ๐) = ((๐ + -๐ด) mod ๐)) |
11 | | 1cnd 7986 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ 1 โ
โ) |
12 | 11, 2 | mulcld 7991 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ (1 ยท ๐) โ
โ) |
13 | | qnegcl 9649 |
. . . . . . 7
โข (๐ด โ โ โ -๐ด โ
โ) |
14 | | qcn 9647 |
. . . . . . 7
โข (-๐ด โ โ โ -๐ด โ
โ) |
15 | 13, 14 | syl 14 |
. . . . . 6
โข (๐ด โ โ โ -๐ด โ
โ) |
16 | 15 | 3ad2ant1 1019 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ -๐ด โ
โ) |
17 | 12, 16 | addcomd 8121 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ ((1 ยท
๐) + -๐ด) = (-๐ด + (1 ยท ๐))) |
18 | 17 | oveq1d 5903 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ (((1 ยท
๐) + -๐ด) mod ๐) = ((-๐ด + (1 ยท ๐)) mod ๐)) |
19 | 13 | 3ad2ant1 1019 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ -๐ด โ
โ) |
20 | | 1zzd 9293 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ 1 โ
โค) |
21 | | simp2 999 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ ๐ โ โ) |
22 | | simp3 1000 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ 0 < ๐) |
23 | | modqcyc 10372 |
. . . 4
โข (((-๐ด โ โ โง 1 โ
โค) โง (๐ โ
โ โง 0 < ๐))
โ ((-๐ด + (1 ยท
๐)) mod ๐) = (-๐ด mod ๐)) |
24 | 19, 20, 21, 22, 23 | syl22anc 1249 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ ((-๐ด + (1 ยท ๐)) mod ๐) = (-๐ด mod ๐)) |
25 | 18, 24 | eqtrd 2220 |
. 2
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ (((1 ยท
๐) + -๐ด) mod ๐) = (-๐ด mod ๐)) |
26 | 7, 10, 25 | 3eqtr2rd 2227 |
1
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ (-๐ด mod ๐) = ((๐ โ ๐ด) mod ๐)) |