Step | Hyp | Ref
| Expression |
1 | | simpl1 1189 |
. . . 4
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ๐บ โ Mnd) |
2 | | nnnn0 12483 |
. . . . . 6
โข ((๐โ๐ด) โ โ โ (๐โ๐ด) โ
โ0) |
3 | 2 | adantl 480 |
. . . . 5
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ (๐โ๐ด) โ
โ0) |
4 | | simpl3 1191 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ๐ โ
โ0) |
5 | 4 | nn0red 12537 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ๐ โ โ) |
6 | | nnrp 12989 |
. . . . . . . 8
โข ((๐โ๐ด) โ โ โ (๐โ๐ด) โ
โ+) |
7 | 6 | adantl 480 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ (๐โ๐ด) โ
โ+) |
8 | 5, 7 | rerpdivcld 13051 |
. . . . . 6
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ (๐ / (๐โ๐ด)) โ โ) |
9 | 4 | nn0ge0d 12539 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ 0 โค ๐) |
10 | | nnre 12223 |
. . . . . . . 8
โข ((๐โ๐ด) โ โ โ (๐โ๐ด) โ โ) |
11 | 10 | adantl 480 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ (๐โ๐ด) โ โ) |
12 | | nngt0 12247 |
. . . . . . . 8
โข ((๐โ๐ด) โ โ โ 0 < (๐โ๐ด)) |
13 | 12 | adantl 480 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ 0 < (๐โ๐ด)) |
14 | | divge0 12087 |
. . . . . . 7
โข (((๐ โ โ โง 0 โค
๐) โง ((๐โ๐ด) โ โ โง 0 < (๐โ๐ด))) โ 0 โค (๐ / (๐โ๐ด))) |
15 | 5, 9, 11, 13, 14 | syl22anc 835 |
. . . . . 6
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ 0 โค (๐ / (๐โ๐ด))) |
16 | | flge0nn0 13789 |
. . . . . 6
โข (((๐ / (๐โ๐ด)) โ โ โง 0 โค (๐ / (๐โ๐ด))) โ (โโ(๐ / (๐โ๐ด))) โ
โ0) |
17 | 8, 15, 16 | syl2anc 582 |
. . . . 5
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ
(โโ(๐ / (๐โ๐ด))) โ
โ0) |
18 | 3, 17 | nn0mulcld 12541 |
. . . 4
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) โ
โ0) |
19 | 4 | nn0zd 12588 |
. . . . 5
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ๐ โ โค) |
20 | | zmodcl 13860 |
. . . . 5
โข ((๐ โ โค โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) โ
โ0) |
21 | 19, 20 | sylancom 586 |
. . . 4
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) โ
โ0) |
22 | | simpl2 1190 |
. . . 4
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ๐ด โ ๐) |
23 | | odcl.1 |
. . . . 5
โข ๐ = (Baseโ๐บ) |
24 | | odid.3 |
. . . . 5
โข ยท =
(.gโ๐บ) |
25 | | eqid 2730 |
. . . . 5
โข
(+gโ๐บ) = (+gโ๐บ) |
26 | 23, 24, 25 | mulgnn0dir 19020 |
. . . 4
โข ((๐บ โ Mnd โง (((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) โ โ0 โง (๐ mod (๐โ๐ด)) โ โ0 โง ๐ด โ ๐)) โ ((((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) + (๐ mod (๐โ๐ด))) ยท ๐ด) = ((((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) ยท ๐ด)(+gโ๐บ)((๐ mod (๐โ๐ด)) ยท ๐ด))) |
27 | 1, 18, 21, 22, 26 | syl13anc 1370 |
. . 3
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) + (๐ mod (๐โ๐ด))) ยท ๐ด) = ((((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) ยท ๐ด)(+gโ๐บ)((๐ mod (๐โ๐ด)) ยท ๐ด))) |
28 | 11 | recnd 11246 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ (๐โ๐ด) โ โ) |
29 | 17 | nn0cnd 12538 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ
(โโ(๐ / (๐โ๐ด))) โ โ) |
30 | 28, 29 | mulcomd 11239 |
. . . . . 6
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) = ((โโ(๐ / (๐โ๐ด))) ยท (๐โ๐ด))) |
31 | 30 | oveq1d 7426 |
. . . . 5
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ (((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) ยท ๐ด) = (((โโ(๐ / (๐โ๐ด))) ยท (๐โ๐ด)) ยท ๐ด)) |
32 | 23, 24 | mulgnn0ass 19026 |
. . . . . . 7
โข ((๐บ โ Mnd โง
((โโ(๐ / (๐โ๐ด))) โ โ0 โง (๐โ๐ด) โ โ0 โง ๐ด โ ๐)) โ (((โโ(๐ / (๐โ๐ด))) ยท (๐โ๐ด)) ยท ๐ด) = ((โโ(๐ / (๐โ๐ด))) ยท ((๐โ๐ด) ยท ๐ด))) |
33 | 1, 17, 3, 22, 32 | syl13anc 1370 |
. . . . . 6
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ
(((โโ(๐ /
(๐โ๐ด))) ยท (๐โ๐ด)) ยท ๐ด) = ((โโ(๐ / (๐โ๐ด))) ยท ((๐โ๐ด) ยท ๐ด))) |
34 | | odcl.2 |
. . . . . . . . . 10
โข ๐ = (odโ๐บ) |
35 | | odid.4 |
. . . . . . . . . 10
โข 0 =
(0gโ๐บ) |
36 | 23, 34, 24, 35 | odid 19447 |
. . . . . . . . 9
โข (๐ด โ ๐ โ ((๐โ๐ด) ยท ๐ด) = 0 ) |
37 | 22, 36 | syl 17 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((๐โ๐ด) ยท ๐ด) = 0 ) |
38 | 37 | oveq2d 7427 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ
((โโ(๐ / (๐โ๐ด))) ยท ((๐โ๐ด) ยท ๐ด)) = ((โโ(๐ / (๐โ๐ด))) ยท 0 )) |
39 | 23, 24, 35 | mulgnn0z 19017 |
. . . . . . . 8
โข ((๐บ โ Mnd โง
(โโ(๐ / (๐โ๐ด))) โ โ0) โ
((โโ(๐ / (๐โ๐ด))) ยท 0 ) = 0 ) |
40 | 1, 17, 39 | syl2anc 582 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ
((โโ(๐ / (๐โ๐ด))) ยท 0 ) = 0 ) |
41 | 38, 40 | eqtrd 2770 |
. . . . . 6
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ
((โโ(๐ / (๐โ๐ด))) ยท ((๐โ๐ด) ยท ๐ด)) = 0 ) |
42 | 33, 41 | eqtrd 2770 |
. . . . 5
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ
(((โโ(๐ /
(๐โ๐ด))) ยท (๐โ๐ด)) ยท ๐ด) = 0 ) |
43 | 31, 42 | eqtrd 2770 |
. . . 4
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ (((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) ยท ๐ด) = 0 ) |
44 | 43 | oveq1d 7426 |
. . 3
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) ยท ๐ด)(+gโ๐บ)((๐ mod (๐โ๐ด)) ยท ๐ด)) = ( 0 (+gโ๐บ)((๐ mod (๐โ๐ด)) ยท ๐ด))) |
45 | 27, 44 | eqtrd 2770 |
. 2
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) + (๐ mod (๐โ๐ด))) ยท ๐ด) = ( 0 (+gโ๐บ)((๐ mod (๐โ๐ด)) ยท ๐ด))) |
46 | | modval 13840 |
. . . . . 6
โข ((๐ โ โ โง (๐โ๐ด) โ โ+) โ (๐ mod (๐โ๐ด)) = (๐ โ ((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))))) |
47 | 5, 7, 46 | syl2anc 582 |
. . . . 5
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) = (๐ โ ((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))))) |
48 | 47 | oveq2d 7427 |
. . . 4
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ (((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) + (๐ mod (๐โ๐ด))) = (((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) + (๐ โ ((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด))))))) |
49 | 18 | nn0cnd 12538 |
. . . . 5
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) โ โ) |
50 | 4 | nn0cnd 12538 |
. . . . 5
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ๐ โ โ) |
51 | 49, 50 | pncan3d 11578 |
. . . 4
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ (((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) + (๐ โ ((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))))) = ๐) |
52 | 48, 51 | eqtrd 2770 |
. . 3
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ (((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) + (๐ mod (๐โ๐ด))) = ๐) |
53 | 52 | oveq1d 7426 |
. 2
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((((๐โ๐ด) ยท (โโ(๐ / (๐โ๐ด)))) + (๐ mod (๐โ๐ด))) ยท ๐ด) = (๐ ยท ๐ด)) |
54 | 23, 24, 1, 21, 22 | mulgnn0cld 19011 |
. . 3
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) โ ๐) |
55 | 23, 25, 35 | mndlid 18679 |
. . 3
โข ((๐บ โ Mnd โง ((๐ mod (๐โ๐ด)) ยท ๐ด) โ ๐) โ ( 0 (+gโ๐บ)((๐ mod (๐โ๐ด)) ยท ๐ด)) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) |
56 | 1, 54, 55 | syl2anc 582 |
. 2
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ( 0
(+gโ๐บ)((๐ mod (๐โ๐ด)) ยท ๐ด)) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) |
57 | 45, 53, 56 | 3eqtr3rd 2779 |
1
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = (๐ ยท ๐ด)) |