Step |
Hyp |
Ref |
Expression |
1 |
|
recn |
โข ( ๐ด โ โ โ ๐ด โ โ ) |
2 |
|
it0e0 |
โข ( i ยท 0 ) = 0 |
3 |
2
|
oveq2i |
โข ( ๐ด + ( i ยท 0 ) ) = ( ๐ด + 0 ) |
4 |
|
addrid |
โข ( ๐ด โ โ โ ( ๐ด + 0 ) = ๐ด ) |
5 |
3 4
|
eqtrid |
โข ( ๐ด โ โ โ ( ๐ด + ( i ยท 0 ) ) = ๐ด ) |
6 |
1 5
|
syl |
โข ( ๐ด โ โ โ ( ๐ด + ( i ยท 0 ) ) = ๐ด ) |
7 |
6
|
fveq2d |
โข ( ๐ด โ โ โ ( โ โ ( ๐ด + ( i ยท 0 ) ) ) = ( โ โ ๐ด ) ) |
8 |
|
0re |
โข 0 โ โ |
9 |
|
crim |
โข ( ( ๐ด โ โ โง 0 โ โ ) โ ( โ โ ( ๐ด + ( i ยท 0 ) ) ) = 0 ) |
10 |
8 9
|
mpan2 |
โข ( ๐ด โ โ โ ( โ โ ( ๐ด + ( i ยท 0 ) ) ) = 0 ) |
11 |
7 10
|
eqtr3d |
โข ( ๐ด โ โ โ ( โ โ ๐ด ) = 0 ) |