Step | Hyp | Ref
| Expression |
1 | | un0addcl.2 |
. . . . 5
โข ๐ = (๐ โช {0}) |
2 | 1 | eleq2i 2825 |
. . . 4
โข (๐ โ ๐ โ ๐ โ (๐ โช {0})) |
3 | | elun 4148 |
. . . 4
โข (๐ โ (๐ โช {0}) โ (๐ โ ๐ โจ ๐ โ {0})) |
4 | 2, 3 | bitri 274 |
. . 3
โข (๐ โ ๐ โ (๐ โ ๐ โจ ๐ โ {0})) |
5 | 1 | eleq2i 2825 |
. . . . . 6
โข (๐ โ ๐ โ ๐ โ (๐ โช {0})) |
6 | | elun 4148 |
. . . . . 6
โข (๐ โ (๐ โช {0}) โ (๐ โ ๐ โจ ๐ โ {0})) |
7 | 5, 6 | bitri 274 |
. . . . 5
โข (๐ โ ๐ โ (๐ โ ๐ โจ ๐ โ {0})) |
8 | | ssun1 4172 |
. . . . . . . . 9
โข ๐ โ (๐ โช {0}) |
9 | 8, 1 | sseqtrri 4019 |
. . . . . . . 8
โข ๐ โ ๐ |
10 | | un0mulcl.3 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ ยท ๐) โ ๐) |
11 | 9, 10 | sselid 3980 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ ยท ๐) โ ๐) |
12 | 11 | expr 457 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ (๐ โ ๐ โ (๐ ยท ๐) โ ๐)) |
13 | | un0addcl.1 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
14 | 13 | sselda 3982 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐) โ ๐ โ โ) |
15 | 14 | mul02d 11411 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ (0 ยท ๐) = 0) |
16 | | ssun2 4173 |
. . . . . . . . . . 11
โข {0}
โ (๐ โช
{0}) |
17 | 16, 1 | sseqtrri 4019 |
. . . . . . . . . 10
โข {0}
โ ๐ |
18 | | c0ex 11207 |
. . . . . . . . . . 11
โข 0 โ
V |
19 | 18 | snss 4789 |
. . . . . . . . . 10
โข (0 โ
๐ โ {0} โ ๐) |
20 | 17, 19 | mpbir 230 |
. . . . . . . . 9
โข 0 โ
๐ |
21 | 15, 20 | eqeltrdi 2841 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ (0 ยท ๐) โ ๐) |
22 | | elsni 4645 |
. . . . . . . . . 10
โข (๐ โ {0} โ ๐ = 0) |
23 | 22 | oveq1d 7423 |
. . . . . . . . 9
โข (๐ โ {0} โ (๐ ยท ๐) = (0 ยท ๐)) |
24 | 23 | eleq1d 2818 |
. . . . . . . 8
โข (๐ โ {0} โ ((๐ ยท ๐) โ ๐ โ (0 ยท ๐) โ ๐)) |
25 | 21, 24 | syl5ibrcom 246 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ (๐ โ {0} โ (๐ ยท ๐) โ ๐)) |
26 | 25 | impancom 452 |
. . . . . 6
โข ((๐ โง ๐ โ {0}) โ (๐ โ ๐ โ (๐ ยท ๐) โ ๐)) |
27 | 12, 26 | jaodan 956 |
. . . . 5
โข ((๐ โง (๐ โ ๐ โจ ๐ โ {0})) โ (๐ โ ๐ โ (๐ ยท ๐) โ ๐)) |
28 | 7, 27 | sylan2b 594 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (๐ โ ๐ โ (๐ ยท ๐) โ ๐)) |
29 | | 0cnd 11206 |
. . . . . . . . . . 11
โข (๐ โ 0 โ
โ) |
30 | 29 | snssd 4812 |
. . . . . . . . . 10
โข (๐ โ {0} โ
โ) |
31 | 13, 30 | unssd 4186 |
. . . . . . . . 9
โข (๐ โ (๐ โช {0}) โ
โ) |
32 | 1, 31 | eqsstrid 4030 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
33 | 32 | sselda 3982 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ ๐ โ โ) |
34 | 33 | mul01d 11412 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ (๐ ยท 0) = 0) |
35 | 34, 20 | eqeltrdi 2841 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ (๐ ยท 0) โ ๐) |
36 | | elsni 4645 |
. . . . . . 7
โข (๐ โ {0} โ ๐ = 0) |
37 | 36 | oveq2d 7424 |
. . . . . 6
โข (๐ โ {0} โ (๐ ยท ๐) = (๐ ยท 0)) |
38 | 37 | eleq1d 2818 |
. . . . 5
โข (๐ โ {0} โ ((๐ ยท ๐) โ ๐ โ (๐ ยท 0) โ ๐)) |
39 | 35, 38 | syl5ibrcom 246 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (๐ โ {0} โ (๐ ยท ๐) โ ๐)) |
40 | 28, 39 | jaod 857 |
. . 3
โข ((๐ โง ๐ โ ๐) โ ((๐ โ ๐ โจ ๐ โ {0}) โ (๐ ยท ๐) โ ๐)) |
41 | 4, 40 | biimtrid 241 |
. 2
โข ((๐ โง ๐ โ ๐) โ (๐ โ ๐ โ (๐ ยท ๐) โ ๐)) |
42 | 41 | impr 455 |
1
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ ยท ๐) โ ๐) |