Step | Hyp | Ref
| Expression |
1 | | 0cn 11205 |
. 2
โข 0 โ
โ |
2 | | cnre 11210 |
. 2
โข (0 โ
โ โ โ๐
โ โ โ๐
โ โ 0 = (๐ + (i
ยท ๐))) |
3 | | oveq2 7416 |
. . . 4
โข (0 =
(๐ + (i ยท ๐)) โ ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) |
4 | | ax-icn 11168 |
. . . . . . . . . 10
โข i โ
โ |
5 | 4 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ โ i โ
โ) |
6 | | recn 11199 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
7 | | 0cnd 11206 |
. . . . . . . . 9
โข (๐ โ โ โ 0 โ
โ) |
8 | 5, 6, 7 | mulassd 11236 |
. . . . . . . 8
โข (๐ โ โ โ ((i
ยท ๐) ยท 0) =
(i ยท (๐ ยท
0))) |
9 | | remul01 41281 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ ยท 0) =
0) |
10 | 9 | oveq2d 7424 |
. . . . . . . 8
โข (๐ โ โ โ (i
ยท (๐ ยท 0)) =
(i ยท 0)) |
11 | 8, 10 | eqtrd 2772 |
. . . . . . 7
โข (๐ โ โ โ ((i
ยท ๐) ยท 0) =
(i ยท 0)) |
12 | 11 | ad2antlr 725 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) โ ((i ยท ๐) ยท 0) = (i ยท
0)) |
13 | | rernegcl 41245 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (0
โโ ๐) โ โ) |
14 | 13 | recnd 11241 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (0
โโ ๐) โ โ) |
15 | 14 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (0
โโ ๐) โ โ) |
16 | | recn 11199 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
17 | 16 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
18 | 5, 6 | mulcld 11233 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (i
ยท ๐) โ
โ) |
19 | 18 | adantl 482 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (i
ยท ๐) โ
โ) |
20 | 15, 17, 19 | addassd 11235 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (((0
โโ ๐) + ๐) + (i ยท ๐)) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) |
21 | | renegid2 41287 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((0
โโ ๐) + ๐) = 0) |
22 | 21 | oveq1d 7423 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (((0
โโ ๐) + ๐) + (i ยท ๐)) = (0 + (i ยท ๐))) |
23 | | sn-addlid 41278 |
. . . . . . . . . . . . 13
โข ((i
ยท ๐) โ โ
โ (0 + (i ยท ๐))
= (i ยท ๐)) |
24 | 18, 23 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (0 + (i
ยท ๐)) = (i ยท
๐)) |
25 | 22, 24 | sylan9eq 2792 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (((0
โโ ๐) + ๐) + (i ยท ๐)) = (i ยท ๐)) |
26 | 20, 25 | eqtr3d 2774 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ((0
โโ ๐) + (๐ + (i ยท ๐))) = (i ยท ๐)) |
27 | 26 | eqeq2d 2743 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐))) โ ((0 โโ
๐) + 0) = (i ยท ๐))) |
28 | 27 | biimpa 477 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) โ ((0 โโ
๐) + 0) = (i ยท ๐)) |
29 | 28 | oveq1d 7423 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) โ (((0 โโ
๐) + 0) ยท 0) = ((i
ยท ๐) ยท
0)) |
30 | | elre0re 41177 |
. . . . . . . . . 10
โข (๐ โ โ โ 0 โ
โ) |
31 | 13, 30 | readdcld 11242 |
. . . . . . . . 9
โข (๐ โ โ โ ((0
โโ ๐) + 0) โ โ) |
32 | 31 | ad2antrr 724 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) โ ((0 โโ
๐) + 0) โ
โ) |
33 | | remul01 41281 |
. . . . . . . 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 2774 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) โ ((i ยท ๐) ยท 0) = 0) |
36 | 12, 35 | eqtr3d 2774 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐)))) โ (i ยท 0) =
0) |
37 | 36 | ex 413 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (((0
โโ ๐) + 0) = ((0 โโ ๐) + (๐ + (i ยท ๐))) โ (i ยท 0) =
0)) |
38 | 3, 37 | syl5 34 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (0 =
(๐ + (i ยท ๐)) โ (i ยท 0) =
0)) |
39 | 38 | rexlimivv 3199 |
. 2
โข
(โ๐ โ
โ โ๐ โ
โ 0 = (๐ + (i
ยท ๐)) โ (i
ยท 0) = 0) |
40 | 1, 2, 39 | mp2b 10 |
1
โข (i
ยท 0) = 0 |