Step | Hyp | Ref
| Expression |
1 | | ax-icn 11118 |
. . . 4
โข i โ
โ |
2 | | resqrtcl 15147 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
๐ด) โ
(โโ๐ด) โ
โ) |
3 | | recn 11149 |
. . . . 5
โข
((โโ๐ด)
โ โ โ (โโ๐ด) โ โ) |
4 | 2, 3 | syl 17 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ
(โโ๐ด) โ
โ) |
5 | | sqmul 14033 |
. . . 4
โข ((i
โ โ โง (โโ๐ด) โ โ) โ ((i ยท
(โโ๐ด))โ2)
= ((iโ2) ยท ((โโ๐ด)โ2))) |
6 | 1, 4, 5 | sylancr 588 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((i ยท
(โโ๐ด))โ2)
= ((iโ2) ยท ((โโ๐ด)โ2))) |
7 | | i2 14115 |
. . . . 5
โข
(iโ2) = -1 |
8 | 7 | a1i 11 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ (iโ2) =
-1) |
9 | | resqrtth 15149 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ
((โโ๐ด)โ2)
= ๐ด) |
10 | 8, 9 | oveq12d 7379 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((iโ2)
ยท ((โโ๐ด)โ2)) = (-1 ยท ๐ด)) |
11 | | recn 11149 |
. . . . 5
โข (๐ด โ โ โ ๐ด โ
โ) |
12 | 11 | adantr 482 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ ๐ด โ โ) |
13 | 12 | mulm1d 11615 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ (-1 ยท
๐ด) = -๐ด) |
14 | 6, 10, 13 | 3eqtrd 2777 |
. 2
โข ((๐ด โ โ โง 0 โค
๐ด) โ ((i ยท
(โโ๐ด))โ2)
= -๐ด) |
15 | | renegcl 11472 |
. . . 4
โข
((โโ๐ด)
โ โ โ -(โโ๐ด) โ โ) |
16 | | 0re 11165 |
. . . . 5
โข 0 โ
โ |
17 | | reim0 15012 |
. . . . . 6
โข
(-(โโ๐ด)
โ โ โ (โโ-(โโ๐ด)) = 0) |
18 | | recn 11149 |
. . . . . . 7
โข
(-(โโ๐ด)
โ โ โ -(โโ๐ด) โ โ) |
19 | | imre 15002 |
. . . . . . 7
โข
(-(โโ๐ด)
โ โ โ (โโ-(โโ๐ด)) = (โโ(-i ยท
-(โโ๐ด)))) |
20 | 18, 19 | syl 17 |
. . . . . 6
โข
(-(โโ๐ด)
โ โ โ (โโ-(โโ๐ด)) = (โโ(-i ยท
-(โโ๐ด)))) |
21 | 17, 20 | eqtr3d 2775 |
. . . . 5
โข
(-(โโ๐ด)
โ โ โ 0 = (โโ(-i ยท -(โโ๐ด)))) |
22 | | eqle 11265 |
. . . . 5
โข ((0
โ โ โง 0 = (โโ(-i ยท -(โโ๐ด)))) โ 0 โค
(โโ(-i ยท -(โโ๐ด)))) |
23 | 16, 21, 22 | sylancr 588 |
. . . 4
โข
(-(โโ๐ด)
โ โ โ 0 โค (โโ(-i ยท -(โโ๐ด)))) |
24 | 2, 15, 23 | 3syl 18 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ 0 โค
(โโ(-i ยท -(โโ๐ด)))) |
25 | | mul2neg 11602 |
. . . . 5
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (-i ยท
-(โโ๐ด)) = (i
ยท (โโ๐ด))) |
26 | 1, 4, 25 | sylancr 588 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ (-i ยท
-(โโ๐ด)) = (i
ยท (โโ๐ด))) |
27 | 26 | fveq2d 6850 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ (โโ(-i
ยท -(โโ๐ด))) = (โโ(i ยท
(โโ๐ด)))) |
28 | 24, 27 | breqtrd 5135 |
. 2
โข ((๐ด โ โ โง 0 โค
๐ด) โ 0 โค
(โโ(i ยท (โโ๐ด)))) |
29 | | ixi 11792 |
. . . . . . 7
โข (i
ยท i) = -1 |
30 | 29 | oveq1i 7371 |
. . . . . 6
โข ((i
ยท i) ยท (โโ๐ด)) = (-1 ยท (โโ๐ด)) |
31 | | mulass 11147 |
. . . . . . 7
โข ((i
โ โ โง i โ โ โง (โโ๐ด) โ โ) โ ((i ยท i)
ยท (โโ๐ด))
= (i ยท (i ยท (โโ๐ด)))) |
32 | 1, 1, 31 | mp3an12 1452 |
. . . . . 6
โข
((โโ๐ด)
โ โ โ ((i ยท i) ยท (โโ๐ด)) = (i ยท (i ยท
(โโ๐ด)))) |
33 | | mulm1 11604 |
. . . . . 6
โข
((โโ๐ด)
โ โ โ (-1 ยท (โโ๐ด)) = -(โโ๐ด)) |
34 | 30, 32, 33 | 3eqtr3a 2797 |
. . . . 5
โข
((โโ๐ด)
โ โ โ (i ยท (i ยท (โโ๐ด))) = -(โโ๐ด)) |
35 | 4, 34 | syl 17 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ (i ยท (i
ยท (โโ๐ด))) = -(โโ๐ด)) |
36 | | sqrtge0 15151 |
. . . . . 6
โข ((๐ด โ โ โง 0 โค
๐ด) โ 0 โค
(โโ๐ด)) |
37 | | le0neg2 11672 |
. . . . . . . 8
โข
((โโ๐ด)
โ โ โ (0 โค (โโ๐ด) โ -(โโ๐ด) โค 0)) |
38 | | lenlt 11241 |
. . . . . . . . 9
โข
((-(โโ๐ด)
โ โ โง 0 โ โ) โ (-(โโ๐ด) โค 0 โ ยฌ 0 <
-(โโ๐ด))) |
39 | 15, 16, 38 | sylancl 587 |
. . . . . . . 8
โข
((โโ๐ด)
โ โ โ (-(โโ๐ด) โค 0 โ ยฌ 0 <
-(โโ๐ด))) |
40 | 37, 39 | bitrd 279 |
. . . . . . 7
โข
((โโ๐ด)
โ โ โ (0 โค (โโ๐ด) โ ยฌ 0 < -(โโ๐ด))) |
41 | 2, 40 | syl 17 |
. . . . . 6
โข ((๐ด โ โ โง 0 โค
๐ด) โ (0 โค
(โโ๐ด) โ
ยฌ 0 < -(โโ๐ด))) |
42 | 36, 41 | mpbid 231 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
๐ด) โ ยฌ 0 <
-(โโ๐ด)) |
43 | | elrp 12925 |
. . . . . 6
โข
(-(โโ๐ด)
โ โ+ โ (-(โโ๐ด) โ โ โง 0 <
-(โโ๐ด))) |
44 | 2, 15 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
๐ด) โ
-(โโ๐ด) โ
โ) |
45 | 44 | biantrurd 534 |
. . . . . 6
โข ((๐ด โ โ โง 0 โค
๐ด) โ (0 <
-(โโ๐ด) โ
(-(โโ๐ด) โ
โ โง 0 < -(โโ๐ด)))) |
46 | 43, 45 | bitr4id 290 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
๐ด) โ
(-(โโ๐ด) โ
โ+ โ 0 < -(โโ๐ด))) |
47 | 42, 46 | mtbird 325 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ ยฌ
-(โโ๐ด) โ
โ+) |
48 | 35, 47 | eqneltrd 2854 |
. . 3
โข ((๐ด โ โ โง 0 โค
๐ด) โ ยฌ (i ยท
(i ยท (โโ๐ด))) โ
โ+) |
49 | | df-nel 3047 |
. . 3
โข ((i
ยท (i ยท (โโ๐ด))) โ โ+ โ ยฌ
(i ยท (i ยท (โโ๐ด))) โ
โ+) |
50 | 48, 49 | sylibr 233 |
. 2
โข ((๐ด โ โ โง 0 โค
๐ด) โ (i ยท (i
ยท (โโ๐ด))) โ
โ+) |
51 | 14, 28, 50 | 3jca 1129 |
1
โข ((๐ด โ โ โง 0 โค
๐ด) โ (((i ยท
(โโ๐ด))โ2)
= -๐ด โง 0 โค
(โโ(i ยท (โโ๐ด))) โง (i ยท (i ยท
(โโ๐ด))) โ
โ+)) |