Step | Hyp | Ref
| Expression |
1 | | 0red 11222 |
. . . . 5
โข (๐ โ โ+
โ 0 โ โ) |
2 | | rpxr 12988 |
. . . . 5
โข (๐ โ โ+
โ ๐ โ
โ*) |
3 | | elico2 13393 |
. . . . 5
โข ((0
โ โ โง ๐
โ โ*) โ (๐ด โ (0[,)๐) โ (๐ด โ โ โง 0 โค ๐ด โง ๐ด < ๐))) |
4 | 1, 2, 3 | syl2anc 583 |
. . . 4
โข (๐ โ โ+
โ (๐ด โ (0[,)๐) โ (๐ด โ โ โง 0 โค ๐ด โง ๐ด < ๐))) |
5 | 4 | adantl 481 |
. . 3
โข ((๐ โ โค โง ๐ โ โ+)
โ (๐ด โ (0[,)๐) โ (๐ด โ โ โง 0 โค ๐ด โง ๐ด < ๐))) |
6 | | zcn 12568 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
โ) |
7 | | rpcn 12989 |
. . . . . . . . 9
โข (๐ โ โ+
โ ๐ โ
โ) |
8 | | mulcl 11198 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
9 | 6, 7, 8 | syl2an 595 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ+)
โ (๐ ยท ๐) โ
โ) |
10 | 9 | adantr 480 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โ+)
โง (๐ด โ โ
โง 0 โค ๐ด โง ๐ด < ๐)) โ (๐ ยท ๐) โ โ) |
11 | | recn 11204 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด โ
โ) |
12 | 11 | 3ad2ant1 1132 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 โค
๐ด โง ๐ด < ๐) โ ๐ด โ โ) |
13 | 12 | adantl 481 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โ+)
โง (๐ด โ โ
โง 0 โค ๐ด โง ๐ด < ๐)) โ ๐ด โ โ) |
14 | 10, 13 | addcomd 11421 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ+)
โง (๐ด โ โ
โง 0 โค ๐ด โง ๐ด < ๐)) โ ((๐ ยท ๐) + ๐ด) = (๐ด + (๐ ยท ๐))) |
15 | 14 | oveq1d 7427 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โ+)
โง (๐ด โ โ
โง 0 โค ๐ด โง ๐ด < ๐)) โ (((๐ ยท ๐) + ๐ด) mod ๐) = ((๐ด + (๐ ยท ๐)) mod ๐)) |
16 | | simp1 1135 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
๐ด โง ๐ด < ๐) โ ๐ด โ โ) |
17 | 16 | adantl 481 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ+)
โง (๐ด โ โ
โง 0 โค ๐ด โง ๐ด < ๐)) โ ๐ด โ โ) |
18 | | simpr 484 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ+)
โ ๐ โ
โ+) |
19 | 18 | adantr 480 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ+)
โง (๐ด โ โ
โง 0 โค ๐ด โง ๐ด < ๐)) โ ๐ โ
โ+) |
20 | | simpll 764 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ+)
โง (๐ด โ โ
โง 0 โค ๐ด โง ๐ด < ๐)) โ ๐ โ โค) |
21 | | modcyc 13876 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ+
โง ๐ โ โค)
โ ((๐ด + (๐ ยท ๐)) mod ๐) = (๐ด mod ๐)) |
22 | 17, 19, 20, 21 | syl3anc 1370 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โ+)
โง (๐ด โ โ
โง 0 โค ๐ด โง ๐ด < ๐)) โ ((๐ด + (๐ ยท ๐)) mod ๐) = (๐ด mod ๐)) |
23 | 18, 16 | anim12ci 613 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ+)
โง (๐ด โ โ
โง 0 โค ๐ด โง ๐ด < ๐)) โ (๐ด โ โ โง ๐ โ
โ+)) |
24 | | 3simpc 1149 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
๐ด โง ๐ด < ๐) โ (0 โค ๐ด โง ๐ด < ๐)) |
25 | 24 | adantl 481 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ+)
โง (๐ด โ โ
โง 0 โค ๐ด โง ๐ด < ๐)) โ (0 โค ๐ด โง ๐ด < ๐)) |
26 | | modid 13866 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ+)
โง (0 โค ๐ด โง ๐ด < ๐)) โ (๐ด mod ๐) = ๐ด) |
27 | 23, 25, 26 | syl2anc 583 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โ+)
โง (๐ด โ โ
โง 0 โค ๐ด โง ๐ด < ๐)) โ (๐ด mod ๐) = ๐ด) |
28 | 15, 22, 27 | 3eqtrd 2775 |
. . . 4
โข (((๐ โ โค โง ๐ โ โ+)
โง (๐ด โ โ
โง 0 โค ๐ด โง ๐ด < ๐)) โ (((๐ ยท ๐) + ๐ด) mod ๐) = ๐ด) |
29 | 28 | ex 412 |
. . 3
โข ((๐ โ โค โง ๐ โ โ+)
โ ((๐ด โ โ
โง 0 โค ๐ด โง ๐ด < ๐) โ (((๐ ยท ๐) + ๐ด) mod ๐) = ๐ด)) |
30 | 5, 29 | sylbid 239 |
. 2
โข ((๐ โ โค โง ๐ โ โ+)
โ (๐ด โ (0[,)๐) โ (((๐ ยท ๐) + ๐ด) mod ๐) = ๐ด)) |
31 | 30 | 3impia 1116 |
1
โข ((๐ โ โค โง ๐ โ โ+
โง ๐ด โ (0[,)๐)) โ (((๐ ยท ๐) + ๐ด) mod ๐) = ๐ด) |