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 syl5eqr ⊢ ( 𝐴 ∈ ℝ+ → ( 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 ) ) )