Step | Hyp | Ref
| Expression |
1 | | 0cn 11155 |
. 2
โข 0 โ
โ |
2 | | cnre 11160 |
. 2
โข (0 โ
โ โ โ๐
โ โ โ๐
โ โ 0 = (๐ + (i
ยท ๐))) |
3 | | oveq2 7369 |
. . . 4
โข (0 =
(๐ + (i ยท ๐)) โ ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) |
4 | | ax-icn 11118 |
. . . . . . . . . 10
โข i โ
โ |
5 | 4 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ โ i โ
โ) |
6 | | recn 11149 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
7 | | 0cnd 11156 |
. . . . . . . . 9
โข (๐ โ โ โ 0 โ
โ) |
8 | 5, 6, 7 | mulassd 11186 |
. . . . . . . 8
โข (๐ โ โ โ ((i
ยท ๐) ยท 0) =
(i ยท (๐ ยท
0))) |
9 | | remul01 40923 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ ยท 0) =
0) |
10 | 9 | oveq2d 7377 |
. . . . . . . 8
โข (๐ โ โ โ (i
ยท (๐ ยท 0)) =
(i ยท 0)) |
11 | 8, 10 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ โ โ ((i
ยท ๐) ยท 0) =
(i ยท 0)) |
12 | 11 | ad2antlr 726 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) โ ((i ยท ๐) ยท 0) = (i ยท
0)) |
13 | | rernegcl 40887 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (0
โโ ๐) โ โ) |
14 | 13 | recnd 11191 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (0
โโ ๐) โ โ) |
15 | 14 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (0
โโ ๐) โ โ) |
16 | | recn 11149 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
17 | 16 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
18 | 5, 6 | mulcld 11183 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (i
ยท ๐) โ
โ) |
19 | 18 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (i
ยท ๐) โ
โ) |
20 | 15, 17, 19 | addassd 11185 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (((0
โโ ๐) + ๐) + (i ยท ๐)) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) |
21 | | renegid2 40929 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((0
โโ ๐) + ๐) = 0) |
22 | 21 | oveq1d 7376 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (((0
โโ ๐) + ๐) + (i ยท ๐)) = (0 + (i ยท ๐))) |
23 | | sn-addid2 40920 |
. . . . . . . . . . . . 13
โข ((i
ยท ๐) โ โ
โ (0 + (i ยท ๐))
= (i ยท ๐)) |
24 | 18, 23 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (0 + (i
ยท ๐)) = (i ยท
๐)) |
25 | 22, 24 | sylan9eq 2793 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (((0
โโ ๐) + ๐) + (i ยท ๐)) = (i ยท ๐)) |
26 | 20, 25 | eqtr3d 2775 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ((0
โโ ๐) + (๐ + (i ยท ๐))) = (i ยท ๐)) |
27 | 26 | eqeq2d 2744 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐))) โ ((0 โโ
๐) + 0) = (i ยท ๐))) |
28 | 27 | biimpa 478 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) โ ((0 โโ
๐) + 0) = (i ยท ๐)) |
29 | 28 | oveq1d 7376 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) โ (((0 โโ
๐) + 0) ยท 0) = ((i
ยท ๐) ยท
0)) |
30 | | elre0re 40824 |
. . . . . . . . . 10
โข (๐ โ โ โ 0 โ
โ) |
31 | 13, 30 | readdcld 11192 |
. . . . . . . . 9
โข (๐ โ โ โ ((0
โโ ๐) + 0) โ โ) |
32 | 31 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) โ ((0 โโ
๐) + 0) โ
โ) |
33 | | remul01 40923 |
. . . . . . . 8
โข (((0
โโ ๐) + 0) โ โ โ (((0
โโ ๐) + 0) ยท 0) = 0) |
34 | 32, 33 | syl 17 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) โ (((0 โโ
๐) + 0) ยท 0) =
0) |
35 | 29, 34 | eqtr3d 2775 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) โ ((i ยท ๐) ยท 0) = 0) |
36 | 12, 35 | eqtr3d 2775 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) โ (i ยท 0) =
0) |
37 | 36 | ex 414 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐))) โ (i ยท 0) =
0)) |
38 | 3, 37 | syl5 34 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (0 =
(๐ + (i ยท ๐)) โ (i ยท 0) =
0)) |
39 | 38 | rexlimivv 3193 |
. 2
โข
(โ๐ โ
โ โ๐ โ
โ 0 = (๐ + (i
ยท ๐)) โ (i
ยท 0) = 0) |
40 | 1, 2, 39 | mp2b 10 |
1
โข (i
ยท 0) = 0 |