Step | Hyp | Ref
| Expression |
1 | | simpll 527 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ ๐ โ โค) |
2 | 1 | zcnd 9389 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ ๐ โ โ) |
3 | | qre 9638 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
4 | 3 | ad2antlr 489 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ ๐ โ โ) |
5 | 4 | recnd 7999 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ ๐ โ โ) |
6 | 2, 5 | mulcld 7991 |
. . . 4
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ (๐ ยท ๐) โ โ) |
7 | | simprr 531 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ ๐ด โ (0[,)๐)) |
8 | | 0red 7971 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ 0 โ
โ) |
9 | 4 | rexrd 8020 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ ๐ โ
โ*) |
10 | | elico2 9950 |
. . . . . . . 8
โข ((0
โ โ โง ๐
โ โ*) โ (๐ด โ (0[,)๐) โ (๐ด โ โ โง 0 โค ๐ด โง ๐ด < ๐))) |
11 | 8, 9, 10 | syl2anc 411 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ (๐ด โ (0[,)๐) โ (๐ด โ โ โง 0 โค ๐ด โง ๐ด < ๐))) |
12 | 7, 11 | mpbid 147 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ (๐ด โ โ โง 0 โค ๐ด โง ๐ด < ๐)) |
13 | 12 | simp1d 1010 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ ๐ด โ โ) |
14 | 13 | recnd 7999 |
. . . 4
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ ๐ด โ โ) |
15 | 6, 14 | addcomd 8121 |
. . 3
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ ((๐ ยท ๐) + ๐ด) = (๐ด + (๐ ยท ๐))) |
16 | 15 | oveq1d 5903 |
. 2
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ (((๐ ยท ๐) + ๐ด) mod ๐) = ((๐ด + (๐ ยท ๐)) mod ๐)) |
17 | | simprl 529 |
. . 3
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ ๐ด โ โ) |
18 | | simplr 528 |
. . 3
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ ๐ โ โ) |
19 | 12 | simp2d 1011 |
. . . 4
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ 0 โค ๐ด) |
20 | 12 | simp3d 1012 |
. . . 4
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ ๐ด < ๐) |
21 | 8, 13, 4, 19, 20 | lelttrd 8095 |
. . 3
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ 0 < ๐) |
22 | | modqcyc 10372 |
. . 3
โข (((๐ด โ โ โง ๐ โ โค) โง (๐ โ โ โง 0 <
๐)) โ ((๐ด + (๐ ยท ๐)) mod ๐) = (๐ด mod ๐)) |
23 | 17, 1, 18, 21, 22 | syl22anc 1249 |
. 2
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ ((๐ด + (๐ ยท ๐)) mod ๐) = (๐ด mod ๐)) |
24 | | modqid 10362 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ) โง (0 โค
๐ด โง ๐ด < ๐)) โ (๐ด mod ๐) = ๐ด) |
25 | 17, 18, 19, 20, 24 | syl22anc 1249 |
. 2
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ (๐ด mod ๐) = ๐ด) |
26 | 16, 23, 25 | 3eqtrd 2224 |
1
โข (((๐ โ โค โง ๐ โ โ) โง (๐ด โ โ โง ๐ด โ (0[,)๐))) โ (((๐ ยท ๐) + ๐ด) mod ๐) = ๐ด) |