Step | Hyp | Ref
| Expression |
1 | | cnre 11159 |
. 2
โข (๐ด โ โ โ
โ๐ โ โ
โ๐ โ โ
๐ด = (๐ + (i ยท ๐))) |
2 | | ax-rnegex 11129 |
. . . . . . 7
โข (๐ โ โ โ
โ๐ โ โ
(๐ + ๐) = 0) |
3 | | ax-rnegex 11129 |
. . . . . . 7
โข (๐ โ โ โ
โ๐ โ โ
(๐ + ๐) = 0) |
4 | 2, 3 | anim12i 614 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ
(โ๐ โ โ
(๐ + ๐) = 0 โง โ๐ โ โ (๐ + ๐) = 0)) |
5 | | reeanv 3220 |
. . . . . 6
โข
(โ๐ โ
โ โ๐ โ
โ ((๐ + ๐) = 0 โง (๐ + ๐) = 0) โ (โ๐ โ โ (๐ + ๐) = 0 โง โ๐ โ โ (๐ + ๐) = 0)) |
6 | 4, 5 | sylibr 233 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ
โ๐ โ โ
โ๐ โ โ
((๐ + ๐) = 0 โง (๐ + ๐) = 0)) |
7 | | ax-icn 11117 |
. . . . . . . . . . 11
โข i โ
โ |
8 | 7 | a1i 11 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ i โ
โ) |
9 | | simplrr 777 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ ๐ โ โ) |
10 | 9 | recnd 11190 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ ๐ โ โ) |
11 | 8, 10 | mulcld 11182 |
. . . . . . . . 9
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ (i ยท ๐) โ โ) |
12 | | simplrl 776 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ ๐ โ โ) |
13 | 12 | recnd 11190 |
. . . . . . . . 9
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ ๐ โ โ) |
14 | 11, 13 | addcld 11181 |
. . . . . . . 8
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ ((i ยท ๐) + ๐) โ โ) |
15 | | simplll 774 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ ๐ โ โ) |
16 | 15 | recnd 11190 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ ๐ โ โ) |
17 | | simpllr 775 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ ๐ โ โ) |
18 | 17 | recnd 11190 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ ๐ โ โ) |
19 | 8, 18 | mulcld 11182 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ (i ยท ๐) โ โ) |
20 | 16, 19, 11 | addassd 11184 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ ((๐ + (i ยท ๐)) + (i ยท ๐)) = (๐ + ((i ยท ๐) + (i ยท ๐)))) |
21 | 8, 18, 10 | adddid 11186 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ (i ยท (๐ + ๐)) = ((i ยท ๐) + (i ยท ๐))) |
22 | | simprr 772 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ (๐ + ๐) = 0) |
23 | 22 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ (i ยท (๐ + ๐)) = (i ยท 0)) |
24 | | mul01 11341 |
. . . . . . . . . . . . . . . 16
โข (i โ
โ โ (i ยท 0) = 0) |
25 | 7, 24 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข (i
ยท 0) = 0 |
26 | 23, 25 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ (i ยท (๐ + ๐)) = 0) |
27 | 21, 26 | eqtr3d 2779 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ ((i ยท ๐) + (i ยท ๐)) = 0) |
28 | 27 | oveq2d 7378 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ (๐ + ((i ยท ๐) + (i ยท ๐))) = (๐ + 0)) |
29 | | addid1 11342 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ + 0) = ๐) |
30 | 16, 29 | syl 17 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ (๐ + 0) = ๐) |
31 | 20, 28, 30 | 3eqtrd 2781 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ ((๐ + (i ยท ๐)) + (i ยท ๐)) = ๐) |
32 | 31 | oveq1d 7377 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ (((๐ + (i ยท ๐)) + (i ยท ๐)) + ๐) = (๐ + ๐)) |
33 | 16, 19 | addcld 11181 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ (๐ + (i ยท ๐)) โ โ) |
34 | 33, 11, 13 | addassd 11184 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ (((๐ + (i ยท ๐)) + (i ยท ๐)) + ๐) = ((๐ + (i ยท ๐)) + ((i ยท ๐) + ๐))) |
35 | 32, 34 | eqtr3d 2779 |
. . . . . . . . 9
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ (๐ + ๐) = ((๐ + (i ยท ๐)) + ((i ยท ๐) + ๐))) |
36 | | simprl 770 |
. . . . . . . . 9
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ (๐ + ๐) = 0) |
37 | 35, 36 | eqtr3d 2779 |
. . . . . . . 8
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ ((๐ + (i ยท ๐)) + ((i ยท ๐) + ๐)) = 0) |
38 | | oveq2 7370 |
. . . . . . . . . 10
โข (๐ฅ = ((i ยท ๐) + ๐) โ ((๐ + (i ยท ๐)) + ๐ฅ) = ((๐ + (i ยท ๐)) + ((i ยท ๐) + ๐))) |
39 | 38 | eqeq1d 2739 |
. . . . . . . . 9
โข (๐ฅ = ((i ยท ๐) + ๐) โ (((๐ + (i ยท ๐)) + ๐ฅ) = 0 โ ((๐ + (i ยท ๐)) + ((i ยท ๐) + ๐)) = 0)) |
40 | 39 | rspcev 3584 |
. . . . . . . 8
โข ((((i
ยท ๐) + ๐) โ โ โง ((๐ + (i ยท ๐)) + ((i ยท ๐) + ๐)) = 0) โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) + ๐ฅ) = 0) |
41 | 14, 37, 40 | syl2anc 585 |
. . . . . . 7
โข ((((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โง ((๐ + ๐) = 0 โง (๐ + ๐) = 0)) โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) + ๐ฅ) = 0) |
42 | 41 | ex 414 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ
(((๐ + ๐) = 0 โง (๐ + ๐) = 0) โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) + ๐ฅ) = 0)) |
43 | 42 | rexlimdvva 3206 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ
(โ๐ โ โ
โ๐ โ โ
((๐ + ๐) = 0 โง (๐ + ๐) = 0) โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) + ๐ฅ) = 0)) |
44 | 6, 43 | mpd 15 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ
โ๐ฅ โ โ
((๐ + (i ยท ๐)) + ๐ฅ) = 0) |
45 | | oveq1 7369 |
. . . . . 6
โข (๐ด = (๐ + (i ยท ๐)) โ (๐ด + ๐ฅ) = ((๐ + (i ยท ๐)) + ๐ฅ)) |
46 | 45 | eqeq1d 2739 |
. . . . 5
โข (๐ด = (๐ + (i ยท ๐)) โ ((๐ด + ๐ฅ) = 0 โ ((๐ + (i ยท ๐)) + ๐ฅ) = 0)) |
47 | 46 | rexbidv 3176 |
. . . 4
โข (๐ด = (๐ + (i ยท ๐)) โ (โ๐ฅ โ โ (๐ด + ๐ฅ) = 0 โ โ๐ฅ โ โ ((๐ + (i ยท ๐)) + ๐ฅ) = 0)) |
48 | 44, 47 | syl5ibrcom 247 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (๐ด = (๐ + (i ยท ๐)) โ โ๐ฅ โ โ (๐ด + ๐ฅ) = 0)) |
49 | 48 | rexlimivv 3197 |
. 2
โข
(โ๐ โ
โ โ๐ โ
โ ๐ด = (๐ + (i ยท ๐)) โ โ๐ฅ โ โ (๐ด + ๐ฅ) = 0) |
50 | 1, 49 | syl 17 |
1
โข (๐ด โ โ โ
โ๐ฅ โ โ
(๐ด + ๐ฅ) = 0) |