Step | Hyp | Ref
| Expression |
1 | | ply1mulgsum.a |
. . . 4
โข ๐ด = (coe1โ๐พ) |
2 | | ply1mulgsum.b |
. . . 4
โข ๐ต = (Baseโ๐) |
3 | | ply1mulgsum.p |
. . . 4
โข ๐ = (Poly1โ๐
) |
4 | | eqid 2733 |
. . . 4
โข
(0gโ๐
) = (0gโ๐
) |
5 | 1, 2, 3, 4 | coe1ae0 21610 |
. . 3
โข (๐พ โ ๐ต โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐ดโ๐) = (0gโ๐
))) |
6 | 5 | 3ad2ant2 1135 |
. 2
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐ดโ๐) = (0gโ๐
))) |
7 | | ply1mulgsum.c |
. . . . 5
โข ๐ถ = (coe1โ๐ฟ) |
8 | 7, 2, 3, 4 | coe1ae0 21610 |
. . . 4
โข (๐ฟ โ ๐ต โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐ถโ๐) = (0gโ๐
))) |
9 | 8 | 3ad2ant3 1136 |
. . 3
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐ถโ๐) = (0gโ๐
))) |
10 | | nn0addcl 12456 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + ๐) โ
โ0) |
11 | 10 | adantr 482 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โ (๐ + ๐) โ
โ0) |
12 | 11 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง (โ๐ โ โ0 (๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง โ๐ โ โ0 (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)))) โ (๐ + ๐) โ
โ0) |
13 | | breq1 5112 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ + ๐) โ (๐ < ๐ โ (๐ + ๐) < ๐)) |
14 | 13 | imbi1d 342 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ + ๐) โ ((๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))) โ ((๐ + ๐) < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))))) |
15 | 14 | ralbidv 3171 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ + ๐) โ (โ๐ โ โ0 (๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))) โ โ๐ โ โ0 ((๐ + ๐) < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))))) |
16 | 15 | adantl 483 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ
โ0 โง ๐
โ โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง (โ๐ โ โ0 (๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง โ๐ โ โ0 (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)))) โง ๐ = (๐ + ๐)) โ (โ๐ โ โ0 (๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))) โ โ๐ โ โ0 ((๐ + ๐) < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))))) |
17 | | r19.26 3111 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ โ
โ0 ((๐
< ๐ โ (๐ถโ๐) = (0gโ๐
)) โง (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
))) โ (โ๐ โ โ0 (๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง โ๐ โ โ0 (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)))) |
18 | | nn0cn 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (๐ โ โ0
โ ๐ โ
โ) |
19 | 18 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โ) |
20 | | nn0cn 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (๐ โ โ0
โ ๐ โ
โ) |
21 | 20 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โ) |
22 | 19, 21 | addcomd 11365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + ๐) = (๐ + ๐)) |
23 | 22 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โ โ0
โง ๐ โ
โ0 โง ๐
โ โ0) โ (๐ + ๐) = (๐ + ๐)) |
24 | 23 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โ โ0
โง ๐ โ
โ0 โง ๐
โ โ0) โ ((๐ + ๐) < ๐ โ (๐ + ๐) < ๐)) |
25 | | nn0sumltlt 46516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โ โ0
โง ๐ โ
โ0 โง ๐
โ โ0) โ ((๐ + ๐) < ๐ โ ๐ < ๐)) |
26 | 24, 25 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โ โ0
โง ๐ โ
โ0 โง ๐
โ โ0) โ ((๐ + ๐) < ๐ โ ๐ < ๐)) |
27 | 26 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ โ โ0 โ ((๐ + ๐) < ๐ โ ๐ < ๐))) |
28 | 27 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ โ โ0 โ ((๐ + ๐) < ๐ โ ๐ < ๐))) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โ (๐ โ โ0 โ ((๐ + ๐) < ๐ โ ๐ < ๐))) |
30 | 29 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โ ((๐ + ๐) < ๐ โ ๐ < ๐)) |
31 | 30 | imim1d 82 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โ ((๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โ ((๐ + ๐) < ๐ โ (๐ถโ๐) = (0gโ๐
)))) |
32 | 31 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โ ((๐ + ๐) < ๐ โ ((๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โ (๐ถโ๐) = (0gโ๐
)))) |
33 | 32 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ โ
โ0 โง ๐
โ โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (๐ + ๐) < ๐) โ ((๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โ (๐ถโ๐) = (0gโ๐
))) |
34 | | nn0sumltlt 46516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ โ0
โง ๐ โ
โ0 โง ๐
โ โ0) โ ((๐ + ๐) < ๐ โ ๐ < ๐)) |
35 | 34 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ โ โ0 โ ((๐ + ๐) < ๐ โ ๐ < ๐))) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โ (๐ โ โ0 โ ((๐ + ๐) < ๐ โ ๐ < ๐))) |
37 | 36 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โ ((๐ + ๐) < ๐ โ ๐ < ๐)) |
38 | 37 | imim1d 82 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โ ((๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)) โ ((๐ + ๐) < ๐ โ (๐ดโ๐) = (0gโ๐
)))) |
39 | 38 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โ ((๐ + ๐) < ๐ โ ((๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)) โ (๐ดโ๐) = (0gโ๐
)))) |
40 | 39 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ โ
โ0 โง ๐
โ โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (๐ + ๐) < ๐) โ ((๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)) โ (๐ดโ๐) = (0gโ๐
))) |
41 | 33, 40 | anim12d 610 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ โ
โ0 โง ๐
โ โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (๐ + ๐) < ๐) โ (((๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
))) โ ((๐ถโ๐) = (0gโ๐
) โง (๐ดโ๐) = (0gโ๐
)))) |
42 | 41 | imp 408 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((๐ โ
โ0 โง ๐
โ โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (๐ + ๐) < ๐) โง ((๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)))) โ ((๐ถโ๐) = (0gโ๐
) โง (๐ดโ๐) = (0gโ๐
))) |
43 | 42 | ancomd 463 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((๐ โ
โ0 โง ๐
โ โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (๐ + ๐) < ๐) โง ((๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)))) โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))) |
44 | 43 | exp31 421 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โ ((๐ + ๐) < ๐ โ (((๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
))) โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))))) |
45 | 44 | com23 86 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โ (((๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
))) โ ((๐ + ๐) < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))))) |
46 | 45 | ralimdva 3161 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โ (โ๐ โ โ0 ((๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
))) โ โ๐ โ โ0 ((๐ + ๐) < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))))) |
47 | 17, 46 | biimtrrid 242 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โ ((โ๐ โ โ0 (๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง โ๐ โ โ0 (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
))) โ โ๐ โ โ0 ((๐ + ๐) < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))))) |
48 | 47 | imp 408 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง (โ๐ โ โ0 (๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง โ๐ โ โ0 (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)))) โ โ๐ โ โ0 ((๐ + ๐) < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
)))) |
49 | 12, 16, 48 | rspcedvd 3585 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ0
โง ๐ โ
โ0) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง (โ๐ โ โ0 (๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง โ๐ โ โ0 (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)))) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
)))) |
50 | 49 | exp31 421 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ ((โ๐ โ โ0 (๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง โ๐ โ โ0 (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
))) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
)))))) |
51 | 50 | com23 86 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((โ๐ โ โ0 (๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โง โ๐ โ โ0 (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
))) โ ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
)))))) |
52 | 51 | expd 417 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โ๐ โ โ0 (๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โ (โ๐ โ โ0 (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)) โ ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))))))) |
53 | 52 | com34 91 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โ๐ โ โ0 (๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โ ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ (โ๐ โ โ0 (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))))))) |
54 | 53 | impancom 453 |
. . . . . . . 8
โข ((๐ โ โ0
โง โ๐ โ
โ0 (๐ <
๐ โ (๐ถโ๐) = (0gโ๐
))) โ (๐ โ โ0 โ ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ (โ๐ โ โ0 (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))))))) |
55 | 54 | com14 96 |
. . . . . . 7
โข
(โ๐ โ
โ0 (๐ <
๐ โ (๐ดโ๐) = (0gโ๐
)) โ (๐ โ โ0 โ ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ ((๐ โ โ0 โง
โ๐ โ
โ0 (๐ <
๐ โ (๐ถโ๐) = (0gโ๐
))) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))))))) |
56 | 55 | impcom 409 |
. . . . . 6
โข ((๐ โ โ0
โง โ๐ โ
โ0 (๐ <
๐ โ (๐ดโ๐) = (0gโ๐
))) โ ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ ((๐ โ โ0 โง
โ๐ โ
โ0 (๐ <
๐ โ (๐ถโ๐) = (0gโ๐
))) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
)))))) |
57 | 56 | rexlimiva 3141 |
. . . . 5
โข
(โ๐ โ
โ0 โ๐ โ โ0 (๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)) โ ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ ((๐ โ โ0 โง
โ๐ โ
โ0 (๐ <
๐ โ (๐ถโ๐) = (0gโ๐
))) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
)))))) |
58 | 57 | com13 88 |
. . . 4
โข ((๐ โ โ0
โง โ๐ โ
โ0 (๐ <
๐ โ (๐ถโ๐) = (0gโ๐
))) โ ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ (โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
)))))) |
59 | 58 | rexlimiva 3141 |
. . 3
โข
(โ๐ โ
โ0 โ๐ โ โ0 (๐ < ๐ โ (๐ถโ๐) = (0gโ๐
)) โ ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ (โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
)))))) |
60 | 9, 59 | mpcom 38 |
. 2
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ (โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐ดโ๐) = (0gโ๐
)) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))))) |
61 | 6, 60 | mpd 15 |
1
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
)))) |