Step | Hyp | Ref
| Expression |
1 | | nn0z 12532 |
. . . . . . 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 19337 |
. . . . . . 7
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ฆ โ โค) โ ((๐โ๐ด) โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) |
7 | 1, 6 | syl3an3 1166 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ฆ โ โ0) โ ((๐โ๐ด) โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) |
8 | 7 | 3expa 1119 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐) โง ๐ฆ โ โ0) โ ((๐โ๐ด) โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) |
9 | 8 | ralrimiva 3140 |
. . . 4
โข ((๐บ โ Grp โง ๐ด โ ๐) โ โ๐ฆ โ โ0 ((๐โ๐ด) โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) |
10 | | breq1 5112 |
. . . . . 6
โข (๐ = (๐โ๐ด) โ (๐ โฅ ๐ฆ โ (๐โ๐ด) โฅ ๐ฆ)) |
11 | 10 | bibi1d 344 |
. . . . 5
โข (๐ = (๐โ๐ด) โ ((๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ) โ ((๐โ๐ด) โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ))) |
12 | 11 | ralbidv 3171 |
. . . 4
โข (๐ = (๐โ๐ด) โ (โ๐ฆ โ โ0 (๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ) โ โ๐ฆ โ โ0
((๐โ๐ด) โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ))) |
13 | 9, 12 | syl5ibrcom 247 |
. . 3
โข ((๐บ โ Grp โง ๐ด โ ๐) โ (๐ = (๐โ๐ด) โ โ๐ฆ โ โ0 (๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ))) |
14 | 13 | 3adant3 1133 |
. 2
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โ (๐ = (๐โ๐ด) โ โ๐ฆ โ โ0 (๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ))) |
15 | | simpl3 1194 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ๐ โ
โ0) |
16 | | simpl2 1193 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ๐ด โ ๐) |
17 | 2, 3 | odcl 19326 |
. . . . 5
โข (๐ด โ ๐ โ (๐โ๐ด) โ
โ0) |
18 | 16, 17 | syl 17 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐โ๐ด) โ
โ0) |
19 | 2, 3, 4, 5 | odid 19328 |
. . . . . 6
โข (๐ด โ ๐ โ ((๐โ๐ด) ยท ๐ด) = 0 ) |
20 | 16, 19 | syl 17 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ((๐โ๐ด) ยท ๐ด) = 0 ) |
21 | 17 | 3ad2ant2 1135 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โ (๐โ๐ด) โ
โ0) |
22 | | breq2 5113 |
. . . . . . . 8
โข (๐ฆ = (๐โ๐ด) โ (๐ โฅ ๐ฆ โ ๐ โฅ (๐โ๐ด))) |
23 | | oveq1 7368 |
. . . . . . . . 9
โข (๐ฆ = (๐โ๐ด) โ (๐ฆ ยท ๐ด) = ((๐โ๐ด) ยท ๐ด)) |
24 | 23 | eqeq1d 2735 |
. . . . . . . 8
โข (๐ฆ = (๐โ๐ด) โ ((๐ฆ ยท ๐ด) = 0 โ ((๐โ๐ด) ยท ๐ด) = 0 )) |
25 | 22, 24 | bibi12d 346 |
. . . . . . 7
โข (๐ฆ = (๐โ๐ด) โ ((๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ) โ (๐ โฅ (๐โ๐ด) โ ((๐โ๐ด) ยท ๐ด) = 0 ))) |
26 | 25 | rspcva 3581 |
. . . . . 6
โข (((๐โ๐ด) โ โ0 โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐ โฅ (๐โ๐ด) โ ((๐โ๐ด) ยท ๐ด) = 0 )) |
27 | 21, 26 | sylan 581 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐ โฅ (๐โ๐ด) โ ((๐โ๐ด) ยท ๐ด) = 0 )) |
28 | 20, 27 | mpbird 257 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ๐ โฅ (๐โ๐ด)) |
29 | | nn0z 12532 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โค) |
30 | | iddvds 16160 |
. . . . . . 7
โข (๐ โ โค โ ๐ โฅ ๐) |
31 | 15, 29, 30 | 3syl 18 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ๐ โฅ ๐) |
32 | | breq2 5113 |
. . . . . . . . 9
โข (๐ฆ = ๐ โ (๐ โฅ ๐ฆ โ ๐ โฅ ๐)) |
33 | | oveq1 7368 |
. . . . . . . . . 10
โข (๐ฆ = ๐ โ (๐ฆ ยท ๐ด) = (๐ ยท ๐ด)) |
34 | 33 | eqeq1d 2735 |
. . . . . . . . 9
โข (๐ฆ = ๐ โ ((๐ฆ ยท ๐ด) = 0 โ (๐ ยท ๐ด) = 0 )) |
35 | 32, 34 | bibi12d 346 |
. . . . . . . 8
โข (๐ฆ = ๐ โ ((๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ) โ (๐ โฅ ๐ โ (๐ ยท ๐ด) = 0 ))) |
36 | 35 | rspcva 3581 |
. . . . . . 7
โข ((๐ โ โ0
โง โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐ โฅ ๐ โ (๐ ยท ๐ด) = 0 )) |
37 | 36 | 3ad2antl3 1188 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐ โฅ ๐ โ (๐ ยท ๐ด) = 0 )) |
38 | 31, 37 | mpbid 231 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐ ยท ๐ด) = 0 ) |
39 | 2, 3, 4, 5 | oddvds 19337 |
. . . . . . 7
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โค) โ ((๐โ๐ด) โฅ ๐ โ (๐ ยท ๐ด) = 0 )) |
40 | 29, 39 | syl3an3 1166 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โ ((๐โ๐ด) โฅ ๐ โ (๐ ยท ๐ด) = 0 )) |
41 | 40 | adantr 482 |
. . . . 5
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ((๐โ๐ด) โฅ ๐ โ (๐ ยท ๐ด) = 0 )) |
42 | 38, 41 | mpbird 257 |
. . . 4
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ (๐โ๐ด) โฅ ๐) |
43 | | dvdseq 16204 |
. . . 4
โข (((๐ โ โ0
โง (๐โ๐ด) โ โ0)
โง (๐ โฅ (๐โ๐ด) โง (๐โ๐ด) โฅ ๐)) โ ๐ = (๐โ๐ด)) |
44 | 15, 18, 28, 42, 43 | syl22anc 838 |
. . 3
โข (((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โง
โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 )) โ ๐ = (๐โ๐ด)) |
45 | 44 | ex 414 |
. 2
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โ
(โ๐ฆ โ
โ0 (๐
โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ) โ ๐ = (๐โ๐ด))) |
46 | 14, 45 | impbid 211 |
1
โข ((๐บ โ Grp โง ๐ด โ ๐ โง ๐ โ โ0) โ (๐ = (๐โ๐ด) โ โ๐ฆ โ โ0 (๐ โฅ ๐ฆ โ (๐ฆ ยท ๐ด) = 0 ))) |