Step | Hyp | Ref
| Expression |
1 | | df-nel 3048 |
. . . . . 6
โข (-(i
ยท ๐ด) โ
โ+ โ ยฌ -(i ยท ๐ด) โ
โ+) |
2 | | simpr 486 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (โโ๐ด) =
0) |
3 | | 0le0 12313 |
. . . . . . . 8
โข 0 โค
0 |
4 | 2, 3 | eqbrtrdi 5188 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (โโ๐ด)
โค 0) |
5 | 4 | biantrurd 534 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (-(i ยท ๐ด)
โ โ+ โ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ
โ+))) |
6 | 1, 5 | bitr3id 285 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (ยฌ -(i ยท ๐ด) โ โ+ โ
((โโ๐ด) โค 0
โง -(i ยท ๐ด)
โ โ+))) |
7 | 6 | con1bid 356 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (ยฌ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ โ+)
โ -(i ยท ๐ด)
โ โ+)) |
8 | | ax-icn 11169 |
. . . . . . . . . . . 12
โข i โ
โ |
9 | | mulcl 11194 |
. . . . . . . . . . . 12
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
10 | 8, 9 | mpan 689 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (i
ยท ๐ด) โ
โ) |
11 | | reim0b 15066 |
. . . . . . . . . . 11
โข ((i
ยท ๐ด) โ โ
โ ((i ยท ๐ด)
โ โ โ (โโ(i ยท ๐ด)) = 0)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
โข (๐ด โ โ โ ((i
ยท ๐ด) โ โ
โ (โโ(i ยท ๐ด)) = 0)) |
13 | | imre 15055 |
. . . . . . . . . . . . 13
โข ((i
ยท ๐ด) โ โ
โ (โโ(i ยท ๐ด)) = (โโ(-i ยท (i ยท
๐ด)))) |
14 | 10, 13 | syl 17 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
(โโ(i ยท ๐ด)) = (โโ(-i ยท (i ยท
๐ด)))) |
15 | | ine0 11649 |
. . . . . . . . . . . . . . . . 17
โข i โ
0 |
16 | | divrec2 11889 |
. . . . . . . . . . . . . . . . 17
โข (((i
ยท ๐ด) โ โ
โง i โ โ โง i โ 0) โ ((i ยท ๐ด) / i) = ((1 / i) ยท (i ยท ๐ด))) |
17 | 8, 15, 16 | mp3an23 1454 |
. . . . . . . . . . . . . . . 16
โข ((i
ยท ๐ด) โ โ
โ ((i ยท ๐ด) / i)
= ((1 / i) ยท (i ยท ๐ด))) |
18 | 10, 17 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ โ ((i
ยท ๐ด) / i) = ((1 / i)
ยท (i ยท ๐ด))) |
19 | | irec 14165 |
. . . . . . . . . . . . . . . 16
โข (1 / i) =
-i |
20 | 19 | oveq1i 7419 |
. . . . . . . . . . . . . . 15
โข ((1 / i)
ยท (i ยท ๐ด)) =
(-i ยท (i ยท ๐ด)) |
21 | 18, 20 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ ((i
ยท ๐ด) / i) = (-i
ยท (i ยท ๐ด))) |
22 | | divcan3 11898 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง i โ
โ โง i โ 0) โ ((i ยท ๐ด) / i) = ๐ด) |
23 | 8, 15, 22 | mp3an23 1454 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ ((i
ยท ๐ด) / i) = ๐ด) |
24 | 21, 23 | eqtr3d 2775 |
. . . . . . . . . . . . 13
โข (๐ด โ โ โ (-i
ยท (i ยท ๐ด)) =
๐ด) |
25 | 24 | fveq2d 6896 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
(โโ(-i ยท (i ยท ๐ด))) = (โโ๐ด)) |
26 | 14, 25 | eqtrd 2773 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(โโ(i ยท ๐ด)) = (โโ๐ด)) |
27 | 26 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ด โ โ โ
((โโ(i ยท ๐ด)) = 0 โ (โโ๐ด) = 0)) |
28 | 12, 27 | bitrd 279 |
. . . . . . . . 9
โข (๐ด โ โ โ ((i
ยท ๐ด) โ โ
โ (โโ๐ด) =
0)) |
29 | 28 | biimpar 479 |
. . . . . . . 8
โข ((๐ด โ โ โง
(โโ๐ด) = 0)
โ (i ยท ๐ด)
โ โ) |
30 | 29 | adantlr 714 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (i ยท ๐ด)
โ โ) |
31 | | mulne0 11856 |
. . . . . . . . 9
โข (((i
โ โ โง i โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ (i ยท ๐ด) โ 0) |
32 | 8, 15, 31 | mpanl12 701 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0) โ (i ยท
๐ด) โ 0) |
33 | 32 | adantr 482 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (i ยท ๐ด) โ
0) |
34 | | rpneg 13006 |
. . . . . . 7
โข (((i
ยท ๐ด) โ โ
โง (i ยท ๐ด) โ
0) โ ((i ยท ๐ด)
โ โ+ โ ยฌ -(i ยท ๐ด) โ
โ+)) |
35 | 30, 33, 34 | syl2anc 585 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ ((i ยท ๐ด)
โ โ+ โ ยฌ -(i ยท ๐ด) โ
โ+)) |
36 | 35 | con2bid 355 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (-(i ยท ๐ด)
โ โ+ โ ยฌ (i ยท ๐ด) โ
โ+)) |
37 | | df-nel 3048 |
. . . . 5
โข ((i
ยท ๐ด) โ
โ+ โ ยฌ (i ยท ๐ด) โ
โ+) |
38 | 36, 37 | bitr4di 289 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (-(i ยท ๐ด)
โ โ+ โ (i ยท ๐ด) โ
โ+)) |
39 | 3, 2 | breqtrrid 5187 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ 0 โค (โโ๐ด)) |
40 | 39 | biantrurd 534 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ ((i ยท ๐ด)
โ โ+ โ (0 โค (โโ๐ด) โง (i ยท ๐ด) โ
โ+))) |
41 | 7, 38, 40 | 3bitrrd 306 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ ((0 โค (โโ๐ด) โง (i ยท ๐ด) โ โ+) โ ยฌ
((โโ๐ด) โค 0
โง -(i ยท ๐ด)
โ โ+))) |
42 | 28 | adantr 482 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ 0) โ ((i ยท
๐ด) โ โ โ
(โโ๐ด) =
0)) |
43 | 42 | necon3bbid 2979 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0) โ (ยฌ (i
ยท ๐ด) โ โ
โ (โโ๐ด)
โ 0)) |
44 | 43 | biimpar 479 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ยฌ (i ยท ๐ด)
โ โ) |
45 | | rpre 12982 |
. . . . . . . 8
โข ((i
ยท ๐ด) โ
โ+ โ (i ยท ๐ด) โ โ) |
46 | 44, 45 | nsyl 140 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ยฌ (i ยท ๐ด)
โ โ+) |
47 | 46, 37 | sylibr 233 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (i ยท ๐ด)
โ โ+) |
48 | 47 | biantrud 533 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (0 โค (โโ๐ด) โ (0 โค (โโ๐ด) โง (i ยท ๐ด) โ
โ+))) |
49 | | simpr 486 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (โโ๐ด)
โ 0) |
50 | 49 | biantrud 533 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (0 โค (โโ๐ด) โ (0 โค (โโ๐ด) โง (โโ๐ด) โ 0))) |
51 | | 0re 11216 |
. . . . . . . 8
โข 0 โ
โ |
52 | | recl 15057 |
. . . . . . . 8
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
53 | | ltlen 11315 |
. . . . . . . . 9
โข ((0
โ โ โง (โโ๐ด) โ โ) โ (0 <
(โโ๐ด) โ (0
โค (โโ๐ด) โง
(โโ๐ด) โ
0))) |
54 | | ltnle 11293 |
. . . . . . . . 9
โข ((0
โ โ โง (โโ๐ด) โ โ) โ (0 <
(โโ๐ด) โ
ยฌ (โโ๐ด) โค
0)) |
55 | 53, 54 | bitr3d 281 |
. . . . . . . 8
โข ((0
โ โ โง (โโ๐ด) โ โ) โ ((0 โค
(โโ๐ด) โง
(โโ๐ด) โ 0)
โ ยฌ (โโ๐ด) โค 0)) |
56 | 51, 52, 55 | sylancr 588 |
. . . . . . 7
โข (๐ด โ โ โ ((0 โค
(โโ๐ด) โง
(โโ๐ด) โ 0)
โ ยฌ (โโ๐ด) โค 0)) |
57 | 56 | ad2antrr 725 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ((0 โค (โโ๐ด) โง (โโ๐ด) โ 0) โ ยฌ (โโ๐ด) โค 0)) |
58 | 50, 57 | bitrd 279 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (0 โค (โโ๐ด) โ ยฌ (โโ๐ด) โค 0)) |
59 | 48, 58 | bitr3d 281 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ((0 โค (โโ๐ด) โง (i ยท ๐ด) โ โ+) โ ยฌ
(โโ๐ด) โค
0)) |
60 | | renegcl 11523 |
. . . . . . . . . 10
โข (-(i
ยท ๐ด) โ โ
โ --(i ยท ๐ด)
โ โ) |
61 | 10 | negnegd 11562 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ --(i
ยท ๐ด) = (i ยท
๐ด)) |
62 | 61 | eleq1d 2819 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (--(i
ยท ๐ด) โ โ
โ (i ยท ๐ด)
โ โ)) |
63 | 62 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (--(i ยท ๐ด)
โ โ โ (i ยท ๐ด) โ โ)) |
64 | 60, 63 | imbitrid 243 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (-(i ยท ๐ด)
โ โ โ (i ยท ๐ด) โ โ)) |
65 | 44, 64 | mtod 197 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ยฌ -(i ยท ๐ด) โ โ) |
66 | | rpre 12982 |
. . . . . . . 8
โข (-(i
ยท ๐ด) โ
โ+ โ -(i ยท ๐ด) โ โ) |
67 | 65, 66 | nsyl 140 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ยฌ -(i ยท ๐ด) โ
โ+) |
68 | 67, 1 | sylibr 233 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ -(i ยท ๐ด)
โ โ+) |
69 | 68 | biantrud 533 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ((โโ๐ด)
โค 0 โ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ
โ+))) |
70 | 69 | notbid 318 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (ยฌ (โโ๐ด) โค 0 โ ยฌ ((โโ๐ด) โค 0 โง -(i ยท
๐ด) โ
โ+))) |
71 | 59, 70 | bitrd 279 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ((0 โค (โโ๐ด) โง (i ยท ๐ด) โ โ+) โ ยฌ
((โโ๐ด) โค 0
โง -(i ยท ๐ด)
โ โ+))) |
72 | 41, 71 | pm2.61dane 3030 |
. 2
โข ((๐ด โ โ โง ๐ด โ 0) โ ((0 โค
(โโ๐ด) โง (i
ยท ๐ด) โ
โ+) โ ยฌ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ
โ+))) |
73 | | reneg 15072 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ-๐ด) =
-(โโ๐ด)) |
74 | 73 | breq2d 5161 |
. . . . . 6
โข (๐ด โ โ โ (0 โค
(โโ-๐ด) โ 0
โค -(โโ๐ด))) |
75 | 52 | le0neg1d 11785 |
. . . . . 6
โข (๐ด โ โ โ
((โโ๐ด) โค 0
โ 0 โค -(โโ๐ด))) |
76 | 74, 75 | bitr4d 282 |
. . . . 5
โข (๐ด โ โ โ (0 โค
(โโ-๐ด) โ
(โโ๐ด) โค
0)) |
77 | | mulneg2 11651 |
. . . . . . 7
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท -๐ด) = -(i ยท ๐ด)) |
78 | 8, 77 | mpan 689 |
. . . . . 6
โข (๐ด โ โ โ (i
ยท -๐ด) = -(i ยท
๐ด)) |
79 | | neleq1 3053 |
. . . . . 6
โข ((i
ยท -๐ด) = -(i ยท
๐ด) โ ((i ยท
-๐ด) โ
โ+ โ -(i ยท ๐ด) โ
โ+)) |
80 | 78, 79 | syl 17 |
. . . . 5
โข (๐ด โ โ โ ((i
ยท -๐ด) โ
โ+ โ -(i ยท ๐ด) โ
โ+)) |
81 | 76, 80 | anbi12d 632 |
. . . 4
โข (๐ด โ โ โ ((0 โค
(โโ-๐ด) โง (i
ยท -๐ด) โ
โ+) โ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ
โ+))) |
82 | 81 | notbid 318 |
. . 3
โข (๐ด โ โ โ (ยฌ (0
โค (โโ-๐ด)
โง (i ยท -๐ด)
โ โ+) โ ยฌ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ
โ+))) |
83 | 82 | adantr 482 |
. 2
โข ((๐ด โ โ โง ๐ด โ 0) โ (ยฌ (0 โค
(โโ-๐ด) โง (i
ยท -๐ด) โ
โ+) โ ยฌ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ
โ+))) |
84 | 72, 83 | bitr4d 282 |
1
โข ((๐ด โ โ โง ๐ด โ 0) โ ((0 โค
(โโ๐ด) โง (i
ยท ๐ด) โ
โ+) โ ยฌ (0 โค (โโ-๐ด) โง (i ยท -๐ด) โ
โ+))) |