Step | Hyp | Ref
| Expression |
1 | | df-nel 3047 |
. . . . . 6
โข (-(i
ยท ๐ด) โ
โ+ โ ยฌ -(i ยท ๐ด) โ
โ+) |
2 | | simpr 485 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (โโ๐ด) =
0) |
3 | | 0le0 12309 |
. . . . . . . 8
โข 0 โค
0 |
4 | 2, 3 | eqbrtrdi 5186 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (โโ๐ด)
โค 0) |
5 | 4 | biantrurd 533 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (-(i ยท ๐ด)
โ โ+ โ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ
โ+))) |
6 | 1, 5 | bitr3id 284 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (ยฌ -(i ยท ๐ด) โ โ+ โ
((โโ๐ด) โค 0
โง -(i ยท ๐ด)
โ โ+))) |
7 | 6 | con1bid 355 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (ยฌ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ โ+)
โ -(i ยท ๐ด)
โ โ+)) |
8 | | ax-icn 11165 |
. . . . . . . . . . . 12
โข i โ
โ |
9 | | mulcl 11190 |
. . . . . . . . . . . 12
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
10 | 8, 9 | mpan 688 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (i
ยท ๐ด) โ
โ) |
11 | | reim0b 15062 |
. . . . . . . . . . 11
โข ((i
ยท ๐ด) โ โ
โ ((i ยท ๐ด)
โ โ โ (โโ(i ยท ๐ด)) = 0)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
โข (๐ด โ โ โ ((i
ยท ๐ด) โ โ
โ (โโ(i ยท ๐ด)) = 0)) |
13 | | imre 15051 |
. . . . . . . . . . . . 13
โข ((i
ยท ๐ด) โ โ
โ (โโ(i ยท ๐ด)) = (โโ(-i ยท (i ยท
๐ด)))) |
14 | 10, 13 | syl 17 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
(โโ(i ยท ๐ด)) = (โโ(-i ยท (i ยท
๐ด)))) |
15 | | ine0 11645 |
. . . . . . . . . . . . . . . . 17
โข i โ
0 |
16 | | divrec2 11885 |
. . . . . . . . . . . . . . . . 17
โข (((i
ยท ๐ด) โ โ
โง i โ โ โง i โ 0) โ ((i ยท ๐ด) / i) = ((1 / i) ยท (i ยท ๐ด))) |
17 | 8, 15, 16 | mp3an23 1453 |
. . . . . . . . . . . . . . . 16
โข ((i
ยท ๐ด) โ โ
โ ((i ยท ๐ด) / i)
= ((1 / i) ยท (i ยท ๐ด))) |
18 | 10, 17 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ โ ((i
ยท ๐ด) / i) = ((1 / i)
ยท (i ยท ๐ด))) |
19 | | irec 14161 |
. . . . . . . . . . . . . . . 16
โข (1 / i) =
-i |
20 | 19 | oveq1i 7415 |
. . . . . . . . . . . . . . 15
โข ((1 / i)
ยท (i ยท ๐ด)) =
(-i ยท (i ยท ๐ด)) |
21 | 18, 20 | eqtrdi 2788 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ ((i
ยท ๐ด) / i) = (-i
ยท (i ยท ๐ด))) |
22 | | divcan3 11894 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง i โ
โ โง i โ 0) โ ((i ยท ๐ด) / i) = ๐ด) |
23 | 8, 15, 22 | mp3an23 1453 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ ((i
ยท ๐ด) / i) = ๐ด) |
24 | 21, 23 | eqtr3d 2774 |
. . . . . . . . . . . . 13
โข (๐ด โ โ โ (-i
ยท (i ยท ๐ด)) =
๐ด) |
25 | 24 | fveq2d 6892 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
(โโ(-i ยท (i ยท ๐ด))) = (โโ๐ด)) |
26 | 14, 25 | eqtrd 2772 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(โโ(i ยท ๐ด)) = (โโ๐ด)) |
27 | 26 | eqeq1d 2734 |
. . . . . . . . . 10
โข (๐ด โ โ โ
((โโ(i ยท ๐ด)) = 0 โ (โโ๐ด) = 0)) |
28 | 12, 27 | bitrd 278 |
. . . . . . . . 9
โข (๐ด โ โ โ ((i
ยท ๐ด) โ โ
โ (โโ๐ด) =
0)) |
29 | 28 | biimpar 478 |
. . . . . . . 8
โข ((๐ด โ โ โง
(โโ๐ด) = 0)
โ (i ยท ๐ด)
โ โ) |
30 | 29 | adantlr 713 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (i ยท ๐ด)
โ โ) |
31 | | mulne0 11852 |
. . . . . . . . 9
โข (((i
โ โ โง i โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ (i ยท ๐ด) โ 0) |
32 | 8, 15, 31 | mpanl12 700 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0) โ (i ยท
๐ด) โ 0) |
33 | 32 | adantr 481 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (i ยท ๐ด) โ
0) |
34 | | rpneg 13002 |
. . . . . . 7
โข (((i
ยท ๐ด) โ โ
โง (i ยท ๐ด) โ
0) โ ((i ยท ๐ด)
โ โ+ โ ยฌ -(i ยท ๐ด) โ
โ+)) |
35 | 30, 33, 34 | syl2anc 584 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ ((i ยท ๐ด)
โ โ+ โ ยฌ -(i ยท ๐ด) โ
โ+)) |
36 | 35 | con2bid 354 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (-(i ยท ๐ด)
โ โ+ โ ยฌ (i ยท ๐ด) โ
โ+)) |
37 | | df-nel 3047 |
. . . . 5
โข ((i
ยท ๐ด) โ
โ+ โ ยฌ (i ยท ๐ด) โ
โ+) |
38 | 36, 37 | bitr4di 288 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ (-(i ยท ๐ด)
โ โ+ โ (i ยท ๐ด) โ
โ+)) |
39 | 3, 2 | breqtrrid 5185 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ 0 โค (โโ๐ด)) |
40 | 39 | biantrurd 533 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ ((i ยท ๐ด)
โ โ+ โ (0 โค (โโ๐ด) โง (i ยท ๐ด) โ
โ+))) |
41 | 7, 38, 40 | 3bitrrd 305 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) = 0)
โ ((0 โค (โโ๐ด) โง (i ยท ๐ด) โ โ+) โ ยฌ
((โโ๐ด) โค 0
โง -(i ยท ๐ด)
โ โ+))) |
42 | 28 | adantr 481 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ 0) โ ((i ยท
๐ด) โ โ โ
(โโ๐ด) =
0)) |
43 | 42 | necon3bbid 2978 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0) โ (ยฌ (i
ยท ๐ด) โ โ
โ (โโ๐ด)
โ 0)) |
44 | 43 | biimpar 478 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ยฌ (i ยท ๐ด)
โ โ) |
45 | | rpre 12978 |
. . . . . . . 8
โข ((i
ยท ๐ด) โ
โ+ โ (i ยท ๐ด) โ โ) |
46 | 44, 45 | nsyl 140 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ยฌ (i ยท ๐ด)
โ โ+) |
47 | 46, 37 | sylibr 233 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (i ยท ๐ด)
โ โ+) |
48 | 47 | biantrud 532 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (0 โค (โโ๐ด) โ (0 โค (โโ๐ด) โง (i ยท ๐ด) โ
โ+))) |
49 | | simpr 485 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (โโ๐ด)
โ 0) |
50 | 49 | biantrud 532 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (0 โค (โโ๐ด) โ (0 โค (โโ๐ด) โง (โโ๐ด) โ 0))) |
51 | | 0re 11212 |
. . . . . . . 8
โข 0 โ
โ |
52 | | recl 15053 |
. . . . . . . 8
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
53 | | ltlen 11311 |
. . . . . . . . 9
โข ((0
โ โ โง (โโ๐ด) โ โ) โ (0 <
(โโ๐ด) โ (0
โค (โโ๐ด) โง
(โโ๐ด) โ
0))) |
54 | | ltnle 11289 |
. . . . . . . . 9
โข ((0
โ โ โง (โโ๐ด) โ โ) โ (0 <
(โโ๐ด) โ
ยฌ (โโ๐ด) โค
0)) |
55 | 53, 54 | bitr3d 280 |
. . . . . . . 8
โข ((0
โ โ โง (โโ๐ด) โ โ) โ ((0 โค
(โโ๐ด) โง
(โโ๐ด) โ 0)
โ ยฌ (โโ๐ด) โค 0)) |
56 | 51, 52, 55 | sylancr 587 |
. . . . . . 7
โข (๐ด โ โ โ ((0 โค
(โโ๐ด) โง
(โโ๐ด) โ 0)
โ ยฌ (โโ๐ด) โค 0)) |
57 | 56 | ad2antrr 724 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ((0 โค (โโ๐ด) โง (โโ๐ด) โ 0) โ ยฌ (โโ๐ด) โค 0)) |
58 | 50, 57 | bitrd 278 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (0 โค (โโ๐ด) โ ยฌ (โโ๐ด) โค 0)) |
59 | 48, 58 | bitr3d 280 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ((0 โค (โโ๐ด) โง (i ยท ๐ด) โ โ+) โ ยฌ
(โโ๐ด) โค
0)) |
60 | | renegcl 11519 |
. . . . . . . . . 10
โข (-(i
ยท ๐ด) โ โ
โ --(i ยท ๐ด)
โ โ) |
61 | 10 | negnegd 11558 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ --(i
ยท ๐ด) = (i ยท
๐ด)) |
62 | 61 | eleq1d 2818 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (--(i
ยท ๐ด) โ โ
โ (i ยท ๐ด)
โ โ)) |
63 | 62 | ad2antrr 724 |
. . . . . . . . . 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 12978 |
. . . . . . . 8
โข (-(i
ยท ๐ด) โ
โ+ โ -(i ยท ๐ด) โ โ) |
67 | 65, 66 | nsyl 140 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ยฌ -(i ยท ๐ด) โ
โ+) |
68 | 67, 1 | sylibr 233 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ -(i ยท ๐ด)
โ โ+) |
69 | 68 | biantrud 532 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ((โโ๐ด)
โค 0 โ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ
โ+))) |
70 | 69 | notbid 317 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ (ยฌ (โโ๐ด) โค 0 โ ยฌ ((โโ๐ด) โค 0 โง -(i ยท
๐ด) โ
โ+))) |
71 | 59, 70 | bitrd 278 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง
(โโ๐ด) โ 0)
โ ((0 โค (โโ๐ด) โง (i ยท ๐ด) โ โ+) โ ยฌ
((โโ๐ด) โค 0
โง -(i ยท ๐ด)
โ โ+))) |
72 | 41, 71 | pm2.61dane 3029 |
. 2
โข ((๐ด โ โ โง ๐ด โ 0) โ ((0 โค
(โโ๐ด) โง (i
ยท ๐ด) โ
โ+) โ ยฌ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ
โ+))) |
73 | | reneg 15068 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ-๐ด) =
-(โโ๐ด)) |
74 | 73 | breq2d 5159 |
. . . . . 6
โข (๐ด โ โ โ (0 โค
(โโ-๐ด) โ 0
โค -(โโ๐ด))) |
75 | 52 | le0neg1d 11781 |
. . . . . 6
โข (๐ด โ โ โ
((โโ๐ด) โค 0
โ 0 โค -(โโ๐ด))) |
76 | 74, 75 | bitr4d 281 |
. . . . 5
โข (๐ด โ โ โ (0 โค
(โโ-๐ด) โ
(โโ๐ด) โค
0)) |
77 | | mulneg2 11647 |
. . . . . . 7
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท -๐ด) = -(i ยท ๐ด)) |
78 | 8, 77 | mpan 688 |
. . . . . 6
โข (๐ด โ โ โ (i
ยท -๐ด) = -(i ยท
๐ด)) |
79 | | neleq1 3052 |
. . . . . 6
โข ((i
ยท -๐ด) = -(i ยท
๐ด) โ ((i ยท
-๐ด) โ
โ+ โ -(i ยท ๐ด) โ
โ+)) |
80 | 78, 79 | syl 17 |
. . . . 5
โข (๐ด โ โ โ ((i
ยท -๐ด) โ
โ+ โ -(i ยท ๐ด) โ
โ+)) |
81 | 76, 80 | anbi12d 631 |
. . . 4
โข (๐ด โ โ โ ((0 โค
(โโ-๐ด) โง (i
ยท -๐ด) โ
โ+) โ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ
โ+))) |
82 | 81 | notbid 317 |
. . 3
โข (๐ด โ โ โ (ยฌ (0
โค (โโ-๐ด)
โง (i ยท -๐ด)
โ โ+) โ ยฌ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ
โ+))) |
83 | 82 | adantr 481 |
. 2
โข ((๐ด โ โ โง ๐ด โ 0) โ (ยฌ (0 โค
(โโ-๐ด) โง (i
ยท -๐ด) โ
โ+) โ ยฌ ((โโ๐ด) โค 0 โง -(i ยท ๐ด) โ
โ+))) |
84 | 72, 83 | bitr4d 281 |
1
โข ((๐ด โ โ โง ๐ด โ 0) โ ((0 โค
(โโ๐ด) โง (i
ยท ๐ด) โ
โ+) โ ยฌ (0 โค (โโ-๐ด) โง (i ยท -๐ด) โ
โ+))) |