Metamath Proof Explorer

Theorem atanbndlem

Description: Lemma for atanbnd . (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion atanbndlem 
|- ( A e. RR+ -> ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )

Proof

Step Hyp Ref Expression
1 rpre 
 |-  ( A e. RR+ -> A e. RR )
2 atanrecl 
 |-  ( A e. RR -> ( arctan ` A ) e. RR )
3 1 2 syl 
 |-  ( A e. RR+ -> ( arctan ` A ) e. RR )
4 picn 
 |-  _pi e. CC
5 2cn 
 |-  2 e. CC
6 2ne0 
 |-  2 =/= 0
7 divneg 
 |-  ( ( _pi e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( _pi / 2 ) = ( -u _pi / 2 ) )
8 4 5 6 7 mp3an 
 |-  -u ( _pi / 2 ) = ( -u _pi / 2 )
9 ax-1cn 
 |-  1 e. CC
10 ax-icn 
 |-  _i e. CC
11 1 recnd 
 |-  ( A e. RR+ -> A e. CC )
12 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
13 10 11 12 sylancr 
 |-  ( A e. RR+ -> ( _i x. A ) e. CC )
14 addcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC )
15 9 13 14 sylancr 
 |-  ( A e. RR+ -> ( 1 + ( _i x. A ) ) e. CC )
16 atanre 
 |-  ( A e. RR -> A e. dom arctan )
17 1 16 syl 
 |-  ( A e. RR+ -> A e. dom arctan )
18 atandm2 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
19 17 18 sylib 
 |-  ( A e. RR+ -> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
20 19 simp3d 
 |-  ( A e. RR+ -> ( 1 + ( _i x. A ) ) =/= 0 )
21 15 20 logcld 
 |-  ( A e. RR+ -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC )
22 subcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC )
23 9 13 22 sylancr 
 |-  ( A e. RR+ -> ( 1 - ( _i x. A ) ) e. CC )
24 19 simp2d 
 |-  ( A e. RR+ -> ( 1 - ( _i x. A ) ) =/= 0 )
25 23 24 logcld 
 |-  ( A e. RR+ -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC )
26 21 25 subcld 
 |-  ( A e. RR+ -> ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) e. CC )
27 imre 
 |-  ( ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) e. CC -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( Re ` ( -u _i x. ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) ) )
28 26 27 syl 
 |-  ( A e. RR+ -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( Re ` ( -u _i x. ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) ) )
29 atanval 
 |-  ( A e. dom arctan -> ( arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
30 17 29 syl 
 |-  ( A e. RR+ -> ( arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
31 30 oveq2d 
 |-  ( A e. RR+ -> ( 2 x. ( arctan ` A ) ) = ( 2 x. ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) )
32 10 5 6 divcan2i 
 |-  ( 2 x. ( _i / 2 ) ) = _i
33 32 oveq1i 
 |-  ( ( 2 x. ( _i / 2 ) ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( _i x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) )
34 2re 
 |-  2 e. RR
35 34 a1i 
 |-  ( A e. RR+ -> 2 e. RR )
36 35 recnd 
 |-  ( A e. RR+ -> 2 e. CC )
37 halfcl 
 |-  ( _i e. CC -> ( _i / 2 ) e. CC )
38 10 37 mp1i 
 |-  ( A e. RR+ -> ( _i / 2 ) e. CC )
39 25 21 subcld 
 |-  ( A e. RR+ -> ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC )
40 36 38 39 mulassd 
 |-  ( A e. RR+ -> ( ( 2 x. ( _i / 2 ) ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( 2 x. ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) )
41 33 40 eqtr3id 
 |-  ( A e. RR+ -> ( _i x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( 2 x. ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) )
42 31 41 eqtr4d 
 |-  ( A e. RR+ -> ( 2 x. ( arctan ` A ) ) = ( _i x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
43 21 25 negsubdi2d 
 |-  ( A e. RR+ -> -u ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) = ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) )
44 43 oveq2d 
 |-  ( A e. RR+ -> ( _i x. -u ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( _i x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
45 42 44 eqtr4d 
 |-  ( A e. RR+ -> ( 2 x. ( arctan ` A ) ) = ( _i x. -u ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
46 mulneg12 
 |-  ( ( _i e. CC /\ ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) e. CC ) -> ( -u _i x. ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( _i x. -u ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
47 10 26 46 sylancr 
 |-  ( A e. RR+ -> ( -u _i x. ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( _i x. -u ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
48 45 47 eqtr4d 
 |-  ( A e. RR+ -> ( 2 x. ( arctan ` A ) ) = ( -u _i x. ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
49 48 fveq2d 
 |-  ( A e. RR+ -> ( Re ` ( 2 x. ( arctan ` A ) ) ) = ( Re ` ( -u _i x. ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) ) )
50 remulcl 
 |-  ( ( 2 e. RR /\ ( arctan ` A ) e. RR ) -> ( 2 x. ( arctan ` A ) ) e. RR )
51 34 3 50 sylancr 
 |-  ( A e. RR+ -> ( 2 x. ( arctan ` A ) ) e. RR )
52 51 rered 
 |-  ( A e. RR+ -> ( Re ` ( 2 x. ( arctan ` A ) ) ) = ( 2 x. ( arctan ` A ) ) )
53 28 49 52 3eqtr2rd 
 |-  ( A e. RR+ -> ( 2 x. ( arctan ` A ) ) = ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
54 rpgt0 
 |-  ( A e. RR+ -> 0 < A )
55 1 rered 
 |-  ( A e. RR+ -> ( Re ` A ) = A )
56 54 55 breqtrrd 
 |-  ( A e. RR+ -> 0 < ( Re ` A ) )
57 atanlogsublem 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) _pi ) )
58 17 56 57 syl2anc 
 |-  ( A e. RR+ -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) _pi ) )
