Step | Hyp | Ref
| Expression |
1 | | 0cn 7949 |
. 2
โข 0 โ
โ |
2 | | cnre 7953 |
. 2
โข (0 โ
โ โ โ๐ฅ
โ โ โ๐ฆ
โ โ 0 = (๐ฅ + (i
ยท ๐ฆ))) |
3 | | ax-rnegex 7920 |
. . . . . 6
โข (๐ฅ โ โ โ
โ๐ง โ โ
(๐ฅ + ๐ง) = 0) |
4 | 3 | adantr 276 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
โ๐ง โ โ
(๐ฅ + ๐ง) = 0) |
5 | | recn 7944 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
6 | | ax-icn 7906 |
. . . . . . . . . . . 12
โข i โ
โ |
7 | | recn 7944 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
8 | | mulcl 7938 |
. . . . . . . . . . . 12
โข ((i
โ โ โง ๐ฆ
โ โ) โ (i ยท ๐ฆ) โ โ) |
9 | 6, 7, 8 | sylancr 414 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ (i
ยท ๐ฆ) โ
โ) |
10 | | recn 7944 |
. . . . . . . . . . 11
โข (๐ง โ โ โ ๐ง โ
โ) |
11 | | addlid 8096 |
. . . . . . . . . . . . . . 15
โข (๐ง โ โ โ (0 +
๐ง) = ๐ง) |
12 | 11 | 3ad2ant3 1020 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ
โง ๐ง โ โ)
โ (0 + ๐ง) = ๐ง) |
13 | 12 | adantr 276 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ
โง ๐ง โ โ)
โง ((๐ฅ + ๐ง) = 0 โง 0 = (๐ฅ + (i ยท ๐ฆ)))) โ (0 + ๐ง) = ๐ง) |
14 | | oveq1 5882 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ + ๐ง) = 0 โ ((๐ฅ + ๐ง) + (i ยท ๐ฆ)) = (0 + (i ยท ๐ฆ))) |
15 | 14 | ad2antrl 490 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ
โง ๐ง โ โ)
โง ((๐ฅ + ๐ง) = 0 โง 0 = (๐ฅ + (i ยท ๐ฆ)))) โ ((๐ฅ + ๐ง) + (i ยท ๐ฆ)) = (0 + (i ยท ๐ฆ))) |
16 | | add32 8116 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ โ โ โง ๐ง โ โ โง (i
ยท ๐ฆ) โ โ)
โ ((๐ฅ + ๐ง) + (i ยท ๐ฆ)) = ((๐ฅ + (i ยท ๐ฆ)) + ๐ง)) |
17 | 16 | 3com23 1209 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ
โง ๐ง โ โ)
โ ((๐ฅ + ๐ง) + (i ยท ๐ฆ)) = ((๐ฅ + (i ยท ๐ฆ)) + ๐ง)) |
18 | | oveq1 5882 |
. . . . . . . . . . . . . . . . 17
โข (0 =
(๐ฅ + (i ยท ๐ฆ)) โ (0 + ๐ง) = ((๐ฅ + (i ยท ๐ฆ)) + ๐ง)) |
19 | 18 | eqcomd 2183 |
. . . . . . . . . . . . . . . 16
โข (0 =
(๐ฅ + (i ยท ๐ฆ)) โ ((๐ฅ + (i ยท ๐ฆ)) + ๐ง) = (0 + ๐ง)) |
20 | 17, 19 | sylan9eq 2230 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ
โง ๐ง โ โ)
โง 0 = (๐ฅ + (i ยท
๐ฆ))) โ ((๐ฅ + ๐ง) + (i ยท ๐ฆ)) = (0 + ๐ง)) |
21 | 20 | adantrl 478 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ
โง ๐ง โ โ)
โง ((๐ฅ + ๐ง) = 0 โง 0 = (๐ฅ + (i ยท ๐ฆ)))) โ ((๐ฅ + ๐ง) + (i ยท ๐ฆ)) = (0 + ๐ง)) |
22 | | addlid 8096 |
. . . . . . . . . . . . . . . 16
โข ((i
ยท ๐ฆ) โ โ
โ (0 + (i ยท ๐ฆ))
= (i ยท ๐ฆ)) |
23 | 22 | 3ad2ant2 1019 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ
โง ๐ง โ โ)
โ (0 + (i ยท ๐ฆ))
= (i ยท ๐ฆ)) |
24 | 23 | adantr 276 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ
โง ๐ง โ โ)
โง ((๐ฅ + ๐ง) = 0 โง 0 = (๐ฅ + (i ยท ๐ฆ)))) โ (0 + (i ยท
๐ฆ)) = (i ยท ๐ฆ)) |
25 | 15, 21, 24 | 3eqtr3d 2218 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ
โง ๐ง โ โ)
โง ((๐ฅ + ๐ง) = 0 โง 0 = (๐ฅ + (i ยท ๐ฆ)))) โ (0 + ๐ง) = (i ยท ๐ฆ)) |
26 | 13, 25 | eqtr3d 2212 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ
โง ๐ง โ โ)
โง ((๐ฅ + ๐ง) = 0 โง 0 = (๐ฅ + (i ยท ๐ฆ)))) โ ๐ง = (i ยท ๐ฆ)) |
27 | 26 | ex 115 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ
โง ๐ง โ โ)
โ (((๐ฅ + ๐ง) = 0 โง 0 = (๐ฅ + (i ยท ๐ฆ))) โ ๐ง = (i ยท ๐ฆ))) |
28 | 5, 9, 10, 27 | syl3an 1280 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ง โ โ) โ (((๐ฅ + ๐ง) = 0 โง 0 = (๐ฅ + (i ยท ๐ฆ))) โ ๐ง = (i ยท ๐ฆ))) |
29 | 28 | 3expa 1203 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ (((๐ฅ + ๐ง) = 0 โง 0 = (๐ฅ + (i ยท ๐ฆ))) โ ๐ง = (i ยท ๐ฆ))) |
30 | 29 | imp 124 |
. . . . . . . 8
โข ((((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โง ((๐ฅ + ๐ง) = 0 โง 0 = (๐ฅ + (i ยท ๐ฆ)))) โ ๐ง = (i ยท ๐ฆ)) |
31 | | simplr 528 |
. . . . . . . 8
โข ((((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โง ((๐ฅ + ๐ง) = 0 โง 0 = (๐ฅ + (i ยท ๐ฆ)))) โ ๐ง โ โ) |
32 | 30, 31 | eqeltrrd 2255 |
. . . . . . 7
โข ((((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โง ((๐ฅ + ๐ง) = 0 โง 0 = (๐ฅ + (i ยท ๐ฆ)))) โ (i ยท ๐ฆ) โ โ) |
33 | 32 | exp32 365 |
. . . . . 6
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐ฅ + ๐ง) = 0 โ (0 = (๐ฅ + (i ยท ๐ฆ)) โ (i ยท ๐ฆ) โ โ))) |
34 | 33 | rexlimdva 2594 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
(โ๐ง โ โ
(๐ฅ + ๐ง) = 0 โ (0 = (๐ฅ + (i ยท ๐ฆ)) โ (i ยท ๐ฆ) โ โ))) |
35 | 4, 34 | mpd 13 |
. . . 4
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (0 =
(๐ฅ + (i ยท ๐ฆ)) โ (i ยท ๐ฆ) โ
โ)) |
36 | 35 | reximdva 2579 |
. . 3
โข (๐ฅ โ โ โ
(โ๐ฆ โ โ 0
= (๐ฅ + (i ยท ๐ฆ)) โ โ๐ฆ โ โ (i ยท
๐ฆ) โ
โ)) |
37 | 36 | rexlimiv 2588 |
. 2
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ 0 = (๐ฅ + (i
ยท ๐ฆ)) โ
โ๐ฆ โ โ (i
ยท ๐ฆ) โ
โ) |
38 | 1, 2, 37 | mp2b 8 |
1
โข
โ๐ฆ โ
โ (i ยท ๐ฆ)
โ โ |