Step | Hyp | Ref
| Expression |
1 | | imcl 15003 |
. . . . 5
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
2 | 1 | adantr 482 |
. . . 4
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (โโ๐ด)
โ โ) |
3 | 2 | renegcld 11589 |
. . 3
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ -(โโ๐ด)
โ โ) |
4 | | ax-1cn 11116 |
. . . . . 6
โข 1 โ
โ |
5 | | sqcl 14030 |
. . . . . . 7
โข (๐ด โ โ โ (๐ดโ2) โ
โ) |
6 | 5 | adantr 482 |
. . . . . 6
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (๐ดโ2) โ
โ) |
7 | | subcl 11407 |
. . . . . 6
โข ((1
โ โ โง (๐ดโ2) โ โ) โ (1 โ
(๐ดโ2)) โ
โ) |
8 | 4, 6, 7 | sylancr 588 |
. . . . 5
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (1 โ (๐ดโ2)) โ โ) |
9 | 8 | sqrtcld 15329 |
. . . 4
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (โโ(1 โ (๐ดโ2))) โ โ) |
10 | 9 | recld 15086 |
. . 3
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (โโ(โโ(1 โ (๐ดโ2)))) โ โ) |
11 | 1 | le0neg1d 11733 |
. . . 4
โข (๐ด โ โ โ
((โโ๐ด) โค 0
โ 0 โค -(โโ๐ด))) |
12 | 11 | biimpa 478 |
. . 3
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ 0 โค -(โโ๐ด)) |
13 | 8 | sqrtrege0d 15330 |
. . 3
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ 0 โค (โโ(โโ(1 โ (๐ดโ2))))) |
14 | 3, 10, 12, 13 | addge0d 11738 |
. 2
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ 0 โค (-(โโ๐ด) + (โโ(โโ(1 โ
(๐ดโ2)))))) |
15 | | ax-icn 11117 |
. . . . 5
โข i โ
โ |
16 | | simpl 484 |
. . . . 5
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ ๐ด โ
โ) |
17 | | mulcl 11142 |
. . . . 5
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
18 | 15, 16, 17 | sylancr 588 |
. . . 4
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (i ยท ๐ด)
โ โ) |
19 | 18, 9 | readdd 15106 |
. . 3
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (โโ((i ยท ๐ด) + (โโ(1 โ (๐ดโ2))))) = ((โโ(i
ยท ๐ด)) +
(โโ(โโ(1 โ (๐ดโ2)))))) |
20 | | negicn 11409 |
. . . . . . 7
โข -i โ
โ |
21 | | mulcl 11142 |
. . . . . . 7
โข ((-i
โ โ โง ๐ด
โ โ) โ (-i ยท ๐ด) โ โ) |
22 | 20, 16, 21 | sylancr 588 |
. . . . . 6
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (-i ยท ๐ด)
โ โ) |
23 | 22 | renegd 15101 |
. . . . 5
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (โโ-(-i ยท ๐ด)) = -(โโ(-i ยท ๐ด))) |
24 | 15 | negnegi 11478 |
. . . . . . . 8
โข --i =
i |
25 | 24 | oveq1i 7372 |
. . . . . . 7
โข (--i
ยท ๐ด) = (i ยท
๐ด) |
26 | | mulneg1 11598 |
. . . . . . . 8
โข ((-i
โ โ โง ๐ด
โ โ) โ (--i ยท ๐ด) = -(-i ยท ๐ด)) |
27 | 20, 16, 26 | sylancr 588 |
. . . . . . 7
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (--i ยท ๐ด) =
-(-i ยท ๐ด)) |
28 | 25, 27 | eqtr3id 2791 |
. . . . . 6
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (i ยท ๐ด) =
-(-i ยท ๐ด)) |
29 | 28 | fveq2d 6851 |
. . . . 5
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (โโ(i ยท ๐ด)) = (โโ-(-i ยท ๐ด))) |
30 | | imre 15000 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ๐ด) =
(โโ(-i ยท ๐ด))) |
31 | 30 | adantr 482 |
. . . . . 6
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (โโ๐ด) =
(โโ(-i ยท ๐ด))) |
32 | 31 | negeqd 11402 |
. . . . 5
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ -(โโ๐ด) =
-(โโ(-i ยท ๐ด))) |
33 | 23, 29, 32 | 3eqtr4d 2787 |
. . . 4
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (โโ(i ยท ๐ด)) = -(โโ๐ด)) |
34 | 33 | oveq1d 7377 |
. . 3
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ ((โโ(i ยท ๐ด)) + (โโ(โโ(1 โ
(๐ดโ2))))) =
(-(โโ๐ด) +
(โโ(โโ(1 โ (๐ดโ2)))))) |
35 | 19, 34 | eqtrd 2777 |
. 2
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ (โโ((i ยท ๐ด) + (โโ(1 โ (๐ดโ2))))) =
(-(โโ๐ด) +
(โโ(โโ(1 โ (๐ดโ2)))))) |
36 | 14, 35 | breqtrrd 5138 |
1
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ 0 โค (โโ((i ยท ๐ด) + (โโ(1 โ (๐ดโ2)))))) |