59 53 58 eqeltrd 
 |-  ( A e. RR+ -> ( 2 x. ( arctan ` A ) ) e. ( -u _pi (,) _pi ) )
60 eliooord 
 |-  ( ( 2 x. ( arctan ` A ) ) e. ( -u _pi (,) _pi ) -> ( -u _pi < ( 2 x. ( arctan ` A ) ) /\ ( 2 x. ( arctan ` A ) ) < _pi ) )
61 59 60 syl 
 |-  ( A e. RR+ -> ( -u _pi < ( 2 x. ( arctan ` A ) ) /\ ( 2 x. ( arctan ` A ) ) < _pi ) )
62 61 simpld 
 |-  ( A e. RR+ -> -u _pi < ( 2 x. ( arctan ` A ) ) )
63 pire 
 |-  _pi e. RR
64 63 renegcli 
 |-  -u _pi e. RR
65 64 a1i 
 |-  ( A e. RR+ -> -u _pi e. RR )
66 2pos 
 |-  0 < 2
67 66 a1i 
 |-  ( A e. RR+ -> 0 < 2 )
68 ltdivmul 
 |-  ( ( -u _pi e. RR /\ ( arctan ` A ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( -u _pi / 2 ) < ( arctan ` A ) <-> -u _pi < ( 2 x. ( arctan ` A ) ) ) )
69 65 3 35 67 68 syl112anc 
 |-  ( A e. RR+ -> ( ( -u _pi / 2 ) < ( arctan ` A ) <-> -u _pi < ( 2 x. ( arctan ` A ) ) ) )
70 62 69 mpbird 
 |-  ( A e. RR+ -> ( -u _pi / 2 ) < ( arctan ` A ) )
71 8 70 eqbrtrid 
 |-  ( A e. RR+ -> -u ( _pi / 2 ) < ( arctan ` A ) )
72 61 simprd 
 |-  ( A e. RR+ -> ( 2 x. ( arctan ` A ) ) < _pi )
73 63 a1i 
 |-  ( A e. RR+ -> _pi e. RR )
74 ltmuldiv2 
 |-  ( ( ( arctan ` A ) e. RR /\ _pi e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. ( arctan ` A ) ) < _pi <-> ( arctan ` A ) < ( _pi / 2 ) ) )
75 3 73 35 67 74 syl112anc 
 |-  ( A e. RR+ -> ( ( 2 x. ( arctan ` A ) ) < _pi <-> ( arctan ` A ) < ( _pi / 2 ) ) )
76 72 75 mpbid 
 |-  ( A e. RR+ -> ( arctan ` A ) < ( _pi / 2 ) )
77 halfpire 
 |-  ( _pi / 2 ) e. RR
78 77 renegcli 
 |-  -u ( _pi / 2 ) e. RR
79 78 rexri 
 |-  -u ( _pi / 2 ) e. RR*
80 77 rexri 
 |-  ( _pi / 2 ) e. RR*
81 elioo2 
 |-  ( ( -u ( _pi / 2 ) e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( ( arctan ` A ) e. RR /\ -u ( _pi / 2 ) < ( arctan ` A ) /\ ( arctan ` A ) < ( _pi / 2 ) ) ) )
82 79 80 81 mp2an 
 |-  ( ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( ( arctan ` A ) e. RR /\ -u ( _pi / 2 ) < ( arctan ` A ) /\ ( arctan ` A ) < ( _pi / 2 ) ) )
83 3 71 76 82 syl3anbrc 
 |-  ( A e. RR+ -> ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )