Step | Hyp | Ref
| Expression |
1 | | mndodconglem.2 |
. . . . . . 7
โข (๐ โ ๐ด โ ๐) |
2 | | mndodconglem.3 |
. . . . . . . . . . 11
โข (๐ โ (๐โ๐ด) โ โ) |
3 | 2 | nnred 12227 |
. . . . . . . . . 10
โข (๐ โ (๐โ๐ด) โ โ) |
4 | 3 | recnd 11242 |
. . . . . . . . 9
โข (๐ โ (๐โ๐ด) โ โ) |
5 | | mndodconglem.4 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ
โ0) |
6 | 5 | nn0red 12533 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
7 | 6 | recnd 11242 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
8 | | mndodconglem.5 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ
โ0) |
9 | 8 | nn0red 12533 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
10 | 9 | recnd 11242 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
11 | 4, 7, 10 | addsubassd 11591 |
. . . . . . . 8
โข (๐ โ (((๐โ๐ด) + ๐) โ ๐) = ((๐โ๐ด) + (๐ โ ๐))) |
12 | 2 | nnzd 12585 |
. . . . . . . . . . . 12
โข (๐ โ (๐โ๐ด) โ โค) |
13 | 5 | nn0zd 12584 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โค) |
14 | 12, 13 | zaddcld 12670 |
. . . . . . . . . . 11
โข (๐ โ ((๐โ๐ด) + ๐) โ โค) |
15 | 14 | zred 12666 |
. . . . . . . . . 10
โข (๐ โ ((๐โ๐ด) + ๐) โ โ) |
16 | | mndodconglem.7 |
. . . . . . . . . 10
โข (๐ โ ๐ < (๐โ๐ด)) |
17 | | nn0addge1 12518 |
. . . . . . . . . . 11
โข (((๐โ๐ด) โ โ โง ๐ โ โ0) โ (๐โ๐ด) โค ((๐โ๐ด) + ๐)) |
18 | 3, 5, 17 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ (๐โ๐ด) โค ((๐โ๐ด) + ๐)) |
19 | 9, 3, 15, 16, 18 | ltletrd 11374 |
. . . . . . . . 9
โข (๐ โ ๐ < ((๐โ๐ด) + ๐)) |
20 | 8 | nn0zd 12584 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โค) |
21 | | znnsub 12608 |
. . . . . . . . . 10
โข ((๐ โ โค โง ((๐โ๐ด) + ๐) โ โค) โ (๐ < ((๐โ๐ด) + ๐) โ (((๐โ๐ด) + ๐) โ ๐) โ โ)) |
22 | 20, 14, 21 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (๐ < ((๐โ๐ด) + ๐) โ (((๐โ๐ด) + ๐) โ ๐) โ โ)) |
23 | 19, 22 | mpbid 231 |
. . . . . . . 8
โข (๐ โ (((๐โ๐ด) + ๐) โ ๐) โ โ) |
24 | 11, 23 | eqeltrrd 2835 |
. . . . . . 7
โข (๐ โ ((๐โ๐ด) + (๐ โ ๐)) โ โ) |
25 | 4, 7, 10 | addsub12d 11594 |
. . . . . . . . 9
โข (๐ โ ((๐โ๐ด) + (๐ โ ๐)) = (๐ + ((๐โ๐ด) โ ๐))) |
26 | 25 | oveq1d 7424 |
. . . . . . . 8
โข (๐ โ (((๐โ๐ด) + (๐ โ ๐)) ยท ๐ด) = ((๐ + ((๐โ๐ด) โ ๐)) ยท ๐ด)) |
27 | | mndodconglem.8 |
. . . . . . . . . . 11
โข (๐ โ (๐ ยท ๐ด) = (๐ ยท ๐ด)) |
28 | 27 | oveq1d 7424 |
. . . . . . . . . 10
โข (๐ โ ((๐ ยท ๐ด)(+gโ๐บ)(((๐โ๐ด) โ ๐) ยท ๐ด)) = ((๐ ยท ๐ด)(+gโ๐บ)(((๐โ๐ด) โ ๐) ยท ๐ด))) |
29 | | mndodconglem.1 |
. . . . . . . . . . 11
โข (๐ โ ๐บ โ Mnd) |
30 | | znnsub 12608 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง (๐โ๐ด) โ โค) โ (๐ < (๐โ๐ด) โ ((๐โ๐ด) โ ๐) โ โ)) |
31 | 20, 12, 30 | syl2anc 585 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ < (๐โ๐ด) โ ((๐โ๐ด) โ ๐) โ โ)) |
32 | 16, 31 | mpbid 231 |
. . . . . . . . . . . 12
โข (๐ โ ((๐โ๐ด) โ ๐) โ โ) |
33 | 32 | nnnn0d 12532 |
. . . . . . . . . . 11
โข (๐ โ ((๐โ๐ด) โ ๐) โ
โ0) |
34 | | odcl.1 |
. . . . . . . . . . . 12
โข ๐ = (Baseโ๐บ) |
35 | | odid.3 |
. . . . . . . . . . . 12
โข ยท =
(.gโ๐บ) |
36 | | eqid 2733 |
. . . . . . . . . . . 12
โข
(+gโ๐บ) = (+gโ๐บ) |
37 | 34, 35, 36 | mulgnn0dir 18984 |
. . . . . . . . . . 11
โข ((๐บ โ Mnd โง (๐ โ โ0
โง ((๐โ๐ด) โ ๐) โ โ0 โง ๐ด โ ๐)) โ ((๐ + ((๐โ๐ด) โ ๐)) ยท ๐ด) = ((๐ ยท ๐ด)(+gโ๐บ)(((๐โ๐ด) โ ๐) ยท ๐ด))) |
38 | 29, 5, 33, 1, 37 | syl13anc 1373 |
. . . . . . . . . 10
โข (๐ โ ((๐ + ((๐โ๐ด) โ ๐)) ยท ๐ด) = ((๐ ยท ๐ด)(+gโ๐บ)(((๐โ๐ด) โ ๐) ยท ๐ด))) |
39 | 34, 35, 36 | mulgnn0dir 18984 |
. . . . . . . . . . 11
โข ((๐บ โ Mnd โง (๐ โ โ0
โง ((๐โ๐ด) โ ๐) โ โ0 โง ๐ด โ ๐)) โ ((๐ + ((๐โ๐ด) โ ๐)) ยท ๐ด) = ((๐ ยท ๐ด)(+gโ๐บ)(((๐โ๐ด) โ ๐) ยท ๐ด))) |
40 | 29, 8, 33, 1, 39 | syl13anc 1373 |
. . . . . . . . . 10
โข (๐ โ ((๐ + ((๐โ๐ด) โ ๐)) ยท ๐ด) = ((๐ ยท ๐ด)(+gโ๐บ)(((๐โ๐ด) โ ๐) ยท ๐ด))) |
41 | 28, 38, 40 | 3eqtr4d 2783 |
. . . . . . . . 9
โข (๐ โ ((๐ + ((๐โ๐ด) โ ๐)) ยท ๐ด) = ((๐ + ((๐โ๐ด) โ ๐)) ยท ๐ด)) |
42 | 10, 4 | pncan3d 11574 |
. . . . . . . . . . 11
โข (๐ โ (๐ + ((๐โ๐ด) โ ๐)) = (๐โ๐ด)) |
43 | 42 | oveq1d 7424 |
. . . . . . . . . 10
โข (๐ โ ((๐ + ((๐โ๐ด) โ ๐)) ยท ๐ด) = ((๐โ๐ด) ยท ๐ด)) |
44 | | odcl.2 |
. . . . . . . . . . . 12
โข ๐ = (odโ๐บ) |
45 | | odid.4 |
. . . . . . . . . . . 12
โข 0 =
(0gโ๐บ) |
46 | 34, 44, 35, 45 | odid 19406 |
. . . . . . . . . . 11
โข (๐ด โ ๐ โ ((๐โ๐ด) ยท ๐ด) = 0 ) |
47 | 1, 46 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ((๐โ๐ด) ยท ๐ด) = 0 ) |
48 | 43, 47 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ ((๐ + ((๐โ๐ด) โ ๐)) ยท ๐ด) = 0 ) |
49 | 41, 48 | eqtrd 2773 |
. . . . . . . 8
โข (๐ โ ((๐ + ((๐โ๐ด) โ ๐)) ยท ๐ด) = 0 ) |
50 | 26, 49 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ (((๐โ๐ด) + (๐ โ ๐)) ยท ๐ด) = 0 ) |
51 | 34, 44, 35, 45 | odlem2 19407 |
. . . . . . 7
โข ((๐ด โ ๐ โง ((๐โ๐ด) + (๐ โ ๐)) โ โ โง (((๐โ๐ด) + (๐ โ ๐)) ยท ๐ด) = 0 ) โ (๐โ๐ด) โ (1...((๐โ๐ด) + (๐ โ ๐)))) |
52 | 1, 24, 50, 51 | syl3anc 1372 |
. . . . . 6
โข (๐ โ (๐โ๐ด) โ (1...((๐โ๐ด) + (๐ โ ๐)))) |
53 | | elfzle2 13505 |
. . . . . 6
โข ((๐โ๐ด) โ (1...((๐โ๐ด) + (๐ โ ๐))) โ (๐โ๐ด) โค ((๐โ๐ด) + (๐ โ ๐))) |
54 | 52, 53 | syl 17 |
. . . . 5
โข (๐ โ (๐โ๐ด) โค ((๐โ๐ด) + (๐ โ ๐))) |
55 | 13, 20 | zsubcld 12671 |
. . . . . . 7
โข (๐ โ (๐ โ ๐) โ โค) |
56 | 55 | zred 12666 |
. . . . . 6
โข (๐ โ (๐ โ ๐) โ โ) |
57 | 3, 56 | addge01d 11802 |
. . . . 5
โข (๐ โ (0 โค (๐ โ ๐) โ (๐โ๐ด) โค ((๐โ๐ด) + (๐ โ ๐)))) |
58 | 54, 57 | mpbird 257 |
. . . 4
โข (๐ โ 0 โค (๐ โ ๐)) |
59 | 6, 9 | subge0d 11804 |
. . . 4
โข (๐ โ (0 โค (๐ โ ๐) โ ๐ โค ๐)) |
60 | 58, 59 | mpbid 231 |
. . 3
โข (๐ โ ๐ โค ๐) |
61 | 6, 9 | letri3d 11356 |
. . . 4
โข (๐ โ (๐ = ๐ โ (๐ โค ๐ โง ๐ โค ๐))) |
62 | 61 | biimprd 247 |
. . 3
โข (๐ โ ((๐ โค ๐ โง ๐ โค ๐) โ ๐ = ๐)) |
63 | 60, 62 | mpan2d 693 |
. 2
โข (๐ โ (๐ โค ๐ โ ๐ = ๐)) |
64 | 63 | imp 408 |
1
โข ((๐ โง ๐ โค ๐) โ ๐ = ๐) |