Step | Hyp | Ref
| Expression |
1 | | recn 11223 |
. . . . . 6
โข (๐ด โ โ โ ๐ด โ
โ) |
2 | 1 | 3ad2ant1 1130 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โ ๐ด โ
โ) |
3 | 2 | adantr 479 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ๐ด โ
โ) |
4 | | simpl2 1189 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ๐ต โ
โ) |
5 | | simpr 483 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ๐ โ
โ+) |
6 | 4, 5 | modcld 13867 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ (๐ต mod ๐) โ
โ) |
7 | 6 | recnd 11267 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ (๐ต mod ๐) โ
โ) |
8 | | zcn 12588 |
. . . . . . 7
โข (๐ถ โ โค โ ๐ถ โ
โ) |
9 | 8 | 3ad2ant3 1132 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โ ๐ถ โ
โ) |
10 | 9 | adantr 479 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ๐ถ โ
โ) |
11 | 7, 10 | mulcld 11259 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ((๐ต mod ๐) ยท ๐ถ) โ โ) |
12 | 3, 11 | addcomd 11441 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ (๐ด + ((๐ต mod ๐) ยท ๐ถ)) = (((๐ต mod ๐) ยท ๐ถ) + ๐ด)) |
13 | 12 | oveq1d 7428 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ((๐ด + ((๐ต mod ๐) ยท ๐ถ)) mod ๐) = ((((๐ต mod ๐) ยท ๐ถ) + ๐ด) mod ๐)) |
14 | | zre 12587 |
. . . . . 6
โข (๐ถ โ โค โ ๐ถ โ
โ) |
15 | 14 | 3ad2ant3 1132 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โ ๐ถ โ
โ) |
16 | 15 | adantr 479 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ๐ถ โ
โ) |
17 | 6, 16 | remulcld 11269 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ((๐ต mod ๐) ยท ๐ถ) โ โ) |
18 | | simpl 481 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ถ โ โค) โ ๐ต โ
โ) |
19 | 14 | adantl 480 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ถ โ โค) โ ๐ถ โ
โ) |
20 | 18, 19 | remulcld 11269 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โค) โ (๐ต ยท ๐ถ) โ โ) |
21 | 20 | 3adant1 1127 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โ (๐ต ยท ๐ถ) โ โ) |
22 | 21 | adantr 479 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ (๐ต ยท ๐ถ) โ
โ) |
23 | 22, 5 | modcld 13867 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ((๐ต ยท ๐ถ) mod ๐) โ โ) |
24 | | simp1 1133 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โ ๐ด โ
โ) |
25 | 24 | anim1i 613 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ (๐ด โ โ
โง ๐ โ
โ+)) |
26 | | simpl3 1190 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ๐ถ โ
โค) |
27 | | modmulmod 13928 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โค โง ๐ โ โ+)
โ (((๐ต mod ๐) ยท ๐ถ) mod ๐) = ((๐ต ยท ๐ถ) mod ๐)) |
28 | 4, 26, 5, 27 | syl3anc 1368 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ (((๐ต mod ๐) ยท ๐ถ) mod ๐) = ((๐ต ยท ๐ถ) mod ๐)) |
29 | | remulcl 11218 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยท ๐ถ) โ โ) |
30 | 14, 29 | sylan2 591 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โค) โ (๐ต ยท ๐ถ) โ โ) |
31 | 30 | 3adant1 1127 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โ (๐ต ยท ๐ถ) โ โ) |
32 | | modabs2 13897 |
. . . . 5
โข (((๐ต ยท ๐ถ) โ โ โง ๐ โ โ+) โ (((๐ต ยท ๐ถ) mod ๐) mod ๐) = ((๐ต ยท ๐ถ) mod ๐)) |
33 | 31, 32 | sylan 578 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ (((๐ต ยท ๐ถ) mod ๐) mod ๐) = ((๐ต ยท ๐ถ) mod ๐)) |
34 | 28, 33 | eqtr4d 2768 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ (((๐ต mod ๐) ยท ๐ถ) mod ๐) = (((๐ต ยท ๐ถ) mod ๐) mod ๐)) |
35 | | modadd1 13900 |
. . 3
โข
(((((๐ต mod ๐) ยท ๐ถ) โ โ โง ((๐ต ยท ๐ถ) mod ๐) โ โ) โง (๐ด โ โ โง ๐ โ โ+) โง (((๐ต mod ๐) ยท ๐ถ) mod ๐) = (((๐ต ยท ๐ถ) mod ๐) mod ๐)) โ ((((๐ต mod ๐) ยท ๐ถ) + ๐ด) mod ๐) = ((((๐ต ยท ๐ถ) mod ๐) + ๐ด) mod ๐)) |
36 | 17, 23, 25, 34, 35 | syl211anc 1373 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ((((๐ต mod ๐) ยท ๐ถ) + ๐ด) mod ๐) = ((((๐ต ยท ๐ถ) mod ๐) + ๐ด) mod ๐)) |
37 | 31 | adantr 479 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ (๐ต ยท ๐ถ) โ
โ) |
38 | 24 | adantr 479 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ๐ด โ
โ) |
39 | | modaddmod 13902 |
. . . 4
โข (((๐ต ยท ๐ถ) โ โ โง ๐ด โ โ โง ๐ โ โ+) โ
((((๐ต ยท ๐ถ) mod ๐) + ๐ด) mod ๐) = (((๐ต ยท ๐ถ) + ๐ด) mod ๐)) |
40 | 37, 38, 5, 39 | syl3anc 1368 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ((((๐ต ยท ๐ถ) mod ๐) + ๐ด) mod ๐) = (((๐ต ยท ๐ถ) + ๐ด) mod ๐)) |
41 | | recn 11223 |
. . . . . . . 8
โข (๐ต โ โ โ ๐ต โ
โ) |
42 | | mulcl 11217 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยท ๐ถ) โ โ) |
43 | 41, 8, 42 | syl2an 594 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ถ โ โค) โ (๐ต ยท ๐ถ) โ โ) |
44 | 43 | 3adant1 1127 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โ (๐ต ยท ๐ถ) โ โ) |
45 | 44, 2 | addcomd 11441 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โ ((๐ต ยท ๐ถ) + ๐ด) = (๐ด + (๐ต ยท ๐ถ))) |
46 | 45 | adantr 479 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ((๐ต ยท ๐ถ) + ๐ด) = (๐ด + (๐ต ยท ๐ถ))) |
47 | 46 | oveq1d 7428 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ (((๐ต ยท ๐ถ) + ๐ด) mod ๐) = ((๐ด + (๐ต ยท ๐ถ)) mod ๐)) |
48 | 40, 47 | eqtrd 2765 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ((((๐ต ยท ๐ถ) mod ๐) + ๐ด) mod ๐) = ((๐ด + (๐ต ยท ๐ถ)) mod ๐)) |
49 | 13, 36, 48 | 3eqtrd 2769 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โค) โง ๐ โ โ+)
โ ((๐ด + ((๐ต mod ๐) ยท ๐ถ)) mod ๐) = ((๐ด + (๐ต ยท ๐ถ)) mod ๐)) |