Step | Hyp | Ref
| Expression |
1 | | modval 13839 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ท โ โ+)
โ (๐ด mod ๐ท) = (๐ด โ (๐ท ยท (โโ(๐ด / ๐ท))))) |
2 | | modval 13839 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ท โ โ+)
โ (๐ต mod ๐ท) = (๐ต โ (๐ท ยท (โโ(๐ต / ๐ท))))) |
3 | 1, 2 | eqeqan12d 2740 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ท โ โ+)
โง (๐ต โ โ
โง ๐ท โ
โ+)) โ ((๐ด mod ๐ท) = (๐ต mod ๐ท) โ (๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) = (๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))))) |
4 | 3 | anandirs 676 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ท โ โ+)
โ ((๐ด mod ๐ท) = (๐ต mod ๐ท) โ (๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) = (๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))))) |
5 | 4 | adantrl 713 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ+))
โ ((๐ด mod ๐ท) = (๐ต mod ๐ท) โ (๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) = (๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))))) |
6 | | oveq1 7411 |
. . . . 5
โข ((๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) = (๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))) โ ((๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) + ๐ถ) = ((๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))) + ๐ถ)) |
7 | 5, 6 | biimtrdi 252 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ+))
โ ((๐ด mod ๐ท) = (๐ต mod ๐ท) โ ((๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) + ๐ถ) = ((๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))) + ๐ถ))) |
8 | | recn 11199 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ
โ) |
9 | 8 | adantr 480 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ ๐ด โ
โ) |
10 | | recn 11199 |
. . . . . . . 8
โข (๐ถ โ โ โ ๐ถ โ
โ) |
11 | 10 | ad2antrl 725 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ ๐ถ โ
โ) |
12 | | rpcn 12987 |
. . . . . . . . . 10
โข (๐ท โ โ+
โ ๐ท โ
โ) |
13 | 12 | adantl 481 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ท โ โ+)
โ ๐ท โ
โ) |
14 | | rerpdivcl 13007 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ท โ โ+)
โ (๐ด / ๐ท) โ
โ) |
15 | | reflcl 13764 |
. . . . . . . . . . 11
โข ((๐ด / ๐ท) โ โ โ
(โโ(๐ด / ๐ท)) โ
โ) |
16 | 15 | recnd 11243 |
. . . . . . . . . 10
โข ((๐ด / ๐ท) โ โ โ
(โโ(๐ด / ๐ท)) โ
โ) |
17 | 14, 16 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ท โ โ+)
โ (โโ(๐ด /
๐ท)) โ
โ) |
18 | 13, 17 | mulcld 11235 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ท โ โ+)
โ (๐ท ยท
(โโ(๐ด / ๐ท))) โ
โ) |
19 | 18 | adantrl 713 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ (๐ท ยท
(โโ(๐ด / ๐ท))) โ
โ) |
20 | 9, 11, 19 | addsubd 11593 |
. . . . . 6
โข ((๐ด โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ ((๐ด + ๐ถ) โ (๐ท ยท (โโ(๐ด / ๐ท)))) = ((๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) + ๐ถ)) |
21 | 20 | adantlr 712 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ+))
โ ((๐ด + ๐ถ) โ (๐ท ยท (โโ(๐ด / ๐ท)))) = ((๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) + ๐ถ)) |
22 | | recn 11199 |
. . . . . . . 8
โข (๐ต โ โ โ ๐ต โ
โ) |
23 | 22 | adantr 480 |
. . . . . . 7
โข ((๐ต โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ ๐ต โ
โ) |
24 | 10 | ad2antrl 725 |
. . . . . . 7
โข ((๐ต โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ ๐ถ โ
โ) |
25 | 12 | adantl 481 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ท โ โ+)
โ ๐ท โ
โ) |
26 | | rerpdivcl 13007 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ท โ โ+)
โ (๐ต / ๐ท) โ
โ) |
27 | | reflcl 13764 |
. . . . . . . . . . 11
โข ((๐ต / ๐ท) โ โ โ
(โโ(๐ต / ๐ท)) โ
โ) |
28 | 27 | recnd 11243 |
. . . . . . . . . 10
โข ((๐ต / ๐ท) โ โ โ
(โโ(๐ต / ๐ท)) โ
โ) |
29 | 26, 28 | syl 17 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ท โ โ+)
โ (โโ(๐ต /
๐ท)) โ
โ) |
30 | 25, 29 | mulcld 11235 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ท โ โ+)
โ (๐ท ยท
(โโ(๐ต / ๐ท))) โ
โ) |
31 | 30 | adantrl 713 |
. . . . . . 7
โข ((๐ต โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ (๐ท ยท
(โโ(๐ต / ๐ท))) โ
โ) |
32 | 23, 24, 31 | addsubd 11593 |
. . . . . 6
โข ((๐ต โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ ((๐ต + ๐ถ) โ (๐ท ยท (โโ(๐ต / ๐ท)))) = ((๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))) + ๐ถ)) |
33 | 32 | adantll 711 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ+))
โ ((๐ต + ๐ถ) โ (๐ท ยท (โโ(๐ต / ๐ท)))) = ((๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))) + ๐ถ)) |
34 | 21, 33 | eqeq12d 2742 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ+))
โ (((๐ด + ๐ถ) โ (๐ท ยท (โโ(๐ด / ๐ท)))) = ((๐ต + ๐ถ) โ (๐ท ยท (โโ(๐ต / ๐ท)))) โ ((๐ด โ (๐ท ยท (โโ(๐ด / ๐ท)))) + ๐ถ) = ((๐ต โ (๐ท ยท (โโ(๐ต / ๐ท)))) + ๐ถ))) |
35 | 7, 34 | sylibrd 259 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ+))
โ ((๐ด mod ๐ท) = (๐ต mod ๐ท) โ ((๐ด + ๐ถ) โ (๐ท ยท (โโ(๐ด / ๐ท)))) = ((๐ต + ๐ถ) โ (๐ท ยท (โโ(๐ต / ๐ท)))))) |
36 | | oveq1 7411 |
. . . 4
โข (((๐ด + ๐ถ) โ (๐ท ยท (โโ(๐ด / ๐ท)))) = ((๐ต + ๐ถ) โ (๐ท ยท (โโ(๐ต / ๐ท)))) โ (((๐ด + ๐ถ) โ (๐ท ยท (โโ(๐ด / ๐ท)))) mod ๐ท) = (((๐ต + ๐ถ) โ (๐ท ยท (โโ(๐ต / ๐ท)))) mod ๐ท)) |
37 | | readdcl 11192 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด + ๐ถ) โ โ) |
38 | 37 | adantrr 714 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ (๐ด + ๐ถ) โ
โ) |
39 | | simprr 770 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ ๐ท โ
โ+) |
40 | 14 | flcld 13766 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ท โ โ+)
โ (โโ(๐ด /
๐ท)) โ
โค) |
41 | 40 | adantrl 713 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ (โโ(๐ด /
๐ท)) โ
โค) |
42 | | modcyc2 13875 |
. . . . . . 7
โข (((๐ด + ๐ถ) โ โ โง ๐ท โ โ+ โง
(โโ(๐ด / ๐ท)) โ โค) โ
(((๐ด + ๐ถ) โ (๐ท ยท (โโ(๐ด / ๐ท)))) mod ๐ท) = ((๐ด + ๐ถ) mod ๐ท)) |
43 | 38, 39, 41, 42 | syl3anc 1368 |
. . . . . 6
โข ((๐ด โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ (((๐ด + ๐ถ) โ (๐ท ยท (โโ(๐ด / ๐ท)))) mod ๐ท) = ((๐ด + ๐ถ) mod ๐ท)) |
44 | 43 | adantlr 712 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ+))
โ (((๐ด + ๐ถ) โ (๐ท ยท (โโ(๐ด / ๐ท)))) mod ๐ท) = ((๐ด + ๐ถ) mod ๐ท)) |
45 | | readdcl 11192 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต + ๐ถ) โ โ) |
46 | 45 | adantrr 714 |
. . . . . . 7
โข ((๐ต โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ (๐ต + ๐ถ) โ
โ) |
47 | | simprr 770 |
. . . . . . 7
โข ((๐ต โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ ๐ท โ
โ+) |
48 | 26 | flcld 13766 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ท โ โ+)
โ (โโ(๐ต /
๐ท)) โ
โค) |
49 | 48 | adantrl 713 |
. . . . . . 7
โข ((๐ต โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ (โโ(๐ต /
๐ท)) โ
โค) |
50 | | modcyc2 13875 |
. . . . . . 7
โข (((๐ต + ๐ถ) โ โ โง ๐ท โ โ+ โง
(โโ(๐ต / ๐ท)) โ โค) โ
(((๐ต + ๐ถ) โ (๐ท ยท (โโ(๐ต / ๐ท)))) mod ๐ท) = ((๐ต + ๐ถ) mod ๐ท)) |
51 | 46, 47, 49, 50 | syl3anc 1368 |
. . . . . 6
โข ((๐ต โ โ โง (๐ถ โ โ โง ๐ท โ โ+))
โ (((๐ต + ๐ถ) โ (๐ท ยท (โโ(๐ต / ๐ท)))) mod ๐ท) = ((๐ต + ๐ถ) mod ๐ท)) |
52 | 51 | adantll 711 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ+))
โ (((๐ต + ๐ถ) โ (๐ท ยท (โโ(๐ต / ๐ท)))) mod ๐ท) = ((๐ต + ๐ถ) mod ๐ท)) |
53 | 44, 52 | eqeq12d 2742 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ+))
โ ((((๐ด + ๐ถ) โ (๐ท ยท (โโ(๐ด / ๐ท)))) mod ๐ท) = (((๐ต + ๐ถ) โ (๐ท ยท (โโ(๐ต / ๐ท)))) mod ๐ท) โ ((๐ด + ๐ถ) mod ๐ท) = ((๐ต + ๐ถ) mod ๐ท))) |
54 | 36, 53 | imbitrid 243 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ+))
โ (((๐ด + ๐ถ) โ (๐ท ยท (โโ(๐ด / ๐ท)))) = ((๐ต + ๐ถ) โ (๐ท ยท (โโ(๐ต / ๐ท)))) โ ((๐ด + ๐ถ) mod ๐ท) = ((๐ต + ๐ถ) mod ๐ท))) |
55 | 35, 54 | syld 47 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ+))
โ ((๐ด mod ๐ท) = (๐ต mod ๐ท) โ ((๐ด + ๐ถ) mod ๐ท) = ((๐ต + ๐ถ) mod ๐ท))) |
56 | 55 | 3impia 1114 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ+)
โง (๐ด mod ๐ท) = (๐ต mod ๐ท)) โ ((๐ด + ๐ถ) mod ๐ท) = ((๐ต + ๐ถ) mod ๐ท)) |