Step | Hyp | Ref
| Expression |
1 | | un0addcl.2 |
. . . . 5
โข ๐ = (๐ โช {0}) |
2 | 1 | eleq2i 2830 |
. . . 4
โข (๐ โ ๐ โ ๐ โ (๐ โช {0})) |
3 | | elun 4109 |
. . . 4
โข (๐ โ (๐ โช {0}) โ (๐ โ ๐ โจ ๐ โ {0})) |
4 | 2, 3 | bitri 275 |
. . 3
โข (๐ โ ๐ โ (๐ โ ๐ โจ ๐ โ {0})) |
5 | 1 | eleq2i 2830 |
. . . . . 6
โข (๐ โ ๐ โ ๐ โ (๐ โช {0})) |
6 | | elun 4109 |
. . . . . 6
โข (๐ โ (๐ โช {0}) โ (๐ โ ๐ โจ ๐ โ {0})) |
7 | 5, 6 | bitri 275 |
. . . . 5
โข (๐ โ ๐ โ (๐ โ ๐ โจ ๐ โ {0})) |
8 | | ssun1 4133 |
. . . . . . . . 9
โข ๐ โ (๐ โช {0}) |
9 | 8, 1 | sseqtrri 3982 |
. . . . . . . 8
โข ๐ โ ๐ |
10 | | un0mulcl.3 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ ยท ๐) โ ๐) |
11 | 9, 10 | sselid 3943 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ ยท ๐) โ ๐) |
12 | 11 | expr 458 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ (๐ โ ๐ โ (๐ ยท ๐) โ ๐)) |
13 | | un0addcl.1 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
14 | 13 | sselda 3945 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐) โ ๐ โ โ) |
15 | 14 | mul02d 11354 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ (0 ยท ๐) = 0) |
16 | | ssun2 4134 |
. . . . . . . . . . 11
โข {0}
โ (๐ โช
{0}) |
17 | 16, 1 | sseqtrri 3982 |
. . . . . . . . . 10
โข {0}
โ ๐ |
18 | | c0ex 11150 |
. . . . . . . . . . 11
โข 0 โ
V |
19 | 18 | snss 4747 |
. . . . . . . . . 10
โข (0 โ
๐ โ {0} โ ๐) |
20 | 17, 19 | mpbir 230 |
. . . . . . . . 9
โข 0 โ
๐ |
21 | 15, 20 | eqeltrdi 2846 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ (0 ยท ๐) โ ๐) |
22 | | elsni 4604 |
. . . . . . . . . 10
โข (๐ โ {0} โ ๐ = 0) |
23 | 22 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ {0} โ (๐ ยท ๐) = (0 ยท ๐)) |
24 | 23 | eleq1d 2823 |
. . . . . . . 8
โข (๐ โ {0} โ ((๐ ยท ๐) โ ๐ โ (0 ยท ๐) โ ๐)) |
25 | 21, 24 | syl5ibrcom 247 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ (๐ โ {0} โ (๐ ยท ๐) โ ๐)) |
26 | 25 | impancom 453 |
. . . . . 6
โข ((๐ โง ๐ โ {0}) โ (๐ โ ๐ โ (๐ ยท ๐) โ ๐)) |
27 | 12, 26 | jaodan 957 |
. . . . 5
โข ((๐ โง (๐ โ ๐ โจ ๐ โ {0})) โ (๐ โ ๐ โ (๐ ยท ๐) โ ๐)) |
28 | 7, 27 | sylan2b 595 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (๐ โ ๐ โ (๐ ยท ๐) โ ๐)) |
29 | | 0cnd 11149 |
. . . . . . . . . . 11
โข (๐ โ 0 โ
โ) |
30 | 29 | snssd 4770 |
. . . . . . . . . 10
โข (๐ โ {0} โ
โ) |
31 | 13, 30 | unssd 4147 |
. . . . . . . . 9
โข (๐ โ (๐ โช {0}) โ
โ) |
32 | 1, 31 | eqsstrid 3993 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
33 | 32 | sselda 3945 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ ๐ โ โ) |
34 | 33 | mul01d 11355 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ (๐ ยท 0) = 0) |
35 | 34, 20 | eqeltrdi 2846 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ (๐ ยท 0) โ ๐) |
36 | | elsni 4604 |
. . . . . . 7
โข (๐ โ {0} โ ๐ = 0) |
37 | 36 | oveq2d 7374 |
. . . . . 6
โข (๐ โ {0} โ (๐ ยท ๐) = (๐ ยท 0)) |
38 | 37 | eleq1d 2823 |
. . . . 5
โข (๐ โ {0} โ ((๐ ยท ๐) โ ๐ โ (๐ ยท 0) โ ๐)) |
39 | 35, 38 | syl5ibrcom 247 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (๐ โ {0} โ (๐ ยท ๐) โ ๐)) |
40 | 28, 39 | jaod 858 |
. . 3
โข ((๐ โง ๐ โ ๐) โ ((๐ โ ๐ โจ ๐ โ {0}) โ (๐ ยท ๐) โ ๐)) |
41 | 4, 40 | biimtrid 241 |
. 2
โข ((๐ โง ๐ โ ๐) โ (๐ โ ๐ โ (๐ ยท ๐) โ ๐)) |
42 | 41 | impr 456 |
1
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ ยท ๐) โ ๐) |