Step | Hyp | Ref
| Expression |
1 | | ax-1cn 11168 |
. . . . . 6
β’ 1 β
β |
2 | | ax-icn 11169 |
. . . . . . 7
β’ i β
β |
3 | | simpl 484 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
π΄ β dom
arctan) |
4 | | atandm2 26382 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (π΄ β β β§ (1 β
(i Β· π΄)) β 0
β§ (1 + (i Β· π΄))
β 0)) |
5 | 3, 4 | sylib 217 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(π΄ β β β§ (1
β (i Β· π΄))
β 0 β§ (1 + (i Β· π΄)) β 0)) |
6 | 5 | simp1d 1143 |
. . . . . . 7
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
π΄ β
β) |
7 | | mulcl 11194 |
. . . . . . 7
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
8 | 2, 6, 7 | sylancr 588 |
. . . . . 6
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (i
Β· π΄) β
β) |
9 | | addcl 11192 |
. . . . . 6
β’ ((1
β β β§ (i Β· π΄) β β) β (1 + (i Β·
π΄)) β
β) |
10 | 1, 8, 9 | sylancr 588 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (1
+ (i Β· π΄)) β
β) |
11 | 5 | simp3d 1145 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (1
+ (i Β· π΄)) β
0) |
12 | 10, 11 | logcld 26079 |
. . . 4
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(logβ(1 + (i Β· π΄))) β β) |
13 | | subcl 11459 |
. . . . . 6
β’ ((1
β β β§ (i Β· π΄) β β) β (1 β (i
Β· π΄)) β
β) |
14 | 1, 8, 13 | sylancr 588 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (1
β (i Β· π΄))
β β) |
15 | 5 | simp2d 1144 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (1
β (i Β· π΄))
β 0) |
16 | 14, 15 | logcld 26079 |
. . . 4
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(logβ(1 β (i Β· π΄))) β β) |
17 | 12, 16 | imsubd 15164 |
. . 3
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) =
((ββ(logβ(1 + (i Β· π΄)))) β (ββ(logβ(1
β (i Β· π΄)))))) |
18 | 2 | a1i 11 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β i
β β) |
19 | 18, 6, 18 | subdid 11670 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (i
Β· (π΄ β i)) =
((i Β· π΄) β (i
Β· i))) |
20 | | ixi 11843 |
. . . . . . . . . . 11
β’ (i
Β· i) = -1 |
21 | 20 | oveq2i 7420 |
. . . . . . . . . 10
β’ ((i
Β· π΄) β (i
Β· i)) = ((i Β· π΄) β -1) |
22 | | subneg 11509 |
. . . . . . . . . . 11
β’ (((i
Β· π΄) β β
β§ 1 β β) β ((i Β· π΄) β -1) = ((i Β· π΄) + 1)) |
23 | 8, 1, 22 | sylancl 587 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((i Β· π΄) β -1)
= ((i Β· π΄) +
1)) |
24 | 21, 23 | eqtrid 2785 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((i Β· π΄) β (i
Β· i)) = ((i Β· π΄) + 1)) |
25 | | addcom 11400 |
. . . . . . . . . 10
β’ (((i
Β· π΄) β β
β§ 1 β β) β ((i Β· π΄) + 1) = (1 + (i Β· π΄))) |
26 | 8, 1, 25 | sylancl 587 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((i Β· π΄) + 1) = (1 +
(i Β· π΄))) |
27 | 19, 24, 26 | 3eqtrd 2777 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (i
Β· (π΄ β i)) =
(1 + (i Β· π΄))) |
28 | 27 | fveq2d 6896 |
. . . . . . 7
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(logβ(i Β· (π΄
β i))) = (logβ(1 + (i Β· π΄)))) |
29 | | subcl 11459 |
. . . . . . . . 9
β’ ((π΄ β β β§ i β
β) β (π΄ β
i) β β) |
30 | 6, 2, 29 | sylancl 587 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(π΄ β i) β
β) |
31 | | resub 15074 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ i β
β) β (ββ(π΄ β i)) = ((ββπ΄) β
(ββi))) |
32 | 6, 2, 31 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(π΄ β
i)) = ((ββπ΄)
β (ββi))) |
33 | | rei 15103 |
. . . . . . . . . . . . 13
β’
(ββi) = 0 |
34 | 33 | oveq2i 7420 |
. . . . . . . . . . . 12
β’
((ββπ΄)
β (ββi)) = ((ββπ΄) β 0) |
35 | 6 | recld 15141 |
. . . . . . . . . . . . . 14
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββπ΄) β
β) |
36 | 35 | recnd 11242 |
. . . . . . . . . . . . 13
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββπ΄) β
β) |
37 | 36 | subid1d 11560 |
. . . . . . . . . . . 12
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββπ΄) β
0) = (ββπ΄)) |
38 | 34, 37 | eqtrid 2785 |
. . . . . . . . . . 11
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββπ΄) β
(ββi)) = (ββπ΄)) |
39 | 32, 38 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(π΄ β
i)) = (ββπ΄)) |
40 | | gt0ne0 11679 |
. . . . . . . . . . 11
β’
(((ββπ΄)
β β β§ 0 < (ββπ΄)) β (ββπ΄) β 0) |
41 | 35, 40 | sylancom 589 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββπ΄) β
0) |
42 | 39, 41 | eqnetrd 3009 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(π΄ β
i)) β 0) |
43 | | fveq2 6892 |
. . . . . . . . . . 11
β’ ((π΄ β i) = 0 β
(ββ(π΄ β
i)) = (ββ0)) |
44 | | re0 15099 |
. . . . . . . . . . 11
β’
(ββ0) = 0 |
45 | 43, 44 | eqtrdi 2789 |
. . . . . . . . . 10
β’ ((π΄ β i) = 0 β
(ββ(π΄ β
i)) = 0) |
46 | 45 | necon3i 2974 |
. . . . . . . . 9
β’
((ββ(π΄
β i)) β 0 β (π΄ β i) β 0) |
47 | 42, 46 | syl 17 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(π΄ β i) β
0) |
48 | | simpr 486 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β 0
< (ββπ΄)) |
49 | | 0re 11216 |
. . . . . . . . . . 11
β’ 0 β
β |
50 | | ltle 11302 |
. . . . . . . . . . 11
β’ ((0
β β β§ (ββπ΄) β β) β (0 <
(ββπ΄) β 0
β€ (ββπ΄))) |
51 | 49, 35, 50 | sylancr 588 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (0
< (ββπ΄)
β 0 β€ (ββπ΄))) |
52 | 48, 51 | mpd 15 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β 0
β€ (ββπ΄)) |
53 | 52, 39 | breqtrrd 5177 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β 0
β€ (ββ(π΄
β i))) |
54 | | logimul 26122 |
. . . . . . . 8
β’ (((π΄ β i) β β β§
(π΄ β i) β 0 β§
0 β€ (ββ(π΄
β i))) β (logβ(i Β· (π΄ β i))) = ((logβ(π΄ β i)) + (i Β· (Ο
/ 2)))) |
55 | 30, 47, 53, 54 | syl3anc 1372 |
. . . . . . 7
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(logβ(i Β· (π΄
β i))) = ((logβ(π΄ β i)) + (i Β· (Ο /
2)))) |
56 | 28, 55 | eqtr3d 2775 |
. . . . . 6
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(logβ(1 + (i Β· π΄))) = ((logβ(π΄ β i)) + (i Β· (Ο /
2)))) |
57 | 56 | fveq2d 6896 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(logβ(1 + (i Β· π΄)))) = (ββ((logβ(π΄ β i)) + (i Β· (Ο
/ 2))))) |
58 | 30, 47 | logcld 26079 |
. . . . . . 7
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(logβ(π΄ β i))
β β) |
59 | | halfpire 25974 |
. . . . . . . . 9
β’ (Ο /
2) β β |
60 | 59 | recni 11228 |
. . . . . . . 8
β’ (Ο /
2) β β |
61 | 2, 60 | mulcli 11221 |
. . . . . . 7
β’ (i
Β· (Ο / 2)) β β |
62 | | imadd 15081 |
. . . . . . 7
β’
(((logβ(π΄
β i)) β β β§ (i Β· (Ο / 2)) β β) β
(ββ((logβ(π΄ β i)) + (i Β· (Ο / 2)))) =
((ββ(logβ(π΄ β i))) + (ββ(i Β·
(Ο / 2))))) |
63 | 58, 61, 62 | sylancl 587 |
. . . . . 6
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ((logβ(π΄ β i)) + (i Β· (Ο / 2)))) =
((ββ(logβ(π΄ β i))) + (ββ(i Β·
(Ο / 2))))) |
64 | | reim 15056 |
. . . . . . . . 9
β’ ((Ο /
2) β β β (ββ(Ο / 2)) = (ββ(i Β·
(Ο / 2)))) |
65 | 60, 64 | ax-mp 5 |
. . . . . . . 8
β’
(ββ(Ο / 2)) = (ββ(i Β· (Ο /
2))) |
66 | | rere 15069 |
. . . . . . . . 9
β’ ((Ο /
2) β β β (ββ(Ο / 2)) = (Ο /
2)) |
67 | 59, 66 | ax-mp 5 |
. . . . . . . 8
β’
(ββ(Ο / 2)) = (Ο / 2) |
68 | 65, 67 | eqtr3i 2763 |
. . . . . . 7
β’
(ββ(i Β· (Ο / 2))) = (Ο / 2) |
69 | 68 | oveq2i 7420 |
. . . . . 6
β’
((ββ(logβ(π΄ β i))) + (ββ(i Β·
(Ο / 2)))) = ((ββ(logβ(π΄ β i))) + (Ο / 2)) |
70 | 63, 69 | eqtrdi 2789 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ((logβ(π΄ β i)) + (i Β· (Ο / 2)))) =
((ββ(logβ(π΄ β i))) + (Ο /
2))) |
71 | 57, 70 | eqtrd 2773 |
. . . 4
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(logβ(1 + (i Β· π΄)))) = ((ββ(logβ(π΄ β i))) + (Ο /
2))) |
72 | | addcl 11192 |
. . . . . . . . . 10
β’ ((π΄ β β β§ i β
β) β (π΄ + i)
β β) |
73 | 6, 2, 72 | sylancl 587 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(π΄ + i) β
β) |
74 | | mulcl 11194 |
. . . . . . . . 9
β’ ((i
β β β§ (π΄ +
i) β β) β (i Β· (π΄ + i)) β β) |
75 | 2, 73, 74 | sylancr 588 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (i
Β· (π΄ + i)) β
β) |
76 | | reim 15056 |
. . . . . . . . . . 11
β’ ((π΄ + i) β β β
(ββ(π΄ + i)) =
(ββ(i Β· (π΄ + i)))) |
77 | 73, 76 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(π΄ + i)) =
(ββ(i Β· (π΄ + i)))) |
78 | | readd 15073 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ i β
β) β (ββ(π΄ + i)) = ((ββπ΄) + (ββi))) |
79 | 6, 2, 78 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(π΄ + i)) =
((ββπ΄) +
(ββi))) |
80 | 33 | oveq2i 7420 |
. . . . . . . . . . . 12
β’
((ββπ΄) +
(ββi)) = ((ββπ΄) + 0) |
81 | 36 | addridd 11414 |
. . . . . . . . . . . 12
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββπ΄) + 0) =
(ββπ΄)) |
82 | 80, 81 | eqtrid 2785 |
. . . . . . . . . . 11
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββπ΄) +
(ββi)) = (ββπ΄)) |
83 | 79, 82 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(π΄ + i)) =
(ββπ΄)) |
84 | 77, 83 | eqtr3d 2775 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(i Β· (π΄ + i))) = (ββπ΄)) |
85 | 48, 84 | breqtrrd 5177 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β 0
< (ββ(i Β· (π΄ + i)))) |
86 | | logneg2 26123 |
. . . . . . . 8
β’ (((i
Β· (π΄ + i)) β
β β§ 0 < (ββ(i Β· (π΄ + i)))) β (logβ-(i Β·
(π΄ + i))) = ((logβ(i
Β· (π΄ + i))) β
(i Β· Ο))) |
87 | 75, 85, 86 | syl2anc 585 |
. . . . . . 7
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(logβ-(i Β· (π΄
+ i))) = ((logβ(i Β· (π΄ + i))) β (i Β·
Ο))) |
88 | 18, 6, 18 | adddid 11238 |
. . . . . . . . . . 11
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (i
Β· (π΄ + i)) = ((i
Β· π΄) + (i Β·
i))) |
89 | 20 | oveq2i 7420 |
. . . . . . . . . . . 12
β’ ((i
Β· π΄) + (i Β·
i)) = ((i Β· π΄) +
-1) |
90 | | negsub 11508 |
. . . . . . . . . . . . 13
β’ (((i
Β· π΄) β β
β§ 1 β β) β ((i Β· π΄) + -1) = ((i Β· π΄) β 1)) |
91 | 8, 1, 90 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((i Β· π΄) + -1) = ((i
Β· π΄) β
1)) |
92 | 89, 91 | eqtrid 2785 |
. . . . . . . . . . 11
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((i Β· π΄) + (i
Β· i)) = ((i Β· π΄) β 1)) |
93 | 88, 92 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (i
Β· (π΄ + i)) = ((i
Β· π΄) β
1)) |
94 | 93 | negeqd 11454 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
-(i Β· (π΄ + i)) =
-((i Β· π΄) β
1)) |
95 | | negsubdi2 11519 |
. . . . . . . . . 10
β’ (((i
Β· π΄) β β
β§ 1 β β) β -((i Β· π΄) β 1) = (1 β (i Β· π΄))) |
96 | 8, 1, 95 | sylancl 587 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
-((i Β· π΄) β 1)
= (1 β (i Β· π΄))) |
97 | 94, 96 | eqtrd 2773 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
-(i Β· (π΄ + i)) = (1
β (i Β· π΄))) |
98 | 97 | fveq2d 6896 |
. . . . . . 7
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(logβ-(i Β· (π΄
+ i))) = (logβ(1 β (i Β· π΄)))) |
99 | 83, 41 | eqnetrd 3009 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(π΄ + i)) β
0) |
100 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ ((π΄ + i) = 0 β
(ββ(π΄ + i)) =
(ββ0)) |
101 | 100, 44 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ ((π΄ + i) = 0 β
(ββ(π΄ + i)) =
0) |
102 | 101 | necon3i 2974 |
. . . . . . . . . 10
β’
((ββ(π΄ +
i)) β 0 β (π΄ + i)
β 0) |
103 | 99, 102 | syl 17 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(π΄ + i) β
0) |
104 | 73, 103 | logcld 26079 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(logβ(π΄ + i)) β
β) |
105 | 61 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (i
Β· (Ο / 2)) β β) |
106 | | picn 25969 |
. . . . . . . . . 10
β’ Ο
β β |
107 | 2, 106 | mulcli 11221 |
. . . . . . . . 9
β’ (i
Β· Ο) β β |
108 | 107 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (i
Β· Ο) β β) |
109 | 52, 83 | breqtrrd 5177 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β 0
β€ (ββ(π΄ +
i))) |
110 | | logimul 26122 |
. . . . . . . . . 10
β’ (((π΄ + i) β β β§
(π΄ + i) β 0 β§ 0 β€
(ββ(π΄ + i)))
β (logβ(i Β· (π΄ + i))) = ((logβ(π΄ + i)) + (i Β· (Ο /
2)))) |
111 | 73, 103, 109, 110 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(logβ(i Β· (π΄ +
i))) = ((logβ(π΄ + i))
+ (i Β· (Ο / 2)))) |
112 | 111 | oveq1d 7424 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((logβ(i Β· (π΄
+ i))) β (i Β· Ο)) = (((logβ(π΄ + i)) + (i Β· (Ο / 2))) β (i
Β· Ο))) |
113 | 104, 105,
108, 112 | assraddsubd 11628 |
. . . . . . 7
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((logβ(i Β· (π΄
+ i))) β (i Β· Ο)) = ((logβ(π΄ + i)) + ((i Β· (Ο / 2)) β (i
Β· Ο)))) |
114 | 87, 98, 113 | 3eqtr3d 2781 |
. . . . . 6
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(logβ(1 β (i Β· π΄))) = ((logβ(π΄ + i)) + ((i Β· (Ο / 2)) β (i
Β· Ο)))) |
115 | 114 | fveq2d 6896 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(logβ(1 β (i Β· π΄)))) = (ββ((logβ(π΄ + i)) + ((i Β· (Ο /
2)) β (i Β· Ο))))) |
116 | 61, 107 | subcli 11536 |
. . . . . . 7
β’ ((i
Β· (Ο / 2)) β (i Β· Ο)) β β |
117 | | imadd 15081 |
. . . . . . 7
β’
(((logβ(π΄ +
i)) β β β§ ((i Β· (Ο / 2)) β (i Β· Ο))
β β) β (ββ((logβ(π΄ + i)) + ((i Β· (Ο / 2)) β (i
Β· Ο)))) = ((ββ(logβ(π΄ + i))) + (ββ((i Β· (Ο
/ 2)) β (i Β· Ο))))) |
118 | 104, 116,
117 | sylancl 587 |
. . . . . 6
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ((logβ(π΄ + i)) + ((i Β· (Ο / 2)) β (i
Β· Ο)))) = ((ββ(logβ(π΄ + i))) + (ββ((i Β· (Ο
/ 2)) β (i Β· Ο))))) |
119 | | imsub 15082 |
. . . . . . . . 9
β’ (((i
Β· (Ο / 2)) β β β§ (i Β· Ο) β β)
β (ββ((i Β· (Ο / 2)) β (i Β· Ο))) =
((ββ(i Β· (Ο / 2))) β (ββ(i Β·
Ο)))) |
120 | 61, 107, 119 | mp2an 691 |
. . . . . . . 8
β’
(ββ((i Β· (Ο / 2)) β (i Β· Ο))) =
((ββ(i Β· (Ο / 2))) β (ββ(i Β·
Ο))) |
121 | | reim 15056 |
. . . . . . . . . . 11
β’ (Ο
β β β (ββΟ) = (ββ(i Β·
Ο))) |
122 | 106, 121 | ax-mp 5 |
. . . . . . . . . 10
β’
(ββΟ) = (ββ(i Β· Ο)) |
123 | | pire 25968 |
. . . . . . . . . . 11
β’ Ο
β β |
124 | | rere 15069 |
. . . . . . . . . . 11
β’ (Ο
β β β (ββΟ) = Ο) |
125 | 123, 124 | ax-mp 5 |
. . . . . . . . . 10
β’
(ββΟ) = Ο |
126 | 122, 125 | eqtr3i 2763 |
. . . . . . . . 9
β’
(ββ(i Β· Ο)) = Ο |
127 | 68, 126 | oveq12i 7421 |
. . . . . . . 8
β’
((ββ(i Β· (Ο / 2))) β (ββ(i
Β· Ο))) = ((Ο / 2) β Ο) |
128 | 60 | negcli 11528 |
. . . . . . . . 9
β’ -(Ο /
2) β β |
129 | 106, 60 | negsubi 11538 |
. . . . . . . . . 10
β’ (Ο +
-(Ο / 2)) = (Ο β (Ο / 2)) |
130 | | pidiv2halves 25977 |
. . . . . . . . . . 11
β’ ((Ο /
2) + (Ο / 2)) = Ο |
131 | 106, 60, 60, 130 | subaddrii 11549 |
. . . . . . . . . 10
β’ (Ο
β (Ο / 2)) = (Ο / 2) |
132 | 129, 131 | eqtri 2761 |
. . . . . . . . 9
β’ (Ο +
-(Ο / 2)) = (Ο / 2) |
133 | 60, 106, 128, 132 | subaddrii 11549 |
. . . . . . . 8
β’ ((Ο /
2) β Ο) = -(Ο / 2) |
134 | 120, 127,
133 | 3eqtri 2765 |
. . . . . . 7
β’
(ββ((i Β· (Ο / 2)) β (i Β· Ο))) =
-(Ο / 2) |
135 | 134 | oveq2i 7420 |
. . . . . 6
β’
((ββ(logβ(π΄ + i))) + (ββ((i Β· (Ο
/ 2)) β (i Β· Ο)))) = ((ββ(logβ(π΄ + i))) + -(Ο /
2)) |
136 | 118, 135 | eqtrdi 2789 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ((logβ(π΄ + i)) + ((i Β· (Ο / 2)) β (i
Β· Ο)))) = ((ββ(logβ(π΄ + i))) + -(Ο / 2))) |
137 | 115, 136 | eqtrd 2773 |
. . . 4
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(logβ(1 β (i Β· π΄)))) = ((ββ(logβ(π΄ + i))) + -(Ο /
2))) |
138 | 71, 137 | oveq12d 7427 |
. . 3
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββ(logβ(1 + (i Β· π΄)))) β (ββ(logβ(1
β (i Β· π΄)))))
= (((ββ(logβ(π΄ β i))) + (Ο / 2)) β
((ββ(logβ(π΄ + i))) + -(Ο / 2)))) |
139 | 58 | imcld 15142 |
. . . . . 6
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(logβ(π΄ β i))) β
β) |
140 | 139 | recnd 11242 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(logβ(π΄ β i))) β
β) |
141 | 60 | a1i 11 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(Ο / 2) β β) |
142 | 104 | imcld 15142 |
. . . . . 6
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(logβ(π΄ + i))) β β) |
143 | 142 | recnd 11242 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(logβ(π΄ + i))) β β) |
144 | 128 | a1i 11 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
-(Ο / 2) β β) |
145 | 140, 141,
143, 144 | addsub4d 11618 |
. . . 4
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(((ββ(logβ(π΄ β i))) + (Ο / 2)) β
((ββ(logβ(π΄ + i))) + -(Ο / 2))) =
(((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + ((Ο / 2) β -(Ο /
2)))) |
146 | 60, 60 | subnegi 11539 |
. . . . . 6
β’ ((Ο /
2) β -(Ο / 2)) = ((Ο / 2) + (Ο / 2)) |
147 | 146, 130 | eqtri 2761 |
. . . . 5
β’ ((Ο /
2) β -(Ο / 2)) = Ο |
148 | 147 | oveq2i 7420 |
. . . 4
β’
(((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + ((Ο / 2) β -(Ο / 2)))
= (((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) |
149 | 145, 148 | eqtrdi 2789 |
. . 3
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(((ββ(logβ(π΄ β i))) + (Ο / 2)) β
((ββ(logβ(π΄ + i))) + -(Ο / 2))) =
(((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο)) |
150 | 17, 138, 149 | 3eqtrd 2777 |
. 2
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) =
(((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο)) |
151 | 139, 142 | resubcld 11642 |
. . . 4
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) β β) |
152 | | readdcl 11193 |
. . . 4
β’
((((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) β β β§ Ο β
β) β (((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) β
β) |
153 | 151, 123,
152 | sylancl 587 |
. . 3
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) β
β) |
154 | 123 | renegcli 11521 |
. . . . . . 7
β’ -Ο
β β |
155 | 154 | recni 11228 |
. . . . . 6
β’ -Ο
β β |
156 | 155, 106 | negsubi 11538 |
. . . . 5
β’ (-Ο +
-Ο) = (-Ο β Ο) |
157 | 154 | a1i 11 |
. . . . . . 7
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
-Ο β β) |
158 | 142 | renegcld 11641 |
. . . . . . 7
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
-(ββ(logβ(π΄ + i))) β β) |
159 | 30, 47 | logimcld 26080 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(-Ο < (ββ(logβ(π΄ β i))) β§
(ββ(logβ(π΄ β i))) β€ Ο)) |
160 | 159 | simpld 496 |
. . . . . . 7
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
-Ο < (ββ(logβ(π΄ β i)))) |
161 | 73, 103 | logimcld 26080 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(-Ο < (ββ(logβ(π΄ + i))) β§
(ββ(logβ(π΄ + i))) β€ Ο)) |
162 | 161 | simprd 497 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(logβ(π΄ + i))) β€ Ο) |
163 | | leneg 11717 |
. . . . . . . . 9
β’
(((ββ(logβ(π΄ + i))) β β β§ Ο β
β) β ((ββ(logβ(π΄ + i))) β€ Ο β -Ο β€
-(ββ(logβ(π΄ + i))))) |
164 | 142, 123,
163 | sylancl 587 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββ(logβ(π΄ + i))) β€ Ο β -Ο β€
-(ββ(logβ(π΄ + i))))) |
165 | 162, 164 | mpbid 231 |
. . . . . . 7
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
-Ο β€ -(ββ(logβ(π΄ + i)))) |
166 | 157, 157,
139, 158, 160, 165 | ltleaddd 11835 |
. . . . . 6
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(-Ο + -Ο) < ((ββ(logβ(π΄ β i))) +
-(ββ(logβ(π΄ + i))))) |
167 | 140, 143 | negsubd 11577 |
. . . . . 6
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββ(logβ(π΄ β i))) +
-(ββ(logβ(π΄ + i)))) = ((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i))))) |
168 | 166, 167 | breqtrd 5175 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(-Ο + -Ο) < ((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i))))) |
169 | 156, 168 | eqbrtrrid 5185 |
. . . 4
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(-Ο β Ο) < ((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i))))) |
170 | 123 | a1i 11 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
Ο β β) |
171 | 157, 170,
151 | ltsubaddd 11810 |
. . . 4
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((-Ο β Ο) < ((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) β -Ο <
(((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο))) |
172 | 169, 171 | mpbid 231 |
. . 3
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
-Ο < (((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο)) |
173 | | 0red 11217 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β 0
β β) |
174 | 6 | imcld 15142 |
. . . . . . . . . . . . 13
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββπ΄) β
β) |
175 | | peano2rem 11527 |
. . . . . . . . . . . . 13
β’
((ββπ΄)
β β β ((ββπ΄) β 1) β
β) |
176 | 174, 175 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββπ΄) β
1) β β) |
177 | | peano2re 11387 |
. . . . . . . . . . . . 13
β’
((ββπ΄)
β β β ((ββπ΄) + 1) β β) |
178 | 174, 177 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββπ΄) + 1)
β β) |
179 | 174 | ltm1d 12146 |
. . . . . . . . . . . 12
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββπ΄) β
1) < (ββπ΄)) |
180 | 174 | ltp1d 12144 |
. . . . . . . . . . . 12
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββπ΄) <
((ββπ΄) +
1)) |
181 | 176, 174,
178, 179, 180 | lttrd 11375 |
. . . . . . . . . . 11
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββπ΄) β
1) < ((ββπ΄)
+ 1)) |
182 | | ltdiv1 12078 |
. . . . . . . . . . . 12
β’
((((ββπ΄)
β 1) β β β§ ((ββπ΄) + 1) β β β§
((ββπ΄) β
β β§ 0 < (ββπ΄))) β (((ββπ΄) β 1) <
((ββπ΄) + 1)
β (((ββπ΄)
β 1) / (ββπ΄)) < (((ββπ΄) + 1) / (ββπ΄)))) |
183 | 176, 178,
35, 48, 182 | syl112anc 1375 |
. . . . . . . . . . 11
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(((ββπ΄) β
1) < ((ββπ΄)
+ 1) β (((ββπ΄) β 1) / (ββπ΄)) < (((ββπ΄) + 1) / (ββπ΄)))) |
184 | 181, 183 | mpbid 231 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(((ββπ΄) β
1) / (ββπ΄)) <
(((ββπ΄) + 1) /
(ββπ΄))) |
185 | | imsub 15082 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ i β
β) β (ββ(π΄ β i)) = ((ββπ΄) β
(ββi))) |
186 | 6, 2, 185 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(π΄ β
i)) = ((ββπ΄)
β (ββi))) |
187 | | imi 15104 |
. . . . . . . . . . . . 13
β’
(ββi) = 1 |
188 | 187 | oveq2i 7420 |
. . . . . . . . . . . 12
β’
((ββπ΄)
β (ββi)) = ((ββπ΄) β 1) |
189 | 186, 188 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(π΄ β
i)) = ((ββπ΄)
β 1)) |
190 | 189, 39 | oveq12d 7427 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββ(π΄ β
i)) / (ββ(π΄
β i))) = (((ββπ΄) β 1) / (ββπ΄))) |
191 | | imadd 15081 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ i β
β) β (ββ(π΄ + i)) = ((ββπ΄) + (ββi))) |
192 | 6, 2, 191 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(π΄ + i)) =
((ββπ΄) +
(ββi))) |
193 | 187 | oveq2i 7420 |
. . . . . . . . . . . 12
β’
((ββπ΄) +
(ββi)) = ((ββπ΄) + 1) |
194 | 192, 193 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(π΄ + i)) =
((ββπ΄) +
1)) |
195 | 194, 83 | oveq12d 7427 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββ(π΄ + i)) /
(ββ(π΄ + i))) =
(((ββπ΄) + 1) /
(ββπ΄))) |
196 | 184, 190,
195 | 3brtr4d 5181 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββ(π΄ β
i)) / (ββ(π΄
β i))) < ((ββ(π΄ + i)) / (ββ(π΄ + i)))) |
197 | | tanarg 26127 |
. . . . . . . . . 10
β’ (((π΄ β i) β β β§
(ββ(π΄ β
i)) β 0) β (tanβ(ββ(logβ(π΄ β i)))) = ((ββ(π΄ β i)) /
(ββ(π΄ β
i)))) |
198 | 30, 42, 197 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(tanβ(ββ(logβ(π΄ β i)))) = ((ββ(π΄ β i)) /
(ββ(π΄ β
i)))) |
199 | | tanarg 26127 |
. . . . . . . . . 10
β’ (((π΄ + i) β β β§
(ββ(π΄ + i)) β
0) β (tanβ(ββ(logβ(π΄ + i)))) = ((ββ(π΄ + i)) / (ββ(π΄ + i)))) |
200 | 73, 99, 199 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(tanβ(ββ(logβ(π΄ + i)))) = ((ββ(π΄ + i)) / (ββ(π΄ + i)))) |
201 | 196, 198,
200 | 3brtr4d 5181 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(tanβ(ββ(logβ(π΄ β i)))) <
(tanβ(ββ(logβ(π΄ + i))))) |
202 | 48, 39 | breqtrrd 5177 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β 0
< (ββ(π΄
β i))) |
203 | | argregt0 26118 |
. . . . . . . . . 10
β’ (((π΄ β i) β β β§
0 < (ββ(π΄
β i))) β (ββ(logβ(π΄ β i))) β (-(Ο / 2)(,)(Ο /
2))) |
204 | 30, 202, 203 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(logβ(π΄ β i))) β (-(Ο / 2)(,)(Ο /
2))) |
205 | 48, 83 | breqtrrd 5177 |
. . . . . . . . . 10
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β 0
< (ββ(π΄ +
i))) |
206 | | argregt0 26118 |
. . . . . . . . . 10
β’ (((π΄ + i) β β β§ 0
< (ββ(π΄ +
i))) β (ββ(logβ(π΄ + i))) β (-(Ο / 2)(,)(Ο /
2))) |
207 | 73, 205, 206 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(logβ(π΄ + i))) β (-(Ο / 2)(,)(Ο /
2))) |
208 | | tanord 26047 |
. . . . . . . . 9
β’
(((ββ(logβ(π΄ β i))) β (-(Ο / 2)(,)(Ο /
2)) β§ (ββ(logβ(π΄ + i))) β (-(Ο / 2)(,)(Ο / 2)))
β ((ββ(logβ(π΄ β i))) <
(ββ(logβ(π΄ + i))) β
(tanβ(ββ(logβ(π΄ β i)))) <
(tanβ(ββ(logβ(π΄ + i)))))) |
209 | 204, 207,
208 | syl2anc 585 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββ(logβ(π΄ β i))) <
(ββ(logβ(π΄ + i))) β
(tanβ(ββ(logβ(π΄ β i)))) <
(tanβ(ββ(logβ(π΄ + i)))))) |
210 | 201, 209 | mpbird 257 |
. . . . . . 7
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(logβ(π΄ β i))) <
(ββ(logβ(π΄ + i)))) |
211 | 143 | addlidd 11415 |
. . . . . . 7
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β (0
+ (ββ(logβ(π΄ + i)))) = (ββ(logβ(π΄ + i)))) |
212 | 210, 211 | breqtrrd 5177 |
. . . . . 6
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ(logβ(π΄ β i))) < (0 +
(ββ(logβ(π΄ + i))))) |
213 | 139, 142,
173 | ltsubaddd 11810 |
. . . . . 6
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) < 0 β
(ββ(logβ(π΄ β i))) < (0 +
(ββ(logβ(π΄ + i)))))) |
214 | 212, 213 | mpbird 257 |
. . . . 5
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) < 0) |
215 | 151, 173,
170, 214 | ltadd1dd 11825 |
. . . 4
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) < (0 +
Ο)) |
216 | 106 | addlidi 11402 |
. . . 4
β’ (0 +
Ο) = Ο |
217 | 215, 216 | breqtrdi 5190 |
. . 3
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) < Ο) |
218 | 154 | rexri 11272 |
. . . 4
β’ -Ο
β β* |
219 | 123 | rexri 11272 |
. . . 4
β’ Ο
β β* |
220 | | elioo2 13365 |
. . . 4
β’ ((-Ο
β β* β§ Ο β β*) β
((((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) β (-Ο(,)Ο)
β ((((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) β β β§ -Ο
< (((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) β§
(((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) <
Ο))) |
221 | 218, 219,
220 | mp2an 691 |
. . 3
β’
((((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) β (-Ο(,)Ο)
β ((((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) β β β§ -Ο
< (((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) β§
(((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) <
Ο)) |
222 | 153, 172,
217, 221 | syl3anbrc 1344 |
. 2
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(((ββ(logβ(π΄ β i))) β
(ββ(logβ(π΄ + i)))) + Ο) β
(-Ο(,)Ο)) |
223 | 150, 222 | eqeltrd 2834 |
1
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) β
(-Ο(,)Ο)) |