atanlogsublem

		Ref	Expression
	Assertion	atanlogsublem	\|- ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) _pi ) )

Proof

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

Metamath Proof Explorer

Theorem atanlogsublem

Proof