Step | Hyp | Ref
| Expression |
1 | | cnre 11159 |
. 2
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ โ
๐ด = (๐ฅ + (i ยท ๐ฆ))) |
2 | | 0cn 11154 |
. . . . . . 7
โข 0 โ
โ |
3 | | recn 11148 |
. . . . . . 7
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
4 | | ax-icn 11117 |
. . . . . . . 8
โข i โ
โ |
5 | | recn 11148 |
. . . . . . . 8
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
6 | | mulcl 11142 |
. . . . . . . 8
โข ((i
โ โ โง ๐ฆ
โ โ) โ (i ยท ๐ฆ) โ โ) |
7 | 4, 5, 6 | sylancr 588 |
. . . . . . 7
โข (๐ฆ โ โ โ (i
ยท ๐ฆ) โ
โ) |
8 | | adddi 11147 |
. . . . . . 7
โข ((0
โ โ โง ๐ฅ
โ โ โง (i ยท ๐ฆ) โ โ) โ (0 ยท (๐ฅ + (i ยท ๐ฆ))) = ((0 ยท ๐ฅ) + (0 ยท (i ยท
๐ฆ)))) |
9 | 2, 3, 7, 8 | mp3an3an 1468 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (0
ยท (๐ฅ + (i ยท
๐ฆ))) = ((0 ยท ๐ฅ) + (0 ยท (i ยท
๐ฆ)))) |
10 | | mul02lem2 11339 |
. . . . . . 7
โข (๐ฅ โ โ โ (0
ยท ๐ฅ) =
0) |
11 | | mul12 11327 |
. . . . . . . . 9
โข ((0
โ โ โง i โ โ โง ๐ฆ โ โ) โ (0 ยท (i
ยท ๐ฆ)) = (i ยท
(0 ยท ๐ฆ))) |
12 | 2, 4, 5, 11 | mp3an12i 1466 |
. . . . . . . 8
โข (๐ฆ โ โ โ (0
ยท (i ยท ๐ฆ)) =
(i ยท (0 ยท ๐ฆ))) |
13 | | mul02lem2 11339 |
. . . . . . . . 9
โข (๐ฆ โ โ โ (0
ยท ๐ฆ) =
0) |
14 | 13 | oveq2d 7378 |
. . . . . . . 8
โข (๐ฆ โ โ โ (i
ยท (0 ยท ๐ฆ)) =
(i ยท 0)) |
15 | 12, 14 | eqtrd 2777 |
. . . . . . 7
โข (๐ฆ โ โ โ (0
ยท (i ยท ๐ฆ)) =
(i ยท 0)) |
16 | 10, 15 | oveqan12d 7381 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((0
ยท ๐ฅ) + (0 ยท
(i ยท ๐ฆ))) = (0 + (i
ยท 0))) |
17 | 9, 16 | eqtrd 2777 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (0
ยท (๐ฅ + (i ยท
๐ฆ))) = (0 + (i ยท
0))) |
18 | | cnre 11159 |
. . . . . . . 8
โข (0 โ
โ โ โ๐ฅ
โ โ โ๐ฆ
โ โ 0 = (๐ฅ + (i
ยท ๐ฆ))) |
19 | 2, 18 | ax-mp 5 |
. . . . . . 7
โข
โ๐ฅ โ
โ โ๐ฆ โ
โ 0 = (๐ฅ + (i
ยท ๐ฆ)) |
20 | | oveq2 7370 |
. . . . . . . . . 10
โข (0 =
(๐ฅ + (i ยท ๐ฆ)) โ (0 ยท 0) = (0
ยท (๐ฅ + (i ยท
๐ฆ)))) |
21 | 20 | eqeq1d 2739 |
. . . . . . . . 9
โข (0 =
(๐ฅ + (i ยท ๐ฆ)) โ ((0 ยท 0) = (0 +
(i ยท 0)) โ (0 ยท (๐ฅ + (i ยท ๐ฆ))) = (0 + (i ยท 0)))) |
22 | 17, 21 | syl5ibrcom 247 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (0 =
(๐ฅ + (i ยท ๐ฆ)) โ (0 ยท 0) = (0 +
(i ยท 0)))) |
23 | 22 | rexlimivv 3197 |
. . . . . . 7
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ 0 = (๐ฅ + (i
ยท ๐ฆ)) โ (0
ยท 0) = (0 + (i ยท 0))) |
24 | 19, 23 | ax-mp 5 |
. . . . . 6
โข (0
ยท 0) = (0 + (i ยท 0)) |
25 | | 0re 11164 |
. . . . . . 7
โข 0 โ
โ |
26 | | mul02lem2 11339 |
. . . . . . 7
โข (0 โ
โ โ (0 ยท 0) = 0) |
27 | 25, 26 | ax-mp 5 |
. . . . . 6
โข (0
ยท 0) = 0 |
28 | 24, 27 | eqtr3i 2767 |
. . . . 5
โข (0 + (i
ยท 0)) = 0 |
29 | 17, 28 | eqtrdi 2793 |
. . . 4
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (0
ยท (๐ฅ + (i ยท
๐ฆ))) = 0) |
30 | | oveq2 7370 |
. . . . 5
โข (๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (0 ยท ๐ด) = (0 ยท (๐ฅ + (i ยท ๐ฆ)))) |
31 | 30 | eqeq1d 2739 |
. . . 4
โข (๐ด = (๐ฅ + (i ยท ๐ฆ)) โ ((0 ยท ๐ด) = 0 โ (0 ยท (๐ฅ + (i ยท ๐ฆ))) = 0)) |
32 | 29, 31 | syl5ibrcom 247 |
. . 3
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (0 ยท ๐ด) = 0)) |
33 | 32 | rexlimivv 3197 |
. 2
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ ๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (0 ยท ๐ด) = 0) |
34 | 1, 33 | syl 17 |
1
โข (๐ด โ โ โ (0
ยท ๐ด) =
0) |