Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ (๐โ๐ด) โ โ) |
2 | | simpl3 1193 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ ๐ โ โค) |
3 | | dvdsval3 16197 |
. . . 4
โข (((๐โ๐ด) โ โ โง ๐ โ โค) โ ((๐โ๐ด) โฅ ๐ โ (๐ mod (๐โ๐ด)) = 0)) |
4 | 1, 2, 3 | syl2anc 584 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ ((๐โ๐ด) โฅ ๐ โ (๐ mod (๐โ๐ด)) = 0)) |
5 | | simpl2 1192 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ ๐ด โ ๐) |
6 | | odcl.1 |
. . . . . . 7
โข ๐ = (Baseโ๐บ) |
7 | | odid.4 |
. . . . . . 7
โข 0 =
(0gโ๐บ) |
8 | | odid.3 |
. . . . . . 7
โข ยท =
(.gโ๐บ) |
9 | 6, 7, 8 | mulg0 18951 |
. . . . . 6
โข (๐ด โ ๐ โ (0 ยท ๐ด) = 0 ) |
10 | 5, 9 | syl 17 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ (0 ยท ๐ด) = 0 ) |
11 | | oveq1 7412 |
. . . . . 6
โข ((๐ mod (๐โ๐ด)) = 0 โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = (0 ยท ๐ด)) |
12 | 11 | eqeq1d 2734 |
. . . . 5
โข ((๐ mod (๐โ๐ด)) = 0 โ (((๐ mod (๐โ๐ด)) ยท ๐ด) = 0 โ (0 ยท ๐ด) = 0 )) |
13 | 10, 12 | syl5ibrcom 246 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) = 0 โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = 0 )) |
14 | 2 | zred 12662 |
. . . . . . . 8
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ ๐ โ โ) |
15 | 1 | nnrpd 13010 |
. . . . . . . 8
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ (๐โ๐ด) โ
โ+) |
16 | | modlt 13841 |
. . . . . . . 8
โข ((๐ โ โ โง (๐โ๐ด) โ โ+) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
17 | 14, 15, 16 | syl2anc 584 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) < (๐โ๐ด)) |
18 | 2, 1 | zmodcld 13853 |
. . . . . . . . 9
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) โ
โ0) |
19 | 18 | nn0red 12529 |
. . . . . . . 8
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ (๐ mod (๐โ๐ด)) โ โ) |
20 | 1 | nnred 12223 |
. . . . . . . 8
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ (๐โ๐ด) โ โ) |
21 | 19, 20 | ltnled 11357 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) < (๐โ๐ด) โ ยฌ (๐โ๐ด) โค (๐ mod (๐โ๐ด)))) |
22 | 17, 21 | mpbid 231 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ ยฌ (๐โ๐ด) โค (๐ mod (๐โ๐ด))) |
23 | | odcl.2 |
. . . . . . . . . . . 12
โข ๐ = (odโ๐บ) |
24 | 6, 23, 8, 7 | odlem2 19401 |
. . . . . . . . . . 11
โข ((๐ด โ ๐ โง (๐ mod (๐โ๐ด)) โ โ โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = 0 ) โ (๐โ๐ด) โ (1...(๐ mod (๐โ๐ด)))) |
25 | | elfzle2 13501 |
. . . . . . . . . . 11
โข ((๐โ๐ด) โ (1...(๐ mod (๐โ๐ด))) โ (๐โ๐ด) โค (๐ mod (๐โ๐ด))) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
โข ((๐ด โ ๐ โง (๐ mod (๐โ๐ด)) โ โ โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = 0 ) โ (๐โ๐ด) โค (๐ mod (๐โ๐ด))) |
27 | 26 | 3com23 1126 |
. . . . . . . . 9
โข ((๐ด โ ๐ โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = 0 โง (๐ mod (๐โ๐ด)) โ โ) โ (๐โ๐ด) โค (๐ mod (๐โ๐ด))) |
28 | 27 | 3expia 1121 |
. . . . . . . 8
โข ((๐ด โ ๐ โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = 0 ) โ ((๐ mod (๐โ๐ด)) โ โ โ (๐โ๐ด) โค (๐ mod (๐โ๐ด)))) |
29 | 28 | con3d 152 |
. . . . . . 7
โข ((๐ด โ ๐ โง ((๐ mod (๐โ๐ด)) ยท ๐ด) = 0 ) โ (ยฌ (๐โ๐ด) โค (๐ mod (๐โ๐ด)) โ ยฌ (๐ mod (๐โ๐ด)) โ โ)) |
30 | 29 | impancom 452 |
. . . . . 6
โข ((๐ด โ ๐ โง ยฌ (๐โ๐ด) โค (๐ mod (๐โ๐ด))) โ (((๐ mod (๐โ๐ด)) ยท ๐ด) = 0 โ ยฌ (๐ mod (๐โ๐ด)) โ โ)) |
31 | 5, 22, 30 | syl2anc 584 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ (((๐ mod (๐โ๐ด)) ยท ๐ด) = 0 โ ยฌ (๐ mod (๐โ๐ด)) โ โ)) |
32 | | elnn0 12470 |
. . . . . . 7
โข ((๐ mod (๐โ๐ด)) โ โ0 โ ((๐ mod (๐โ๐ด)) โ โ โจ (๐ mod (๐โ๐ด)) = 0)) |
33 | 18, 32 | sylib 217 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) โ โ โจ (๐ mod (๐โ๐ด)) = 0)) |
34 | 33 | ord 862 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ (ยฌ (๐ mod (๐โ๐ด)) โ โ โ (๐ mod (๐โ๐ด)) = 0)) |
35 | 31, 34 | syld 47 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ (((๐ mod (๐โ๐ด)) ยท ๐ด) = 0 โ (๐ mod (๐โ๐ด)) = 0)) |
36 | 13, 35 | impbid 211 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) = 0 โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = 0 )) |
37 | 6, 23, 8, 7 | odmod 19408 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ ((๐ mod (๐โ๐ด)) ยท ๐ด) = (๐ ยท ๐ด)) |
38 | 37 | eqeq1d 2734 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ (((๐ mod (๐โ๐ด)) ยท ๐ด) = 0 โ (๐ ยท ๐ด) = 0 )) |
39 | 4, 36, 38 | 3bitrd 304 |
. 2
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) โ โ) โ ((๐โ๐ด) โฅ ๐ โ (๐ ยท ๐ด) = 0 )) |
40 | | simpr 485 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) = 0) โ (๐โ๐ด) = 0) |
41 | 40 | breq1d 5157 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) = 0) โ ((๐โ๐ด) โฅ ๐ โ 0 โฅ ๐)) |
42 | | simpl3 1193 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) = 0) โ ๐ โ โค) |
43 | | 0dvds 16216 |
. . . 4
โข (๐ โ โค โ (0
โฅ ๐ โ ๐ = 0)) |
44 | 42, 43 | syl 17 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) = 0) โ (0 โฅ ๐ โ ๐ = 0)) |
45 | | simpl2 1192 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) = 0) โ ๐ด โ ๐) |
46 | 45, 9 | syl 17 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) = 0) โ (0 ยท ๐ด) = 0 ) |
47 | | oveq1 7412 |
. . . . . 6
โข (๐ = 0 โ (๐ ยท ๐ด) = (0 ยท ๐ด)) |
48 | 47 | eqeq1d 2734 |
. . . . 5
โข (๐ = 0 โ ((๐ ยท ๐ด) = 0 โ (0 ยท ๐ด) = 0 )) |
49 | 46, 48 | syl5ibrcom 246 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) = 0) โ (๐ = 0 โ (๐ ยท ๐ด) = 0 )) |
50 | 6, 23, 8, 7 | odnncl 19407 |
. . . . . . . . 9
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ (๐โ๐ด) โ โ) |
51 | 50 | nnne0d 12258 |
. . . . . . . 8
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ โ 0 โง (๐ ยท ๐ด) = 0 )) โ (๐โ๐ด) โ 0) |
52 | 51 | expr 457 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง ๐ โ 0) โ ((๐ ยท ๐ด) = 0 โ (๐โ๐ด) โ 0)) |
53 | 52 | impancom 452 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = 0 ) โ (๐ โ 0 โ (๐โ๐ด) โ 0)) |
54 | 53 | necon4d 2964 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = 0 ) โ ((๐โ๐ด) = 0 โ ๐ = 0)) |
55 | 54 | impancom 452 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) = 0) โ ((๐ ยท ๐ด) = 0 โ ๐ = 0)) |
56 | 49, 55 | impbid 211 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) = 0) โ (๐ = 0 โ (๐ ยท ๐ด) = 0 )) |
57 | 41, 44, 56 | 3bitrd 304 |
. 2
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โง (๐โ๐ด) = 0) โ ((๐โ๐ด) โฅ ๐ โ (๐ ยท ๐ด) = 0 )) |
58 | 6, 23 | odcl 19398 |
. . . 4
โข (๐ด โ ๐ โ (๐โ๐ด) โ
โ0) |
59 | 58 | 3ad2ant2 1134 |
. . 3
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โ (๐โ๐ด) โ
โ0) |
60 | | elnn0 12470 |
. . 3
โข ((๐โ๐ด) โ โ0 โ ((๐โ๐ด) โ โ โจ (๐โ๐ด) = 0)) |
61 | 59, 60 | sylib 217 |
. 2
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โ ((๐โ๐ด) โ โ โจ (๐โ๐ด) = 0)) |
62 | 39, 57, 61 | mpjaodan 957 |
1
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โ ((๐โ๐ด) โฅ ๐ โ (๐ ยท ๐ด) = 0 )) |