Step | Hyp | Ref
| Expression |
1 | | oveq1 7418 |
. . 3
โข ((๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด)) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) |
2 | | simp2l 1197 |
. . . . . . . . 9
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ โ
โ0) |
3 | 2 | nn0zd 12588 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ โ
โค) |
4 | | simp3 1136 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ (๐โ๐ด) โ โ) |
5 | 3, 4 | zmodcld 13861 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) โ
โ0) |
6 | 5 | adantr 479 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐ mod (๐โ๐ด)) โ
โ0) |
7 | 6 | nn0red 12537 |
. . . . 5
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐ mod (๐โ๐ด)) โ โ) |
8 | | simp2r 1198 |
. . . . . . . . 9
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ โ
โ0) |
9 | 8 | nn0zd 12588 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ โ
โค) |
10 | 9, 4 | zmodcld 13861 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) โ
โ0) |
11 | 10 | adantr 479 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐ mod (๐โ๐ด)) โ
โ0) |
12 | 11 | nn0red 12537 |
. . . . 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 1195 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐บ โ Mnd) |
18 | 17 | adantr 479 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ ๐บ โ Mnd) |
19 | | simp1r 1196 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ด โ ๐) |
20 | 19 | adantr 479 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ ๐ด โ ๐) |
21 | 4 | adantr 479 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐โ๐ด) โ โ) |
22 | 2 | nn0red 12537 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ โ
โ) |
23 | 4 | nnrpd 13018 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ (๐โ๐ด) โ
โ+) |
24 | | modlt 13849 |
. . . . . . . 8
โข ((๐ โ โ โง (๐โ๐ด) โ โ+) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
25 | 22, 23, 24 | syl2anc 582 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
26 | 25 | adantr 479 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
27 | 8 | nn0red 12537 |
. . . . . . . 8
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ๐ โ
โ) |
28 | | modlt 13849 |
. . . . . . . 8
โข ((๐ โ โ โง (๐โ๐ด) โ โ+) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
29 | 27, 23, 28 | syl2anc 582 |
. . . . . . 7
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
30 | 29 | adantr 479 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
31 | | simpr 483 |
. . . . . 6
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) |
32 | 13, 14, 15, 16, 18, 20, 21, 6, 11, 26, 30, 31 | mndodconglem 19450 |
. . . . 5
โข
(((((๐บ โ Mnd
โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โง (๐ mod (๐โ๐ด)) โค (๐ mod (๐โ๐ด))) โ (๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด))) |
33 | 31 | eqcomd 2736 |
. . . . . . 7
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) |
34 | 13, 14, 15, 16, 18, 20, 21, 11, 6, 30, 26, 33 | mndodconglem 19450 |
. . . . . 6
โข
(((((๐บ โ Mnd
โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โง (๐ mod (๐โ๐ด)) โค (๐ mod (๐โ๐ด))) โ (๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด))) |
35 | 34 | eqcomd 2736 |
. . . . 5
โข
(((((๐บ โ Mnd
โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โง (๐ mod (๐โ๐ด)) โค (๐ mod (๐โ๐ด))) โ (๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด))) |
36 | 7, 12, 32, 35 | lecasei 11324 |
. . . 4
โข ((((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด)) โ (๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด))) |
37 | 36 | ex 411 |
. . 3
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ
(((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด) โ (๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด)))) |
38 | 1, 37 | impbid2 225 |
. 2
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด)) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด))) |
39 | | moddvds 16212 |
. . 3
โข (((๐โ๐ด) โ โ โง ๐ โ โค โง ๐ โ โค) โ ((๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด)) โ (๐โ๐ด) โฅ (๐ โ ๐))) |
40 | 4, 3, 9, 39 | syl3anc 1369 |
. 2
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) = (๐ mod (๐โ๐ด)) โ (๐โ๐ด) โฅ (๐ โ ๐))) |
41 | 13, 14, 15, 16 | odmodnn0 19449 |
. . . 4
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = (๐ ยท ๐ด)) |
42 | 17, 19, 2, 4, 41 | syl31anc 1371 |
. . 3
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = (๐ ยท ๐ด)) |
43 | 13, 14, 15, 16 | odmodnn0 19449 |
. . . 4
โข (((๐บ โ Mnd โง ๐ด โ ๐ โง ๐ โ โ0) โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = (๐ ยท ๐ด)) |
44 | 17, 19, 8, 4, 43 | syl31anc 1371 |
. . 3
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = (๐ ยท ๐ด)) |
45 | 42, 44 | eqeq12d 2746 |
. 2
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ
(((๐ mod (๐โ๐ด)) ยท ๐ด) = ((๐ mod (๐โ๐ด)) ยท ๐ด) โ (๐ ยท ๐ด) = (๐ ยท ๐ด))) |
46 | 38, 40, 45 | 3bitr3d 308 |
1
โข (((๐บ โ Mnd โง ๐ด โ ๐) โง (๐ โ โ0 โง ๐ โ โ0)
โง (๐โ๐ด) โ โ) โ ((๐โ๐ด) โฅ (๐ โ ๐) โ (๐ ยท ๐ด) = (๐ ยท ๐ด))) |