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

Metamath Proof Explorer

Theorem atanlogsublem

Proof