# Metamath Proof Explorer

## Theorem atanbndlem

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

Ref Expression
Assertion atanbndlem ${⊢}{A}\in {ℝ}^{+}\to arctan\left({A}\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)$

### Proof

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