Step | Hyp | Ref
| Expression |
1 | | atandm 26242 |
. 2
โข (๐ด โ dom arctan โ (๐ด โ โ โง ๐ด โ -i โง ๐ด โ i)) |
2 | | 3anass 1096 |
. . 3
โข ((๐ด โ โ โง (1 โ
(i ยท ๐ด)) โ 0
โง (1 + (i ยท ๐ด))
โ 0) โ (๐ด โ
โ โง ((1 โ (i ยท ๐ด)) โ 0 โง (1 + (i ยท ๐ด)) โ 0))) |
3 | | ax-1cn 11116 |
. . . . . . . . . 10
โข 1 โ
โ |
4 | | ax-icn 11117 |
. . . . . . . . . . 11
โข i โ
โ |
5 | | mulcl 11142 |
. . . . . . . . . . 11
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
6 | 4, 5 | mpan 689 |
. . . . . . . . . 10
โข (๐ด โ โ โ (i
ยท ๐ด) โ
โ) |
7 | | subeq0 11434 |
. . . . . . . . . 10
โข ((1
โ โ โง (i ยท ๐ด) โ โ) โ ((1 โ (i
ยท ๐ด)) = 0 โ 1 =
(i ยท ๐ด))) |
8 | 3, 6, 7 | sylancr 588 |
. . . . . . . . 9
โข (๐ด โ โ โ ((1
โ (i ยท ๐ด)) = 0
โ 1 = (i ยท ๐ด))) |
9 | 4, 4 | mulneg2i 11609 |
. . . . . . . . . . . 12
โข (i
ยท -i) = -(i ยท i) |
10 | | ixi 11791 |
. . . . . . . . . . . . 13
โข (i
ยท i) = -1 |
11 | 10 | negeqi 11401 |
. . . . . . . . . . . 12
โข -(i
ยท i) = --1 |
12 | | negneg1e1 12278 |
. . . . . . . . . . . 12
โข --1 =
1 |
13 | 9, 11, 12 | 3eqtri 2769 |
. . . . . . . . . . 11
โข (i
ยท -i) = 1 |
14 | 13 | eqeq2i 2750 |
. . . . . . . . . 10
โข ((i
ยท ๐ด) = (i ยท
-i) โ (i ยท ๐ด) =
1) |
15 | | eqcom 2744 |
. . . . . . . . . 10
โข ((i
ยท ๐ด) = 1 โ 1 =
(i ยท ๐ด)) |
16 | 14, 15 | bitri 275 |
. . . . . . . . 9
โข ((i
ยท ๐ด) = (i ยท
-i) โ 1 = (i ยท ๐ด)) |
17 | 8, 16 | bitr4di 289 |
. . . . . . . 8
โข (๐ด โ โ โ ((1
โ (i ยท ๐ด)) = 0
โ (i ยท ๐ด) = (i
ยท -i))) |
18 | | id 22 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด โ
โ) |
19 | 4 | negcli 11476 |
. . . . . . . . . 10
โข -i โ
โ |
20 | 19 | a1i 11 |
. . . . . . . . 9
โข (๐ด โ โ โ -i โ
โ) |
21 | 4 | a1i 11 |
. . . . . . . . 9
โข (๐ด โ โ โ i โ
โ) |
22 | | ine0 11597 |
. . . . . . . . . 10
โข i โ
0 |
23 | 22 | a1i 11 |
. . . . . . . . 9
โข (๐ด โ โ โ i โ
0) |
24 | 18, 20, 21, 23 | mulcand 11795 |
. . . . . . . 8
โข (๐ด โ โ โ ((i
ยท ๐ด) = (i ยท
-i) โ ๐ด =
-i)) |
25 | 17, 24 | bitrd 279 |
. . . . . . 7
โข (๐ด โ โ โ ((1
โ (i ยท ๐ด)) = 0
โ ๐ด =
-i)) |
26 | 25 | necon3bid 2989 |
. . . . . 6
โข (๐ด โ โ โ ((1
โ (i ยท ๐ด))
โ 0 โ ๐ด โ
-i)) |
27 | | addcom 11348 |
. . . . . . . . . . . . 13
โข ((1
โ โ โง (i ยท ๐ด) โ โ) โ (1 + (i ยท
๐ด)) = ((i ยท ๐ด) + 1)) |
28 | 3, 6, 27 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ (1 + (i
ยท ๐ด)) = ((i ยท
๐ด) + 1)) |
29 | | subneg 11457 |
. . . . . . . . . . . . 13
โข (((i
ยท ๐ด) โ โ
โง 1 โ โ) โ ((i ยท ๐ด) โ -1) = ((i ยท ๐ด) + 1)) |
30 | 6, 3, 29 | sylancl 587 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ ((i
ยท ๐ด) โ -1) =
((i ยท ๐ด) +
1)) |
31 | 28, 30 | eqtr4d 2780 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (1 + (i
ยท ๐ด)) = ((i ยท
๐ด) โ
-1)) |
32 | 31 | eqeq1d 2739 |
. . . . . . . . . 10
โข (๐ด โ โ โ ((1 + (i
ยท ๐ด)) = 0 โ ((i
ยท ๐ด) โ -1) =
0)) |
33 | 3 | negcli 11476 |
. . . . . . . . . . 11
โข -1 โ
โ |
34 | | subeq0 11434 |
. . . . . . . . . . 11
โข (((i
ยท ๐ด) โ โ
โง -1 โ โ) โ (((i ยท ๐ด) โ -1) = 0 โ (i ยท ๐ด) = -1)) |
35 | 6, 33, 34 | sylancl 587 |
. . . . . . . . . 10
โข (๐ด โ โ โ (((i
ยท ๐ด) โ -1) = 0
โ (i ยท ๐ด) =
-1)) |
36 | 32, 35 | bitrd 279 |
. . . . . . . . 9
โข (๐ด โ โ โ ((1 + (i
ยท ๐ด)) = 0 โ (i
ยท ๐ด) =
-1)) |
37 | 10 | eqeq2i 2750 |
. . . . . . . . 9
โข ((i
ยท ๐ด) = (i ยท
i) โ (i ยท ๐ด) =
-1) |
38 | 36, 37 | bitr4di 289 |
. . . . . . . 8
โข (๐ด โ โ โ ((1 + (i
ยท ๐ด)) = 0 โ (i
ยท ๐ด) = (i ยท
i))) |
39 | 18, 21, 21, 23 | mulcand 11795 |
. . . . . . . 8
โข (๐ด โ โ โ ((i
ยท ๐ด) = (i ยท
i) โ ๐ด =
i)) |
40 | 38, 39 | bitrd 279 |
. . . . . . 7
โข (๐ด โ โ โ ((1 + (i
ยท ๐ด)) = 0 โ
๐ด = i)) |
41 | 40 | necon3bid 2989 |
. . . . . 6
โข (๐ด โ โ โ ((1 + (i
ยท ๐ด)) โ 0 โ
๐ด โ i)) |
42 | 26, 41 | anbi12d 632 |
. . . . 5
โข (๐ด โ โ โ (((1
โ (i ยท ๐ด))
โ 0 โง (1 + (i ยท ๐ด)) โ 0) โ (๐ด โ -i โง ๐ด โ i))) |
43 | 42 | pm5.32i 576 |
. . . 4
โข ((๐ด โ โ โง ((1
โ (i ยท ๐ด))
โ 0 โง (1 + (i ยท ๐ด)) โ 0)) โ (๐ด โ โ โง (๐ด โ -i โง ๐ด โ i))) |
44 | | 3anass 1096 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ -i โง ๐ด โ i) โ (๐ด โ โ โง (๐ด โ -i โง ๐ด โ i))) |
45 | 43, 44 | bitr4i 278 |
. . 3
โข ((๐ด โ โ โง ((1
โ (i ยท ๐ด))
โ 0 โง (1 + (i ยท ๐ด)) โ 0)) โ (๐ด โ โ โง ๐ด โ -i โง ๐ด โ i)) |
46 | 2, 45 | bitri 275 |
. 2
โข ((๐ด โ โ โง (1 โ
(i ยท ๐ด)) โ 0
โง (1 + (i ยท ๐ด))
โ 0) โ (๐ด โ
โ โง ๐ด โ -i
โง ๐ด โ
i)) |
47 | 1, 46 | bitr4i 278 |
1
โข (๐ด โ dom arctan โ (๐ด โ โ โง (1 โ
(i ยท ๐ด)) โ 0
โง (1 + (i ยท ๐ด))
โ 0)) |