Step | Hyp | Ref
| Expression |
1 | | rpre 12930 |
. . 3
β’ (π΄ β β+
β π΄ β
β) |
2 | | atanrecl 26277 |
. . 3
β’ (π΄ β β β
(arctanβπ΄) β
β) |
3 | 1, 2 | syl 17 |
. 2
β’ (π΄ β β+
β (arctanβπ΄)
β β) |
4 | | picn 25832 |
. . . 4
β’ Ο
β β |
5 | | 2cn 12235 |
. . . 4
β’ 2 β
β |
6 | | 2ne0 12264 |
. . . 4
β’ 2 β
0 |
7 | | divneg 11854 |
. . . 4
β’ ((Ο
β β β§ 2 β β β§ 2 β 0) β -(Ο / 2) =
(-Ο / 2)) |
8 | 4, 5, 6, 7 | mp3an 1462 |
. . 3
β’ -(Ο /
2) = (-Ο / 2) |
9 | | ax-1cn 11116 |
. . . . . . . . . . . 12
β’ 1 β
β |
10 | | ax-icn 11117 |
. . . . . . . . . . . . 13
β’ i β
β |
11 | 1 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (π΄ β β+
β π΄ β
β) |
12 | | mulcl 11142 |
. . . . . . . . . . . . 13
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
13 | 10, 11, 12 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π΄ β β+
β (i Β· π΄)
β β) |
14 | | addcl 11140 |
. . . . . . . . . . . 12
β’ ((1
β β β§ (i Β· π΄) β β) β (1 + (i Β·
π΄)) β
β) |
15 | 9, 13, 14 | sylancr 588 |
. . . . . . . . . . 11
β’ (π΄ β β+
β (1 + (i Β· π΄))
β β) |
16 | | atanre 26251 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β π΄ β dom
arctan) |
17 | 1, 16 | syl 17 |
. . . . . . . . . . . . 13
β’ (π΄ β β+
β π΄ β dom
arctan) |
18 | | atandm2 26243 |
. . . . . . . . . . . . 13
β’ (π΄ β dom arctan β (π΄ β β β§ (1 β
(i Β· π΄)) β 0
β§ (1 + (i Β· π΄))
β 0)) |
19 | 17, 18 | sylib 217 |
. . . . . . . . . . . 12
β’ (π΄ β β+
β (π΄ β β
β§ (1 β (i Β· π΄)) β 0 β§ (1 + (i Β· π΄)) β 0)) |
20 | 19 | simp3d 1145 |
. . . . . . . . . . 11
β’ (π΄ β β+
β (1 + (i Β· π΄))
β 0) |
21 | 15, 20 | logcld 25942 |
. . . . . . . . . 10
β’ (π΄ β β+
β (logβ(1 + (i Β· π΄))) β β) |
22 | | subcl 11407 |
. . . . . . . . . . . 12
β’ ((1
β β β§ (i Β· π΄) β β) β (1 β (i
Β· π΄)) β
β) |
23 | 9, 13, 22 | sylancr 588 |
. . . . . . . . . . 11
β’ (π΄ β β+
β (1 β (i Β· π΄)) β β) |
24 | 19 | simp2d 1144 |
. . . . . . . . . . 11
β’ (π΄ β β+
β (1 β (i Β· π΄)) β 0) |
25 | 23, 24 | logcld 25942 |
. . . . . . . . . 10
β’ (π΄ β β+
β (logβ(1 β (i Β· π΄))) β β) |
26 | 21, 25 | subcld 11519 |
. . . . . . . . 9
β’ (π΄ β β+
β ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄)))) β
β) |
27 | | imre 15000 |
. . . . . . . . 9
β’
(((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄)))) β
β β (ββ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) =
(ββ(-i Β· ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))))) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
β’ (π΄ β β+
β (ββ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) =
(ββ(-i Β· ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))))) |
29 | | atanval 26250 |
. . . . . . . . . . . . . 14
β’ (π΄ β dom arctan β
(arctanβπ΄) = ((i / 2)
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
30 | 17, 29 | syl 17 |
. . . . . . . . . . . . 13
β’ (π΄ β β+
β (arctanβπ΄) =
((i / 2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
31 | 30 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π΄ β β+
β (2 Β· (arctanβπ΄)) = (2 Β· ((i / 2) Β·
((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))))) |
32 | 10, 5, 6 | divcan2i 11905 |
. . . . . . . . . . . . . 14
β’ (2
Β· (i / 2)) = i |
33 | 32 | oveq1i 7372 |
. . . . . . . . . . . . 13
β’ ((2
Β· (i / 2)) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = (i Β·
((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) |
34 | | 2re 12234 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β+
β 2 β β) |
36 | 35 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ (π΄ β β+
β 2 β β) |
37 | | halfcl 12385 |
. . . . . . . . . . . . . . 15
β’ (i β
β β (i / 2) β β) |
38 | 10, 37 | mp1i 13 |
. . . . . . . . . . . . . 14
β’ (π΄ β β+
β (i / 2) β β) |
39 | 25, 21 | subcld 11519 |
. . . . . . . . . . . . . 14
β’ (π΄ β β+
β ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))) β
β) |
40 | 36, 38, 39 | mulassd 11185 |
. . . . . . . . . . . . 13
β’ (π΄ β β+
β ((2 Β· (i / 2)) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄))))) = (2
Β· ((i / 2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))))) |
41 | 33, 40 | eqtr3id 2791 |
. . . . . . . . . . . 12
β’ (π΄ β β+
β (i Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = (2 Β· ((i /
2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))))) |
42 | 31, 41 | eqtr4d 2780 |
. . . . . . . . . . 11
β’ (π΄ β β+
β (2 Β· (arctanβπ΄)) = (i Β· ((logβ(1 β (i
Β· π΄))) β
(logβ(1 + (i Β· π΄)))))) |
43 | 21, 25 | negsubdi2d 11535 |
. . . . . . . . . . . 12
β’ (π΄ β β+
β -((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄)))) =
((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) |
44 | 43 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π΄ β β+
β (i Β· -((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) = (i
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
45 | 42, 44 | eqtr4d 2780 |
. . . . . . . . . 10
β’ (π΄ β β+
β (2 Β· (arctanβπ΄)) = (i Β· -((logβ(1 + (i
Β· π΄))) β
(logβ(1 β (i Β· π΄)))))) |
46 | | mulneg12 11600 |
. . . . . . . . . . 11
β’ ((i
β β β§ ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄)))) β
β) β (-i Β· ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) = (i
Β· -((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄)))))) |
47 | 10, 26, 46 | sylancr 588 |
. . . . . . . . . 10
β’ (π΄ β β+
β (-i Β· ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) = (i
Β· -((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄)))))) |
48 | 45, 47 | eqtr4d 2780 |
. . . . . . . . 9
β’ (π΄ β β+
β (2 Β· (arctanβπ΄)) = (-i Β· ((logβ(1 + (i
Β· π΄))) β
(logβ(1 β (i Β· π΄)))))) |
49 | 48 | fveq2d 6851 |
. . . . . . . 8
β’ (π΄ β β+
β (ββ(2 Β· (arctanβπ΄))) = (ββ(-i Β·
((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))))) |
50 | | remulcl 11143 |
. . . . . . . . . 10
β’ ((2
β β β§ (arctanβπ΄) β β) β (2 Β·
(arctanβπ΄)) β
β) |
51 | 34, 3, 50 | sylancr 588 |
. . . . . . . . 9
β’ (π΄ β β+
β (2 Β· (arctanβπ΄)) β β) |
52 | 51 | rered 15116 |
. . . . . . . 8
β’ (π΄ β β+
β (ββ(2 Β· (arctanβπ΄))) = (2 Β· (arctanβπ΄))) |
53 | 28, 49, 52 | 3eqtr2rd 2784 |
. . . . . . 7
β’ (π΄ β β+
β (2 Β· (arctanβπ΄)) = (ββ((logβ(1 + (i
Β· π΄))) β
(logβ(1 β (i Β· π΄)))))) |
54 | | rpgt0 12934 |
. . . . . . . . 9
β’ (π΄ β β+
β 0 < π΄) |
55 | 1 | rered 15116 |
. . . . . . . . 9
β’ (π΄ β β+
β (ββπ΄) =
π΄) |
56 | 54, 55 | breqtrrd 5138 |
. . . . . . . 8
β’ (π΄ β β+
β 0 < (ββπ΄)) |
57 | | atanlogsublem 26281 |
. . . . . . . 8
β’ ((π΄ β dom arctan β§ 0 <
(ββπ΄)) β
(ββ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) β
(-Ο(,)Ο)) |
58 | 17, 56, 57 | syl2anc 585 |
. . . . . . 7
β’ (π΄ β β+
β (ββ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) β
(-Ο(,)Ο)) |
59 | 53, 58 | eqeltrd 2838 |
. . . . . 6
β’ (π΄ β β+
β (2 Β· (arctanβπ΄)) β (-Ο(,)Ο)) |
60 | | eliooord 13330 |
. . . . . 6
β’ ((2
Β· (arctanβπ΄))
β (-Ο(,)Ο) β (-Ο < (2 Β· (arctanβπ΄)) β§ (2 Β·
(arctanβπ΄)) <
Ο)) |
61 | 59, 60 | syl 17 |
. . . . 5
β’ (π΄ β β+
β (-Ο < (2 Β· (arctanβπ΄)) β§ (2 Β· (arctanβπ΄)) < Ο)) |
62 | 61 | simpld 496 |
. . . 4
β’ (π΄ β β+
β -Ο < (2 Β· (arctanβπ΄))) |
63 | | pire 25831 |
. . . . . . 7
β’ Ο
β β |
64 | 63 | renegcli 11469 |
. . . . . 6
β’ -Ο
β β |
65 | 64 | a1i 11 |
. . . . 5
β’ (π΄ β β+
β -Ο β β) |
66 | | 2pos 12263 |
. . . . . 6
β’ 0 <
2 |
67 | 66 | a1i 11 |
. . . . 5
β’ (π΄ β β+
β 0 < 2) |
68 | | ltdivmul 12037 |
. . . . 5
β’ ((-Ο
β β β§ (arctanβπ΄) β β β§ (2 β β
β§ 0 < 2)) β ((-Ο / 2) < (arctanβπ΄) β -Ο < (2 Β·
(arctanβπ΄)))) |
69 | 65, 3, 35, 67, 68 | syl112anc 1375 |
. . . 4
β’ (π΄ β β+
β ((-Ο / 2) < (arctanβπ΄) β -Ο < (2 Β·
(arctanβπ΄)))) |
70 | 62, 69 | mpbird 257 |
. . 3
β’ (π΄ β β+
β (-Ο / 2) < (arctanβπ΄)) |
71 | 8, 70 | eqbrtrid 5145 |
. 2
β’ (π΄ β β+
β -(Ο / 2) < (arctanβπ΄)) |
72 | 61 | simprd 497 |
. . 3
β’ (π΄ β β+
β (2 Β· (arctanβπ΄)) < Ο) |
73 | 63 | a1i 11 |
. . . 4
β’ (π΄ β β+
β Ο β β) |
74 | | ltmuldiv2 12036 |
. . . 4
β’
(((arctanβπ΄)
β β β§ Ο β β β§ (2 β β β§ 0 <
2)) β ((2 Β· (arctanβπ΄)) < Ο β (arctanβπ΄) < (Ο /
2))) |
75 | 3, 73, 35, 67, 74 | syl112anc 1375 |
. . 3
β’ (π΄ β β+
β ((2 Β· (arctanβπ΄)) < Ο β (arctanβπ΄) < (Ο /
2))) |
76 | 72, 75 | mpbid 231 |
. 2
β’ (π΄ β β+
β (arctanβπ΄)
< (Ο / 2)) |
77 | | halfpire 25837 |
. . . . 5
β’ (Ο /
2) β β |
78 | 77 | renegcli 11469 |
. . . 4
β’ -(Ο /
2) β β |
79 | 78 | rexri 11220 |
. . 3
β’ -(Ο /
2) β β* |
80 | 77 | rexri 11220 |
. . 3
β’ (Ο /
2) β β* |
81 | | elioo2 13312 |
. . 3
β’ ((-(Ο
/ 2) β β* β§ (Ο / 2) β β*)
β ((arctanβπ΄)
β (-(Ο / 2)(,)(Ο / 2)) β ((arctanβπ΄) β β β§ -(Ο / 2) <
(arctanβπ΄) β§
(arctanβπ΄) < (Ο
/ 2)))) |
82 | 79, 80, 81 | mp2an 691 |
. 2
β’
((arctanβπ΄)
β (-(Ο / 2)(,)(Ο / 2)) β ((arctanβπ΄) β β β§ -(Ο / 2) <
(arctanβπ΄) β§
(arctanβπ΄) < (Ο
/ 2))) |
83 | 3, 71, 76, 82 | syl3anbrc 1344 |
1
β’ (π΄ β β+
β (arctanβπ΄)
β (-(Ο / 2)(,)(Ο / 2))) |