Step | Hyp | Ref
| Expression |
1 | | oveq1 7416 |
. . 3
โข ((๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด)) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) |
2 | | simp2l 1200 |
. . . . . . . . 9
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ โ
โ0) |
3 | 2 | nn0zd 12584 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ โ
โค) |
4 | | simp3 1139 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ (๐โ๐ด) โ โ) |
5 | 3, 4 | zmodcld 13857 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) โ
โ0) |
6 | 5 | adantr 482 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐ mod (๐โ๐ด)) โ
โ0) |
7 | 6 | nn0red 12533 |
. . . . 5
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐ mod (๐โ๐ด)) โ โ) |
8 | | simp2r 1201 |
. . . . . . . . 9
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ โ
โ0) |
9 | 8 | nn0zd 12584 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ โ
โค) |
10 | 9, 4 | zmodcld 13857 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) โ
โ0) |
11 | 10 | adantr 482 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐ mod (๐โ๐ด)) โ
โ0) |
12 | 11 | nn0red 12533 |
. . . . 5
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐ mod (๐โ๐ด)) โ โ) |
13 | | odcl.1 |
. . . . . 6
โข ๐ = (Baseโ๐บ) |
14 | | odcl.2 |
. . . . . 6
โข ๐ = (odโ๐บ) |
15 | | odid.3 |
. . . . . 6
โข ยท =
(.gโ๐บ) |
16 | | odid.4 |
. . . . . 6
โข 0 =
(0gโ๐บ) |
17 | | simp1l 1198 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐บ โ Mnd) |
18 | 17 | adantr 482 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ ๐บ โ Mnd) |
19 | | simp1r 1199 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ด โ ๐) |
20 | 19 | adantr 482 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ ๐ด โ ๐) |
21 | 4 | adantr 482 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐โ๐ด) โ โ) |
22 | 2 | nn0red 12533 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ โ
โ) |
23 | 4 | nnrpd 13014 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ (๐โ๐ด) โ
โ+) |
24 | | modlt 13845 |
. . . . . . . 8
โข ((๐ โ โ โง (๐โ๐ด) โ โ+) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
25 | 22, 23, 24 | syl2anc 585 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
26 | 25 | adantr 482 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
27 | 8 | nn0red 12533 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ โ
โ) |
28 | | modlt 13845 |
. . . . . . . 8
โข ((๐ โ โ โง (๐โ๐ด) โ โ+) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
29 | 27, 23, 28 | syl2anc 585 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
30 | 29 | adantr 482 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
31 | | simpr 486 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) |
32 | 13, 14, 15, 16, 18, 20, 21, 6, 11, 26, 30, 31 | mndodconglem 19409 |
. . . . 5
โข
(((((๐บ โ Mnd
โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โง (๐ mod (๐โ๐ด)) โค (๐ mod (๐โ๐ด))) โ (๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด))) |
33 | 31 | eqcomd 2739 |
. . . . . . 7
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) |
34 | 13, 14, 15, 16, 18, 20, 21, 11, 6, 30, 26, 33 | mndodconglem 19409 |
. . . . . 6
โข
(((((๐บ โ Mnd
โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โง (๐ mod (๐โ๐ด)) โค (๐ mod (๐โ๐ด))) โ (๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด))) |
35 | 34 | eqcomd 2739 |
. . . . 5
โข
(((((๐บ โ Mnd
โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โง (๐ mod (๐โ๐ด)) โค (๐ mod (๐โ๐ด))) โ (๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด))) |
36 | 7, 12, 32, 35 | lecasei 11320 |
. . . 4
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด))) |
37 | 36 | ex 414 |
. . 3
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ
(((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด) โ (๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด)))) |
38 | 1, 37 | impbid2 225 |
. 2
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด)) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด))) |
39 | | moddvds 16208 |
. . 3
โข (((๐โ๐ด) โ โ โง ๐ โ โค โง ๐ โ โค) โ ((๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด)) โ (๐โ๐ด) โฅ (๐ โ ๐))) |
40 | 4, 3, 9, 39 | syl3anc 1372 |
. 2
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด)) โ (๐โ๐ด) โฅ (๐ โ ๐))) |
41 | 13, 14, 15, 16 | odmodnn0 19408 |
. . . 4
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = (๐ ยท ๐ด)) |
42 | 17, 19, 2, 4, 41 | syl31anc 1374 |
. . 3
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = (๐ ยท ๐ด)) |
43 | 13, 14, 15, 16 | odmodnn0 19408 |
. . . 4
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = (๐ ยท ๐ด)) |
44 | 17, 19, 8, 4, 43 | syl31anc 1374 |
. . 3
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = (๐ ยท ๐ด)) |
45 | 42, 44 | eqeq12d 2749 |
. 2
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ
(((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด) โ (๐ ยท ๐ด) = (๐ ยท ๐ด))) |
46 | 38, 40, 45 | 3bitr3d 309 |
1
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ((๐โ๐ด) โฅ (๐ โ ๐) โ (๐ ยท ๐ด) = (๐ ยท ๐ด))) |