atanlogadd

Description: The rule sqrt ( z w ) = ( sqrt z ) ( sqrt w ) is not always true on the complex numbers, but it is true when the arguments of z and w sum to within the interval ( -upi , pi ] , so there are some cases such as this one with z = 1 +i A and w = 1 - i A which are true unconditionally. This result can also be stated as " sqrt ( 1 + z ) + sqrt ( 1 - z ) is analytic". (Contributed by Mario Carneiro, 3-Apr-2015)

		Ref	Expression
	Assertion	atanlogadd	$⊢ A \in dom arctan \to \log (1 + i A) + \log (1 - i A) \in ran log$

Proof

Step	Hyp	Ref	Expression
1		0red	$⊢ A \in dom arctan \to 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		atanlogaddlem	$⊢ (A \in dom arctan \land 0 \leq ℜ (A)) \to \log (1 + i A) + \log (1 - i A) \in ran log$
6		ax-1cn	$⊢ 1 \in ℂ$
7		ax-icn	$⊢ i \in ℂ$
8		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
9	7 3 8	sylancr	$⊢ A \in dom arctan \to i A \in ℂ$
10		addcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 + i A \in ℂ$
11	6 9 10	sylancr	$⊢ A \in dom arctan \to 1 + i A \in ℂ$
12	2	simp3bi	$⊢ A \in dom arctan \to 1 + i A \neq 0$
13	11 12	logcld	$⊢ A \in dom arctan \to \log (1 + i A) \in ℂ$
14		subcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 - i A \in ℂ$
15	6 9 14	sylancr	$⊢ A \in dom arctan \to 1 - i A \in ℂ$
16	2	simp2bi	$⊢ A \in dom arctan \to 1 - i A \neq 0$
17	15 16	logcld	$⊢ A \in dom arctan \to \log (1 - i A) \in ℂ$
18	13 17	addcomd	$⊢ A \in dom arctan \to \log (1 + i A) + \log (1 - i A) = \log (1 - i A) + \log (1 + i A)$
19		mulneg2	$⊢ (i \in ℂ \land A \in ℂ) \to i (- A) = - i A$
20	7 3 19	sylancr	$⊢ A \in dom arctan \to i (- A) = - i A$
21	20	oveq2d	$⊢ A \in dom arctan \to 1 + i (- A) = 1 + (- i A)$
22		negsub	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 + (- i A) = 1 - i A$
23	6 9 22	sylancr	$⊢ A \in dom arctan \to 1 + (- i A) = 1 - i A$
24	21 23	eqtrd	$⊢ A \in dom arctan \to 1 + i (- A) = 1 - i A$
25	24	fveq2d	$⊢ A \in dom arctan \to \log (1 + i (- A)) = \log (1 - i A)$
26	20	oveq2d	$⊢ A \in dom arctan \to 1 - i (- A) = 1 - (- i A)$
27		subneg	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 - (- i A) = 1 + i A$
28	6 9 27	sylancr	$⊢ A \in dom arctan \to 1 - (- i A) = 1 + i A$
29	26 28	eqtrd	$⊢ A \in dom arctan \to 1 - i (- A) = 1 + i A$
30	29	fveq2d	$⊢ A \in dom arctan \to \log (1 - i (- A)) = \log (1 + i A)$
31	25 30	oveq12d	$⊢ A \in dom arctan \to \log (1 + i (- A)) + \log (1 - i (- A)) = \log (1 - i A) + \log (1 + i A)$
32	18 31	eqtr4d	$⊢ A \in dom arctan \to \log (1 + i A) + \log (1 - i A) = \log (1 + i (- A)) + \log (1 - i (- A))$
33	32	adantr	$⊢ (A \in dom arctan \land ℜ (A) \leq 0) \to \log (1 + i A) + \log (1 - i A) = \log (1 + i (- A)) + \log (1 - i (- A))$
34		atandmneg	$⊢ A \in dom arctan \to - A \in dom arctan$
35	4	le0neg1d	$⊢ A \in dom arctan \to (ℜ (A) \leq 0 \leftrightarrow 0 \leq - ℜ (A))$
36	35	biimpa	$⊢ (A \in dom arctan \land ℜ (A) \leq 0) \to 0 \leq - ℜ (A)$
37	3	renegd	$⊢ A \in dom arctan \to ℜ (- A) = - ℜ (A)$
38	37	adantr	$⊢ (A \in dom arctan \land ℜ (A) \leq 0) \to ℜ (- A) = - ℜ (A)$
39	36 38	breqtrrd	$⊢ (A \in dom arctan \land ℜ (A) \leq 0) \to 0 \leq ℜ (- A)$
40		atanlogaddlem	$⊢ (- A \in dom arctan \land 0 \leq ℜ (- A)) \to \log (1 + i (- A)) + \log (1 - i (- A)) \in ran log$
41	34 39 40	syl2an2r	$⊢ (A \in dom arctan \land ℜ (A) \leq 0) \to \log (1 + i (- A)) + \log (1 - i (- A)) \in ran log$
42	33 41	eqeltrd	$⊢ (A \in dom arctan \land ℜ (A) \leq 0) \to \log (1 + i A) + \log (1 - i A) \in ran log$
43	1 4 5 42	lecasei	$⊢ A \in dom arctan \to \log (1 + i A) + \log (1 - i A) \in ran log$

Metamath Proof Explorer

Theorem atanlogadd

Proof