Step |
Hyp |
Ref |
Expression |
1 |
|
odmulgid.1 |
โข ๐ = ( Base โ ๐บ ) |
2 |
|
odmulgid.2 |
โข ๐ = ( od โ ๐บ ) |
3 |
|
odmulgid.3 |
โข ยท = ( .g โ ๐บ ) |
4 |
1 2
|
odcl |
โข ( ๐ด โ ๐ โ ( ๐ โ ๐ด ) โ โ0 ) |
5 |
4
|
nn0zd |
โข ( ๐ด โ ๐ โ ( ๐ โ ๐ด ) โ โค ) |
6 |
5
|
3ad2ant2 |
โข ( ( ๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค ) โ ( ๐ โ ๐ด ) โ โค ) |
7 |
|
simp3 |
โข ( ( ๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค ) โ ๐ โ โค ) |
8 |
|
dvdsmul1 |
โข ( ( ( ๐ โ ๐ด ) โ โค โง ๐ โ โค ) โ ( ๐ โ ๐ด ) โฅ ( ( ๐ โ ๐ด ) ยท ๐ ) ) |
9 |
6 7 8
|
syl2anc |
โข ( ( ๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค ) โ ( ๐ โ ๐ด ) โฅ ( ( ๐ โ ๐ด ) ยท ๐ ) ) |
10 |
1 2 3
|
odmulgid |
โข ( ( ( ๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค ) โง ( ๐ โ ๐ด ) โ โค ) โ ( ( ๐ โ ( ๐ ยท ๐ด ) ) โฅ ( ๐ โ ๐ด ) โ ( ๐ โ ๐ด ) โฅ ( ( ๐ โ ๐ด ) ยท ๐ ) ) ) |
11 |
6 10
|
mpdan |
โข ( ( ๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค ) โ ( ( ๐ โ ( ๐ ยท ๐ด ) ) โฅ ( ๐ โ ๐ด ) โ ( ๐ โ ๐ด ) โฅ ( ( ๐ โ ๐ด ) ยท ๐ ) ) ) |
12 |
9 11
|
mpbird |
โข ( ( ๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค ) โ ( ๐ โ ( ๐ ยท ๐ด ) ) โฅ ( ๐ โ ๐ด ) ) |