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\leftrightarrow \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 \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 \log \left(1-\mathrm{i}A\right)\in ℂ$$
26	21 25	subcld	$$⊢A\in {ℝ}^{+}\to \log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\in ℂ$$
27		imre	$$⊢\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\in ℂ\to \Im \left(\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\right)=\Re \left(\left(-\mathrm{i}\right)\left(\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\right)\right)$$
28	26 27	syl	$$⊢A\in {ℝ}^{+}\to \Im \left(\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\right)=\Re \left(\left(-\mathrm{i}\right)\left(\log \left(1+\mathrm{i}A\right)-\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(\log \left(1-\mathrm{i}A\right)-\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(\log \left(1-\mathrm{i}A\right)-\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(\log \left(1-\mathrm{i}A\right)-\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(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=\mathrm{i}\left(\log \left(1-\mathrm{i}A\right)-\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 \log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\in ℂ$$
40	36 38 39	mulassd	$$⊢A\in {ℝ}^{+}\to 2\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=2\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
41	33 40	eqtr3id	$$⊢A\in {ℝ}^{+}\to \mathrm{i}\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=2\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
42	31 41	eqtr4d	$$⊢A\in {ℝ}^{+}\to 2arctan\left(A\right)=\mathrm{i}\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
43	21 25	negsubdi2d	$$⊢A\in {ℝ}^{+}\to -\left(\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\right)=\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)$$
44	43	oveq2d	$$⊢A\in {ℝ}^{+}\to \mathrm{i}\left(-\left(\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\right)\right)=\mathrm{i}\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
45	42 44	eqtr4d	$$⊢A\in {ℝ}^{+}\to 2arctan\left(A\right)=\mathrm{i}\left(-\left(\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\right)\right)$$
46		mulneg12	$$⊢\left(\mathrm{i}\in ℂ\wedge \log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\in ℂ\right)\to \left(-\mathrm{i}\right)\left(\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\right)=\mathrm{i}\left(-\left(\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\right)\right)$$
47	10 26 46	sylancr	$$⊢A\in {ℝ}^{+}\to \left(-\mathrm{i}\right)\left(\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\right)=\mathrm{i}\left(-\left(\log \left(1+\mathrm{i}A\right)-\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(\log \left(1+\mathrm{i}A\right)-\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(\log \left(1+\mathrm{i}A\right)-\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(\log \left(1+\mathrm{i}A\right)-\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(\log \left(1+\mathrm{i}A\right)-\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(\log \left(1+\mathrm{i}A\right)-\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}<arctan\left(A\right)\leftrightarrow -\mathrm{\pi }<2arctan\left(A\right)\right)$$
69	65 3 35 67 68	syl112anc	$$⊢A\in {ℝ}^{+}\to \left(\frac{-\mathrm{\pi }}{2}<arctan\left(A\right)\leftrightarrow -\mathrm{\pi }<2arctan\left(A\right)\right)$$
70	62 69	mpbird	$$⊢A\in {ℝ}^{+}\to \frac{-\mathrm{\pi }}{2}<arctan\left(A\right)$$
71	8 70	eqbrtrid	$$⊢A\in {ℝ}^{+}\to -\frac{\mathrm{\pi }}{2}<arctan\left(A\right)$$
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 }\leftrightarrow 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 }\leftrightarrow 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)\leftrightarrow \left(arctan\left(A\right)\in ℝ\wedge -\frac{\mathrm{\pi }}{2}<arctan\left(A\right)\wedge arctan\left(A\right)<\frac{\mathrm{\pi }}{2}\right)\right)$$
82	79 80 81	mp2an	$$⊢arctan\left(A\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\leftrightarrow \left(arctan\left(A\right)\in ℝ\wedge -\frac{\mathrm{\pi }}{2}<arctan\left(A\right)\wedge arctan\left(A\right)<\frac{\mathrm{\pi }}{2}\right)$$
83	3 71 76 82	syl3anbrc	$$⊢A\in {ℝ}^{+}\to arctan\left(A\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)$$