Step | Hyp | Ref
| Expression |
1 | | nn0z 12582 |
. . . . . . 7
โข (๐ฆ โ โ0
โ ๐ฆ โ
โค) |
2 | | odcl.1 |
. . . . . . . 8
โข ๐ = (Baseโ๐บ) |
3 | | odcl.2 |
. . . . . . . 8
โข ๐ = (odโ๐บ) |
4 | | odid.3 |
. . . . . . . 8
โข ยท =
(.gโ๐บ) |
5 | | odid.4 |
. . . . . . . 8
โข 0 =
(0gโ๐บ) |
6 | 2, 3, 4, 5 | oddvds 19414 |
. . . . . . 7
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ฆ โ โค) โ ((๐โ๐ด) โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) |
7 | 1, 6 | syl3an3 1165 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ฆ โ โ0) โ ((๐โ๐ด) โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) |
8 | 7 | 3expa 1118 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ โ0) โ ((๐โ๐ด) โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) |
9 | 8 | ralrimiva 3146 |
. . . 4
โข ((๐บ โ Grp โง ๐ด โ ๐) โ โ๐ฆ โ โ0 ((๐โ๐ด) โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) |
10 | | breq1 5151 |
. . . . . 6
โข (๐ = (๐โ๐ด) โ (๐ โฅ ๐ฆ โ (๐โ๐ด) โฅ ๐ฆ)) |
11 | 10 | bibi1d 343 |
. . . . 5
โข (๐ = (๐โ๐ด) โ ((๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ) โ ((๐โ๐ด) โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ))) |
12 | 11 | ralbidv 3177 |
. . . 4
โข (๐ = (๐โ๐ด) โ (โ๐ฆ โ โ0 (๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ) โ โ๐ฆ โ โ0
((๐โ๐ด) โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ))) |
13 | 9, 12 | syl5ibrcom 246 |
. . 3
โข ((๐บ โ Grp โง ๐ด โ ๐) โ (๐ = (๐โ๐ด) โ โ๐ฆ โ โ0 (๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ))) |
14 | 13 | 3adant3 1132 |
. 2
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โ (๐ = (๐โ๐ด) โ โ๐ฆ โ โ0 (๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ))) |
15 | | simpl3 1193 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ๐ โ
โ0) |
16 | | simpl2 1192 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ๐ด โ ๐) |
17 | 2, 3 | odcl 19403 |
. . . . 5
โข (๐ด โ ๐ โ (๐โ๐ด) โ
โ0) |
18 | 16, 17 | syl 17 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐โ๐ด) โ
โ0) |
19 | 2, 3, 4, 5 | odid 19405 |
. . . . . 6
โข (๐ด โ ๐ โ ((๐โ๐ด) ยท ๐ด) = 0 ) |
20 | 16, 19 | syl 17 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ((๐โ๐ด) ยท ๐ด) = 0 ) |
21 | 17 | 3ad2ant2 1134 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โ (๐โ๐ด) โ
โ0) |
22 | | breq2 5152 |
. . . . . . . 8
โข (๐ฆ = (๐โ๐ด) โ (๐ โฅ ๐ฆ โ ๐ โฅ (๐โ๐ด))) |
23 | | oveq1 7415 |
. . . . . . . . 9
โข (๐ฆ = (๐โ๐ด) โ (๐ฆ ยท ๐ด) = ((๐โ๐ด) ยท ๐ด)) |
24 | 23 | eqeq1d 2734 |
. . . . . . . 8
โข (๐ฆ = (๐โ๐ด) โ ((๐ฆ ยท ๐ด) = 0 โ ((๐โ๐ด) ยท ๐ด) = 0 )) |
25 | 22, 24 | bibi12d 345 |
. . . . . . 7
โข (๐ฆ = (๐โ๐ด) โ ((๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ) โ (๐ โฅ (๐โ๐ด) โ ((๐โ๐ด) ยท ๐ด) = 0 ))) |
26 | 25 | rspcva 3610 |
. . . . . 6
โข (((๐โ๐ด) โ โ0 โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐ โฅ (๐โ๐ด) โ ((๐โ๐ด) ยท ๐ด) = 0 )) |
27 | 21, 26 | sylan 580 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐ โฅ (๐โ๐ด) โ ((๐โ๐ด) ยท ๐ด) = 0 )) |
28 | 20, 27 | mpbird 256 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ๐ โฅ (๐โ๐ด)) |
29 | | nn0z 12582 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โค) |
30 | | iddvds 16212 |
. . . . . . 7
โข (๐ โ โค โ ๐ โฅ ๐) |
31 | 15, 29, 30 | 3syl 18 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ๐ โฅ ๐) |
32 | | breq2 5152 |
. . . . . . . . 9
โข (๐ฆ = ๐ โ (๐ โฅ ๐ฆ โ ๐ โฅ ๐)) |
33 | | oveq1 7415 |
. . . . . . . . . 10
โข (๐ฆ = ๐ โ (๐ฆ ยท ๐ด) = (๐ ยท ๐ด)) |
34 | 33 | eqeq1d 2734 |
. . . . . . . . 9
โข (๐ฆ = ๐ โ ((๐ฆ ยท ๐ด) = 0 โ (๐ ยท ๐ด) = 0 )) |
35 | 32, 34 | bibi12d 345 |
. . . . . . . 8
โข (๐ฆ = ๐ โ ((๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ) โ (๐ โฅ ๐ โ (๐ ยท ๐ด) = 0 ))) |
36 | 35 | rspcva 3610 |
. . . . . . 7
โข ((๐ โ โ0
โง โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐ โฅ ๐ โ (๐ ยท ๐ด) = 0 )) |
37 | 36 | 3ad2antl3 1187 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐ โฅ ๐ โ (๐ ยท ๐ด) = 0 )) |
38 | 31, 37 | mpbid 231 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐ ยท ๐ด) = 0 ) |
39 | 2, 3, 4, 5 | oddvds 19414 |
. . . . . . 7
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โ ((๐โ๐ด) โฅ ๐ โ (๐ ยท ๐ด) = 0 )) |
40 | 29, 39 | syl3an3 1165 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โ ((๐โ๐ด) โฅ ๐ โ (๐ ยท ๐ด) = 0 )) |
41 | 40 | adantr 481 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ((๐โ๐ด) โฅ ๐ โ (๐ ยท ๐ด) = 0 )) |
42 | 38, 41 | mpbird 256 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐โ๐ด) โฅ ๐) |
43 | | dvdseq 16256 |
. . . 4
โข (((๐ โ โ0
โง (๐โ๐ด) โ โ0)
โง (๐ โฅ (๐โ๐ด) โง (๐โ๐ด) โฅ ๐)) โ ๐ = (๐โ๐ด)) |
44 | 15, 18, 28, 42, 43 | syl22anc 837 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ๐ = (๐โ๐ด)) |
45 | 44 | ex 413 |
. 2
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โ
(โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ) โ ๐ = (๐โ๐ด))) |
46 | 14, 45 | impbid 211 |
1
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โ (๐ = (๐โ๐ด) โ โ๐ฆ โ โ0 (๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ))) |