Metamath Proof Explorer


Theorem atanbndlem

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

Ref Expression
Assertion atanbndlem ( 𝐴 ∈ ℝ+ → ( arctan ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )

Proof

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