atanlogaddlem

		Ref	Expression
	Assertion	atanlogaddlem	$⊢ (A \in dom arctan \land 0 \leq ℜ (A)) \to \log (1 + i A) + \log (1 - i A) \in ran log$

Proof

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		atandm2	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land 1 - i A \neq 0 \land 1 + i A \neq 0)$
3	2	simp1bi	$⊢ A \in dom arctan \to A \in ℂ$
4	3	recld	$⊢ A \in dom arctan \to ℜ (A) \in ℝ$
5		leloe	$⊢ (0 \in ℝ \land ℜ (A) \in ℝ) \to (0 \leq ℜ (A) \leftrightarrow (0 < ℜ (A) \lor 0 = ℜ (A)))$
6	1 4 5	sylancr	$⊢ A \in dom arctan \to (0 \leq ℜ (A) \leftrightarrow (0 < ℜ (A) \lor 0 = ℜ (A)))$
7	6	biimpa	$⊢ (A \in dom arctan \land 0 \leq ℜ (A)) \to (0 < ℜ (A) \lor 0 = ℜ (A))$
8		ax-1cn	$⊢ 1 \in ℂ$
9		ax-icn	$⊢ i \in ℂ$
10		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
11	9 3 10	sylancr	$⊢ A \in dom arctan \to i A \in ℂ$
12		addcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 + i A \in ℂ$
13	8 11 12	sylancr	$⊢ A \in dom arctan \to 1 + i A \in ℂ$
14	2	simp3bi	$⊢ A \in dom arctan \to 1 + i A \neq 0$
15	13 14	logcld	$⊢ A \in dom arctan \to \log (1 + i A) \in ℂ$
16		subcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 - i A \in ℂ$
17	8 11 16	sylancr	$⊢ A \in dom arctan \to 1 - i A \in ℂ$
18	2	simp2bi	$⊢ A \in dom arctan \to 1 - i A \neq 0$
19	17 18	logcld	$⊢ A \in dom arctan \to \log (1 - i A) \in ℂ$
20	15 19	addcld	$⊢ A \in dom arctan \to \log (1 + i A) + \log (1 - i A) \in ℂ$
21	20	adantr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log (1 + i A) + \log (1 - i A) \in ℂ$
22		pire	$⊢ π \in ℝ$
23	22	renegcli	$⊢ - π \in ℝ$
24	23	a1i	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - π \in ℝ$
25	19	adantr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log (1 - i A) \in ℂ$
26	25	imcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 - i A)) \in ℝ$
27	15	adantr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log (1 + i A) \in ℂ$
28	27	imcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A)) \in ℝ$
29	28 26	readdcld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A)) + ℑ (\log (1 - i A)) \in ℝ$
30	17	adantr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 1 - i A \in ℂ$
31		im1	$⊢ ℑ (1) = 0$
32	31	oveq1i	$⊢ ℑ (1) - ℑ (i A) = 0 - ℑ (i A)$
33		df-neg	$⊢ - ℑ (i A) = 0 - ℑ (i A)$
34	32 33	eqtr4i	$⊢ ℑ (1) - ℑ (i A) = - ℑ (i A)$
35	11	adantr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to i A \in ℂ$
36		imsub	$⊢ (1 \in ℂ \land i A \in ℂ) \to ℑ (1 - i A) = ℑ (1) - ℑ (i A)$
37	8 35 36	sylancr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (1 - i A) = ℑ (1) - ℑ (i A)$
38	3	adantr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to A \in ℂ$
39		reim	$⊢ A \in ℂ \to ℜ (A) = ℑ (i A)$
40	38 39	syl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A) = ℑ (i A)$
41	40	negeqd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - ℜ (A) = - ℑ (i A)$
42	34 37 41	3eqtr4a	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (1 - i A) = - ℜ (A)$
43	4	lt0neg2d	$⊢ A \in dom arctan \to (0 < ℜ (A) \leftrightarrow - ℜ (A) < 0)$
44	43	biimpa	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - ℜ (A) < 0$
45	42 44	eqbrtrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (1 - i A) < 0$
46		argimlt0	$⊢ (1 - i A \in ℂ \land ℑ (1 - i A) < 0) \to ℑ (\log (1 - i A)) \in (- π, 0)$
47	30 45 46	syl2anc	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 - i A)) \in (- π, 0)$
48		eliooord	$⊢ ℑ (\log (1 - i A)) \in (- π, 0) \to (- π < ℑ (\log (1 - i A)) \land ℑ (\log (1 - i A)) < 0)$
49	47 48	syl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to (- π < ℑ (\log (1 - i A)) \land ℑ (\log (1 - i A)) < 0)$
50	49	simpld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - π < ℑ (\log (1 - i A))$
51	13	adantr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 1 + i A \in ℂ$
52		simpr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 < ℜ (A)$
53		imadd	$⊢ (1 \in ℂ \land i A \in ℂ) \to ℑ (1 + i A) = ℑ (1) + ℑ (i A)$
54	8 35 53	sylancr	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (1 + i A) = ℑ (1) + ℑ (i A)$
55	40	oveq2d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (1) + ℜ (A) = ℑ (1) + ℑ (i A)$
56	31	oveq1i	$⊢ ℑ (1) + ℜ (A) = 0 + ℜ (A)$
57	38	recld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A) \in ℝ$
58	57	recnd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℜ (A) \in ℂ$
59	58	addid2d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 + ℜ (A) = ℜ (A)$
60	56 59	eqtrid	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (1) + ℜ (A) = ℜ (A)$
61	54 55 60	3eqtr2d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (1 + i A) = ℜ (A)$
62	52 61	breqtrrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 < ℑ (1 + i A)$
63		argimgt0	$⊢ (1 + i A \in ℂ \land 0 < ℑ (1 + i A)) \to ℑ (\log (1 + i A)) \in (0, π)$
64	51 62 63	syl2anc	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A)) \in (0, π)$
65		eliooord	$⊢ ℑ (\log (1 + i A)) \in (0, π) \to (0 < ℑ (\log (1 + i A)) \land ℑ (\log (1 + i A)) < π)$
66	64 65	syl	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to (0 < ℑ (\log (1 + i A)) \land ℑ (\log (1 + i A)) < π)$
67	66	simpld	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 < ℑ (\log (1 + i A))$
68	28 26	ltaddpos2d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to (0 < ℑ (\log (1 + i A)) \leftrightarrow ℑ (\log (1 - i A)) < ℑ (\log (1 + i A)) + ℑ (\log (1 - i A)))$
69	67 68	mpbid	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 - i A)) < ℑ (\log (1 + i A)) + ℑ (\log (1 - i A))$
70	24 26 29 50 69	lttrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - π < ℑ (\log (1 + i A)) + ℑ (\log (1 - i A))$
71	27 25	imaddd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A) + \log (1 - i A)) = ℑ (\log (1 + i A)) + ℑ (\log (1 - i A))$
72	70 71	breqtrrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to - π < ℑ (\log (1 + i A) + \log (1 - i A))$
73	22	a1i	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to π \in ℝ$
74		0red	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to 0 \in ℝ$
75	49	simprd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 - i A)) < 0$
76	26 74 28 75	ltadd2dd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A)) + ℑ (\log (1 - i A)) < ℑ (\log (1 + i A)) + 0$
77	28	recnd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A)) \in ℂ$
78	77	addid1d	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A)) + 0 = ℑ (\log (1 + i A))$
79	76 78	breqtrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A)) + ℑ (\log (1 - i A)) < ℑ (\log (1 + i A))$
80	66	simprd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A)) < π$
81	29 28 73 79 80	lttrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A)) + ℑ (\log (1 - i A)) < π$
82	29 73 81	ltled	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A)) + ℑ (\log (1 - i A)) \leq π$
83	71 82	eqbrtrd	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A) + \log (1 - i A)) \leq π$
84		ellogrn	$⊢ \log (1 + i A) + \log (1 - i A) \in ran log \leftrightarrow (\log (1 + i A) + \log (1 - i A) \in ℂ \land - π < ℑ (\log (1 + i A) + \log (1 - i A)) \land ℑ (\log (1 + i A) + \log (1 - i A)) \leq π)$
85	21 72 83 84	syl3anbrc	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to \log (1 + i A) + \log (1 - i A) \in ran log$
86		0red	$⊢ (A \in dom arctan \land 0 = ℜ (A)) \to 0 \in ℝ$
87	11	adantr	$⊢ (A \in dom arctan \land 0 = ℜ (A)) \to i A \in ℂ$
88		simpr	$⊢ (A \in dom arctan \land 0 = ℜ (A)) \to 0 = ℜ (A)$
89	3	adantr	$⊢ (A \in dom arctan \land 0 = ℜ (A)) \to A \in ℂ$
90	89 39	syl	$⊢ (A \in dom arctan \land 0 = ℜ (A)) \to ℜ (A) = ℑ (i A)$
91	88 90	eqtr2d	$⊢ (A \in dom arctan \land 0 = ℜ (A)) \to ℑ (i A) = 0$
92	87 91	reim0bd	$⊢ (A \in dom arctan \land 0 = ℜ (A)) \to i A \in ℝ$
93	15 19	addcomd	$⊢ A \in dom arctan \to \log (1 + i A) + \log (1 - i A) = \log (1 - i A) + \log (1 + i A)$
94	93	ad2antrr	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land 0 \leq i A) \to \log (1 + i A) + \log (1 - i A) = \log (1 - i A) + \log (1 + i A)$
95		logrncl	$⊢ (1 - i A \in ℂ \land 1 - i A \neq 0) \to \log (1 - i A) \in ran log$
96	17 18 95	syl2anc	$⊢ A \in dom arctan \to \log (1 - i A) \in ran log$
97	96	ad2antrr	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land 0 \leq i A) \to \log (1 - i A) \in ran log$
98		1re	$⊢ 1 \in ℝ$
99	92	adantr	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land 0 \leq i A) \to i A \in ℝ$
100		readdcl	$⊢ (1 \in ℝ \land i A \in ℝ) \to 1 + i A \in ℝ$
101	98 99 100	sylancr	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land 0 \leq i A) \to 1 + i A \in ℝ$
102		0red	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land 0 \leq i A) \to 0 \in ℝ$
103		1red	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land 0 \leq i A) \to 1 \in ℝ$
104		0lt1	$⊢ 0 < 1$
105	104	a1i	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land 0 \leq i A) \to 0 < 1$
106		addge01	$⊢ (1 \in ℝ \land i A \in ℝ) \to (0 \leq i A \leftrightarrow 1 \leq 1 + i A)$
107	98 92 106	sylancr	$⊢ (A \in dom arctan \land 0 = ℜ (A)) \to (0 \leq i A \leftrightarrow 1 \leq 1 + i A)$
108	107	biimpa	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land 0 \leq i A) \to 1 \leq 1 + i A$
109	102 103 101 105 108	ltletrd	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land 0 \leq i A) \to 0 < 1 + i A$
110	101 109	elrpd	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land 0 \leq i A) \to 1 + i A \in ℝ^{+}$
111	110	relogcld	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land 0 \leq i A) \to \log (1 + i A) \in ℝ$
112		logrnaddcl	$⊢ (\log (1 - i A) \in ran log \land \log (1 + i A) \in ℝ) \to \log (1 - i A) + \log (1 + i A) \in ran log$
113	97 111 112	syl2anc	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land 0 \leq i A) \to \log (1 - i A) + \log (1 + i A) \in ran log$
114	94 113	eqeltrd	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land 0 \leq i A) \to \log (1 + i A) + \log (1 - i A) \in ran log$
115		logrncl	$⊢ (1 + i A \in ℂ \land 1 + i A \neq 0) \to \log (1 + i A) \in ran log$
116	13 14 115	syl2anc	$⊢ A \in dom arctan \to \log (1 + i A) \in ran log$
117	116	ad2antrr	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land i A \leq 0) \to \log (1 + i A) \in ran log$
118	92	adantr	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land i A \leq 0) \to i A \in ℝ$
119		resubcl	$⊢ (1 \in ℝ \land i A \in ℝ) \to 1 - i A \in ℝ$
120	98 118 119	sylancr	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land i A \leq 0) \to 1 - i A \in ℝ$
121		0red	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land i A \leq 0) \to 0 \in ℝ$
122		1red	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land i A \leq 0) \to 1 \in ℝ$
123	104	a1i	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land i A \leq 0) \to 0 < 1$
124		1m0e1	$⊢ 1 - 0 = 1$
125		1red	$⊢ (A \in dom arctan \land 0 = ℜ (A)) \to 1 \in ℝ$
126	92 86 125	lesub2d	$⊢ (A \in dom arctan \land 0 = ℜ (A)) \to (i A \leq 0 \leftrightarrow 1 - 0 \leq 1 - i A)$
127	126	biimpa	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land i A \leq 0) \to 1 - 0 \leq 1 - i A$
128	124 127	eqbrtrrid	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land i A \leq 0) \to 1 \leq 1 - i A$
129	121 122 120 123 128	ltletrd	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land i A \leq 0) \to 0 < 1 - i A$
130	120 129	elrpd	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land i A \leq 0) \to 1 - i A \in ℝ^{+}$
131	130	relogcld	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land i A \leq 0) \to \log (1 - i A) \in ℝ$
132		logrnaddcl	$⊢ (\log (1 + i A) \in ran log \land \log (1 - i A) \in ℝ) \to \log (1 + i A) + \log (1 - i A) \in ran log$
133	117 131 132	syl2anc	$⊢ ((A \in dom arctan \land 0 = ℜ (A)) \land i A \leq 0) \to \log (1 + i A) + \log (1 - i A) \in ran log$
134	86 92 114 133	lecasei	$⊢ (A \in dom arctan \land 0 = ℜ (A)) \to \log (1 + i A) + \log (1 - i A) \in ran log$
135	85 134	jaodan	$⊢ (A \in dom arctan \land (0 < ℜ (A) \lor 0 = ℜ (A))) \to \log (1 + i A) + \log (1 - i A) \in ran log$
136	7 135	syldan	$⊢ (A \in dom arctan \land 0 \leq ℜ (A)) \to \log (1 + i A) + \log (1 - i A) \in ran log$

Metamath Proof Explorer

Theorem atanlogaddlem

Proof