atanlogsublem

		Ref	Expression
	Assertion	atanlogsublem	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A) - \log (1 - i A)) \in (- π, π)$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$⊢ 1 \in ℂ$
2		ax-icn	$⊢ i \in ℂ$
3		atandm2	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land 1 - i A \neq 0 \land 1 + i A \neq 0)$
4	3	birani	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to (A \in ℂ \land 1 - i A \neq 0 \land 1 + i A \neq 0)$
5	4	simp1d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to A \in ℂ$
6		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
7	2 5 6	sylancr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i A \in ℂ$
8		addcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 + i A \in ℂ$
9	1 7 8	sylancr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 1 + i A \in ℂ$
10	4	simp3d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 1 + i A \neq 0$
11	9 10	logcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log (1 + i A) \in ℂ$
12		subcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 - i A \in ℂ$
13	1 7 12	sylancr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 1 - i A \in ℂ$
14	4	simp2d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 1 - i A \neq 0$
15	13 14	logcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log (1 - i A) \in ℂ$
16	11 15	imsubd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A) - \log (1 - i A)) = ℑ (\log (1 + i A)) - ℑ (\log (1 - i A))$
17	2	a1i	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i \in ℂ$
18	17 5 17	subdid	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i (A - i) = i A - i i$
19		ixi	$⊢ i i = - 1$
20	19	oveq2i	$⊢ i A - i i = i A - -1$
21		subneg	$⊢ (i A \in ℂ \land 1 \in ℂ) \to i A - -1 = i A + 1$
22	7 1 21	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i A - -1 = i A + 1$
23	20 22	eqtrid	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i A - i i = i A + 1$
24		addcom	$⊢ (i A \in ℂ \land 1 \in ℂ) \to i A + 1 = 1 + i A$
25	7 1 24	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i A + 1 = 1 + i A$
26	18 23 25	3eqtrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i (A - i) = 1 + i A$
27	26	fveq2d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log i (A - i) = \log (1 + i A)$
28		subcl	$⊢ (A \in ℂ \land i \in ℂ) \to A - i \in ℂ$
29	5 2 28	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to A - i \in ℂ$
30		resub	$⊢ (A \in ℂ \land i \in ℂ) \to ℜ (A - i) = ℜ (A) - ℜ (i)$
31	5 2 30	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A - i) = ℜ (A) - ℜ (i)$
32		rei	$⊢ ℜ (i) = 0$
33	32	oveq2i	$⊢ ℜ (A) - ℜ (i) = ℜ (A) - 0$
34	5	recld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A) \in ℝ$
35	34	recnd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A) \in ℂ$
36	35	subid1d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A) - 0 = ℜ (A)$
37	33 36	eqtrid	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A) - ℜ (i) = ℜ (A)$
38	31 37	eqtrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A - i) = ℜ (A)$
39		gt0ne0	$⊢ (ℜ (A) \in ℝ \land 0 < ℜ (A)) \to ℜ (A) \neq 0$
40	34 39	sylancom	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A) \neq 0$
41	38 40	eqnetrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A - i) \neq 0$
42		fveq2	$⊢ A - i = 0 \to ℜ (A - i) = ℜ (0)$
43		re0	$⊢ ℜ (0) = 0$
44	42 43	eqtrdi	$⊢ A - i = 0 \to ℜ (A - i) = 0$
45	44	necon3i	$⊢ ℜ (A - i) \neq 0 \to A - i \neq 0$
46	41 45	syl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to A - i \neq 0$
47		simpr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 < ℜ (A)$
48		0re	$⊢ 0 \in ℝ$
49		ltle	$⊢ (0 \in ℝ \land ℜ (A) \in ℝ) \to (0 < ℜ (A) \to 0 \leq ℜ (A))$
50	48 34 49	sylancr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to (0 < ℜ (A) \to 0 \leq ℜ (A))$
51	47 50	mpd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 \leq ℜ (A)$
52	51 38	breqtrrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 \leq ℜ (A - i)$
53		logimul	$⊢ (A - i \in ℂ \land A - i \neq 0 \land 0 \leq ℜ (A - i)) \to \log i (A - i) = \log (A - i) + i (\frac{π}{2})$
54	29 46 52 53	syl3anc	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log i (A - i) = \log (A - i) + i (\frac{π}{2})$
55	27 54	eqtr3d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log (1 + i A) = \log (A - i) + i (\frac{π}{2})$
56	55	fveq2d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A)) = ℑ (\log (A - i) + i (\frac{π}{2}))$
57	29 46	logcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log (A - i) \in ℂ$
58		halfpire	$⊢ \frac{π}{2} \in ℝ$
59	58	recni	$⊢ \frac{π}{2} \in ℂ$
60	2 59	mulcli	$⊢ i (\frac{π}{2}) \in ℂ$
61		imadd	$⊢ (\log (A - i) \in ℂ \land i (\frac{π}{2}) \in ℂ) \to ℑ (\log (A - i) + i (\frac{π}{2})) = ℑ (\log (A - i)) + ℑ (i (\frac{π}{2}))$
62	57 60 61	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i) + i (\frac{π}{2})) = ℑ (\log (A - i)) + ℑ (i (\frac{π}{2}))$
63		reim	$⊢ \frac{π}{2} \in ℂ \to ℜ (\frac{π}{2}) = ℑ (i (\frac{π}{2}))$
64	59 63	ax-mp	$⊢ ℜ (\frac{π}{2}) = ℑ (i (\frac{π}{2}))$
65		rere	$⊢ \frac{π}{2} \in ℝ \to ℜ (\frac{π}{2}) = \frac{π}{2}$
66	58 65	ax-mp	$⊢ ℜ (\frac{π}{2}) = \frac{π}{2}$
67	64 66	eqtr3i	$⊢ ℑ (i (\frac{π}{2})) = \frac{π}{2}$
68	67	oveq2i	$⊢ ℑ (\log (A - i)) + ℑ (i (\frac{π}{2})) = ℑ (\log (A - i)) + (\frac{π}{2})$
69	62 68	eqtrdi	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i) + i (\frac{π}{2})) = ℑ (\log (A - i)) + (\frac{π}{2})$
70	56 69	eqtrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A)) = ℑ (\log (A - i)) + (\frac{π}{2})$
71		addcl	$⊢ (A \in ℂ \land i \in ℂ) \to A + i \in ℂ$
72	5 2 71	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to A + i \in ℂ$
73		mulcl	$⊢ (i \in ℂ \land A + i \in ℂ) \to i (A + i) \in ℂ$
74	2 72 73	sylancr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i (A + i) \in ℂ$
75		reim	$⊢ A + i \in ℂ \to ℜ (A + i) = ℑ (i (A + i))$
76	72 75	syl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A + i) = ℑ (i (A + i))$
77		readd	$⊢ (A \in ℂ \land i \in ℂ) \to ℜ (A + i) = ℜ (A) + ℜ (i)$
78	5 2 77	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A + i) = ℜ (A) + ℜ (i)$
79	32	oveq2i	$⊢ ℜ (A) + ℜ (i) = ℜ (A) + 0$
80	35	addridd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A) + 0 = ℜ (A)$
81	79 80	eqtrid	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A) + ℜ (i) = ℜ (A)$
82	78 81	eqtrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A + i) = ℜ (A)$
83	76 82	eqtr3d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (i (A + i)) = ℜ (A)$
84	47 83	breqtrrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 < ℑ (i (A + i))$
85		logneg2	$⊢ (i (A + i) \in ℂ \land 0 < ℑ (i (A + i))) \to \log (- i (A + i)) = \log i (A + i) - i π$
86	74 84 85	syl2anc	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log (- i (A + i)) = \log i (A + i) - i π$
87	17 5 17	adddid	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i (A + i) = i A + i i$
88	19	oveq2i	$⊢ i A + i i = i A + -1$
89		negsub	$⊢ (i A \in ℂ \land 1 \in ℂ) \to i A + -1 = i A - 1$
90	7 1 89	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i A + -1 = i A - 1$
91	88 90	eqtrid	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i A + i i = i A - 1$
92	87 91	eqtrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i (A + i) = i A - 1$
93	92	negeqd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - i (A + i) = - (i A - 1)$
94		negsubdi2	$⊢ (i A \in ℂ \land 1 \in ℂ) \to - (i A - 1) = 1 - i A$
95	7 1 94	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - (i A - 1) = 1 - i A$
96	93 95	eqtrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - i (A + i) = 1 - i A$
97	96	fveq2d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log (- i (A + i)) = \log (1 - i A)$
98	82 40	eqnetrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A + i) \neq 0$
99		fveq2	$⊢ A + i = 0 \to ℜ (A + i) = ℜ (0)$
100	99 43	eqtrdi	$⊢ A + i = 0 \to ℜ (A + i) = 0$
101	100	necon3i	$⊢ ℜ (A + i) \neq 0 \to A + i \neq 0$
102	98 101	syl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to A + i \neq 0$
103	72 102	logcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log (A + i) \in ℂ$
104	60	a1i	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i (\frac{π}{2}) \in ℂ$
105		picn	$⊢ π \in ℂ$
106	2 105	mulcli	$⊢ i π \in ℂ$
107	106	a1i	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i π \in ℂ$
108	51 82	breqtrrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 \leq ℜ (A + i)$
109		logimul	$⊢ (A + i \in ℂ \land A + i \neq 0 \land 0 \leq ℜ (A + i)) \to \log i (A + i) = \log (A + i) + i (\frac{π}{2})$
110	72 102 108 109	syl3anc	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log i (A + i) = \log (A + i) + i (\frac{π}{2})$
111	110	oveq1d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log i (A + i) - i π = \log (A + i) + i (\frac{π}{2}) - i π$
112	103 104 107 111	assraddsubd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log i (A + i) - i π = \log (A + i) + i (\frac{π}{2}) - i π$
113	86 97 112	3eqtr3d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log (1 - i A) = \log (A + i) + i (\frac{π}{2}) - i π$
114	113	fveq2d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 - i A)) = ℑ (\log (A + i) + i (\frac{π}{2}) - i π)$
115	60 106	subcli	$⊢ i (\frac{π}{2}) - i π \in ℂ$
116		imadd	$⊢ (\log (A + i) \in ℂ \land i (\frac{π}{2}) - i π \in ℂ) \to ℑ (\log (A + i) + i (\frac{π}{2}) - i π) = ℑ (\log (A + i)) + ℑ (i (\frac{π}{2}) - i π)$
117	103 115 116	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A + i) + i (\frac{π}{2}) - i π) = ℑ (\log (A + i)) + ℑ (i (\frac{π}{2}) - i π)$
118		imsub	$⊢ (i (\frac{π}{2}) \in ℂ \land i π \in ℂ) \to ℑ (i (\frac{π}{2}) - i π) = ℑ (i (\frac{π}{2})) - ℑ (i π)$
119	60 106 118	mp2an	$⊢ ℑ (i (\frac{π}{2}) - i π) = ℑ (i (\frac{π}{2})) - ℑ (i π)$
120		reim	$⊢ π \in ℂ \to ℜ (π) = ℑ (i π)$
121	105 120	ax-mp	$⊢ ℜ (π) = ℑ (i π)$
122		pire	$⊢ π \in ℝ$
123		rere	$⊢ π \in ℝ \to ℜ (π) = π$
124	122 123	ax-mp	$⊢ ℜ (π) = π$
125	121 124	eqtr3i	$⊢ ℑ (i π) = π$
126	67 125	oveq12i	$⊢ ℑ (i (\frac{π}{2})) - ℑ (i π) = (\frac{π}{2}) - π$
127	59	negcli	$⊢ - \frac{π}{2} \in ℂ$
128	105 59	negsubi	$⊢ π + (- \frac{π}{2}) = π - (\frac{π}{2})$
129		pidiv2halves	$⊢ (\frac{π}{2}) + (\frac{π}{2}) = π$
130	105 59 59 129	subaddrii	$⊢ π - (\frac{π}{2}) = \frac{π}{2}$
131	128 130	eqtri	$⊢ π + (- \frac{π}{2}) = \frac{π}{2}$
132	59 105 127 131	subaddrii	$⊢ (\frac{π}{2}) - π = - \frac{π}{2}$
133	119 126 132	3eqtri	$⊢ ℑ (i (\frac{π}{2}) - i π) = - \frac{π}{2}$
134	133	oveq2i	$⊢ ℑ (\log (A + i)) + ℑ (i (\frac{π}{2}) - i π) = ℑ (\log (A + i)) + (- \frac{π}{2})$
135	117 134	eqtrdi	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A + i) + i (\frac{π}{2}) - i π) = ℑ (\log (A + i)) + (- \frac{π}{2})$
136	114 135	eqtrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 - i A)) = ℑ (\log (A + i)) + (- \frac{π}{2})$
137	70 136	oveq12d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A)) - ℑ (\log (1 - i A)) = ℑ (\log (A - i)) + (\frac{π}{2}) - (ℑ (\log (A + i)) + (- \frac{π}{2}))$
138	57	imcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) \in ℝ$
139	138	recnd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) \in ℂ$
140	59	a1i	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \frac{π}{2} \in ℂ$
141	103	imcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A + i)) \in ℝ$
142	141	recnd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A + i)) \in ℂ$
143	127	a1i	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - \frac{π}{2} \in ℂ$
144	139 140 142 143	addsub4d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) + (\frac{π}{2}) - (ℑ (\log (A + i)) + (- \frac{π}{2})) = (ℑ (\log (A - i)) - ℑ (\log (A + i))) + (\frac{π}{2}) - (- \frac{π}{2})$
145	59 59	subnegi	$⊢ (\frac{π}{2}) - (- \frac{π}{2}) = (\frac{π}{2}) + (\frac{π}{2})$
146	145 129	eqtri	$⊢ (\frac{π}{2}) - (- \frac{π}{2}) = π$
147	146	oveq2i	$⊢ (ℑ (\log (A - i)) - ℑ (\log (A + i))) + (\frac{π}{2}) - (- \frac{π}{2}) = ℑ (\log (A - i)) - ℑ (\log (A + i)) + π$
148	144 147	eqtrdi	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) + (\frac{π}{2}) - (ℑ (\log (A + i)) + (- \frac{π}{2})) = ℑ (\log (A - i)) - ℑ (\log (A + i)) + π$
149	16 137 148	3eqtrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A) - \log (1 - i A)) = ℑ (\log (A - i)) - ℑ (\log (A + i)) + π$
150	138 141	resubcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) - ℑ (\log (A + i)) \in ℝ$
151		readdcl	$⊢ (ℑ (\log (A - i)) - ℑ (\log (A + i)) \in ℝ \land π \in ℝ) \to ℑ (\log (A - i)) - ℑ (\log (A + i)) + π \in ℝ$
152	150 122 151	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) - ℑ (\log (A + i)) + π \in ℝ$
153	122	renegcli	$⊢ - π \in ℝ$
154	153	recni	$⊢ - π \in ℂ$
155	154 105	negsubi	$⊢ - π + (- π) = - π - π$
156	153	a1i	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - π \in ℝ$
157	141	renegcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - ℑ (\log (A + i)) \in ℝ$
158	29 46	logimcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to (- π < ℑ (\log (A - i)) \land ℑ (\log (A - i)) \leq π)$
159	158	simpld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - π < ℑ (\log (A - i))$
160	72 102	logimcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to (- π < ℑ (\log (A + i)) \land ℑ (\log (A + i)) \leq π)$
161	160	simprd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A + i)) \leq π$
162		leneg	$⊢ (ℑ (\log (A + i)) \in ℝ \land π \in ℝ) \to (ℑ (\log (A + i)) \leq π \leftrightarrow - π \leq - ℑ (\log (A + i)))$
163	141 122 162	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to (ℑ (\log (A + i)) \leq π \leftrightarrow - π \leq - ℑ (\log (A + i)))$
164	161 163	mpbid	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - π \leq - ℑ (\log (A + i))$
165	156 156 138 157 159 164	ltleaddd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - π + (- π) < ℑ (\log (A - i)) + (- ℑ (\log (A + i)))$
166	139 142	negsubd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) + (- ℑ (\log (A + i))) = ℑ (\log (A - i)) - ℑ (\log (A + i))$
167	165 166	breqtrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - π + (- π) < ℑ (\log (A - i)) - ℑ (\log (A + i))$
168	155 167	eqbrtrrid	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - π - π < ℑ (\log (A - i)) - ℑ (\log (A + i))$
169	122	a1i	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to π \in ℝ$
170	156 169 150	ltsubaddd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to (- π - π < ℑ (\log (A - i)) - ℑ (\log (A + i)) \leftrightarrow - π < ℑ (\log (A - i)) - ℑ (\log (A + i)) + π)$
171	168 170	mpbid	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - π < ℑ (\log (A - i)) - ℑ (\log (A + i)) + π$
172		0red	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 \in ℝ$
173	5	imcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (A) \in ℝ$
174		peano2rem	$⊢ ℑ (A) \in ℝ \to ℑ (A) - 1 \in ℝ$
175	173 174	syl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (A) - 1 \in ℝ$
176		peano2re	$⊢ ℑ (A) \in ℝ \to ℑ (A) + 1 \in ℝ$
177	173 176	syl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (A) + 1 \in ℝ$
178	173	ltm1d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (A) - 1 < ℑ (A)$
179	173	ltp1d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (A) < ℑ (A) + 1$
180	175 173 177 178 179	lttrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (A) - 1 < ℑ (A) + 1$
181		ltdiv1	$⊢ (ℑ (A) - 1 \in ℝ \land ℑ (A) + 1 \in ℝ \land (ℜ (A) \in ℝ \land 0 < ℜ (A))) \to (ℑ (A) - 1 < ℑ (A) + 1 \leftrightarrow \frac{ℑ (A) - 1}{ℜ (A)} < \frac{ℑ (A) + 1}{ℜ (A)})$
182	175 177 34 47 181	syl112anc	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to (ℑ (A) - 1 < ℑ (A) + 1 \leftrightarrow \frac{ℑ (A) - 1}{ℜ (A)} < \frac{ℑ (A) + 1}{ℜ (A)})$
183	180 182	mpbid	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \frac{ℑ (A) - 1}{ℜ (A)} < \frac{ℑ (A) + 1}{ℜ (A)}$
184		imsub	$⊢ (A \in ℂ \land i \in ℂ) \to ℑ (A - i) = ℑ (A) - ℑ (i)$
185	5 2 184	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (A - i) = ℑ (A) - ℑ (i)$
186		imi	$⊢ ℑ (i) = 1$
187	186	oveq2i	$⊢ ℑ (A) - ℑ (i) = ℑ (A) - 1$
188	185 187	eqtrdi	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (A - i) = ℑ (A) - 1$
189	188 38	oveq12d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \frac{ℑ (A - i)}{ℜ (A - i)} = \frac{ℑ (A) - 1}{ℜ (A)}$
190		imadd	$⊢ (A \in ℂ \land i \in ℂ) \to ℑ (A + i) = ℑ (A) + ℑ (i)$
191	5 2 190	sylancl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (A + i) = ℑ (A) + ℑ (i)$
192	186	oveq2i	$⊢ ℑ (A) + ℑ (i) = ℑ (A) + 1$
193	191 192	eqtrdi	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (A + i) = ℑ (A) + 1$
194	193 82	oveq12d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \frac{ℑ (A + i)}{ℜ (A + i)} = \frac{ℑ (A) + 1}{ℜ (A)}$
195	183 189 194	3brtr4d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \frac{ℑ (A - i)}{ℜ (A - i)} < \frac{ℑ (A + i)}{ℜ (A + i)}$
196		tanarg	$⊢ (A - i \in ℂ \land ℜ (A - i) \neq 0) \to \tan ℑ (\log (A - i)) = \frac{ℑ (A - i)}{ℜ (A - i)}$
197	29 41 196	syl2anc	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \tan ℑ (\log (A - i)) = \frac{ℑ (A - i)}{ℜ (A - i)}$
198		tanarg	$⊢ (A + i \in ℂ \land ℜ (A + i) \neq 0) \to \tan ℑ (\log (A + i)) = \frac{ℑ (A + i)}{ℜ (A + i)}$
199	72 98 198	syl2anc	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \tan ℑ (\log (A + i)) = \frac{ℑ (A + i)}{ℜ (A + i)}$
200	195 197 199	3brtr4d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \tan ℑ (\log (A - i)) < \tan ℑ (\log (A + i))$
201	47 38	breqtrrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 < ℜ (A - i)$
202		argregt0	$⊢ (A - i \in ℂ \land 0 < ℜ (A - i)) \to ℑ (\log (A - i)) \in (- \frac{π}{2}, \frac{π}{2})$
203	29 201 202	syl2anc	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) \in (- \frac{π}{2}, \frac{π}{2})$
204	47 82	breqtrrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 < ℜ (A + i)$
205		argregt0	$⊢ (A + i \in ℂ \land 0 < ℜ (A + i)) \to ℑ (\log (A + i)) \in (- \frac{π}{2}, \frac{π}{2})$
206	72 204 205	syl2anc	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A + i)) \in (- \frac{π}{2}, \frac{π}{2})$
207		tanord	$⊢ (ℑ (\log (A - i)) \in (- \frac{π}{2}, \frac{π}{2}) \land ℑ (\log (A + i)) \in (- \frac{π}{2}, \frac{π}{2})) \to (ℑ (\log (A - i)) < ℑ (\log (A + i)) \leftrightarrow \tan ℑ (\log (A - i)) < \tan ℑ (\log (A + i)))$
208	203 206 207	syl2anc	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to (ℑ (\log (A - i)) < ℑ (\log (A + i)) \leftrightarrow \tan ℑ (\log (A - i)) < \tan ℑ (\log (A + i)))$
209	200 208	mpbird	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) < ℑ (\log (A + i))$
210	142	addlidd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 + ℑ (\log (A + i)) = ℑ (\log (A + i))$
211	209 210	breqtrrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) < 0 + ℑ (\log (A + i))$
212	138 141 172	ltsubaddd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to (ℑ (\log (A - i)) - ℑ (\log (A + i)) < 0 \leftrightarrow ℑ (\log (A - i)) < 0 + ℑ (\log (A + i)))$
213	211 212	mpbird	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) - ℑ (\log (A + i)) < 0$
214	150 172 169 213	ltadd1dd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) - ℑ (\log (A + i)) + π < 0 + π$
215	105	addlidi	$⊢ 0 + π = π$
216	214 215	breqtrdi	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) - ℑ (\log (A + i)) + π < π$
217	153	rexri	$⊢ - π \in ℝ^{*}$
218	122	rexri	$⊢ π \in ℝ^{*}$
219		elioo2	$⊢ (- π \in ℝ^{} \land π \in ℝ^{}) \to (ℑ (\log (A - i)) - ℑ (\log (A + i)) + π \in (- π, π) \leftrightarrow (ℑ (\log (A - i)) - ℑ (\log (A + i)) + π \in ℝ \land - π < ℑ (\log (A - i)) - ℑ (\log (A + i)) + π \land ℑ (\log (A - i)) - ℑ (\log (A + i)) + π < π))$
220	217 218 219	mp2an	$⊢ ℑ (\log (A - i)) - ℑ (\log (A + i)) + π \in (- π, π) \leftrightarrow (ℑ (\log (A - i)) - ℑ (\log (A + i)) + π \in ℝ \land - π < ℑ (\log (A - i)) - ℑ (\log (A + i)) + π \land ℑ (\log (A - i)) - ℑ (\log (A + i)) + π < π)$
221	152 171 216 220	syl3anbrc	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (A - i)) - ℑ (\log (A + i)) + π \in (- π, π)$
222	149 221	eqeltrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A) - \log (1 - i A)) \in (- π, π)$

Metamath Proof Explorer

Theorem atanlogsublem

Proof