atanlogsub

Description: A variation on atanlogadd , to show that sqrt ( 1 +i z ) / sqrt ( 1 - i z ) = sqrt ( ( 1 +i z ) / ( 1 - i z ) ) under more limited conditions. (Contributed by Mario Carneiro, 4-Apr-2015)

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

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	simp1bi	$⊢ A \in dom arctan \to A \in ℂ$
5		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
6	2 4 5	sylancr	$⊢ A \in dom arctan \to i A \in ℂ$
7		addcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 + i A \in ℂ$
8	1 6 7	sylancr	$⊢ A \in dom arctan \to 1 + i A \in ℂ$
9	3	simp3bi	$⊢ A \in dom arctan \to 1 + i A \neq 0$
10	8 9	logcld	$⊢ A \in dom arctan \to \log (1 + i A) \in ℂ$
11		subcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 - i A \in ℂ$
12	1 6 11	sylancr	$⊢ A \in dom arctan \to 1 - i A \in ℂ$
13	3	simp2bi	$⊢ A \in dom arctan \to 1 - i A \neq 0$
14	12 13	logcld	$⊢ A \in dom arctan \to \log (1 - i A) \in ℂ$
15	10 14	subcld	$⊢ A \in dom arctan \to \log (1 + i A) - \log (1 - i A) \in ℂ$
16	15	adantr	$⊢ (A \in dom arctan \land ℜ (A) \neq 0) \to \log (1 + i A) - \log (1 - i A) \in ℂ$
17	4	recld	$⊢ A \in dom arctan \to ℜ (A) \in ℝ$
18		0re	$⊢ 0 \in ℝ$
19		lttri2	$⊢ (ℜ (A) \in ℝ \land 0 \in ℝ) \to (ℜ (A) \neq 0 \leftrightarrow (ℜ (A) < 0 \lor 0 < ℜ (A)))$
20	17 18 19	sylancl	$⊢ A \in dom arctan \to (ℜ (A) \neq 0 \leftrightarrow (ℜ (A) < 0 \lor 0 < ℜ (A)))$
21	20	biimpa	$⊢ (A \in dom arctan \land ℜ (A) \neq 0) \to (ℜ (A) < 0 \lor 0 < ℜ (A))$
22	15	imnegd	$⊢ A \in dom arctan \to ℑ (- (\log (1 + i A) - \log (1 - i A))) = - ℑ (\log (1 + i A) - \log (1 - i A))$
23	10 14	negsubdi2d	$⊢ A \in dom arctan \to - (\log (1 + i A) - \log (1 - i A)) = \log (1 - i A) - \log (1 + i A)$
24		mulneg2	$⊢ (i \in ℂ \land A \in ℂ) \to i (- A) = - i A$
25	2 4 24	sylancr	$⊢ A \in dom arctan \to i (- A) = - i A$
26	25	oveq2d	$⊢ A \in dom arctan \to 1 + i (- A) = 1 + (- i A)$
27		negsub	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 + (- i A) = 1 - i A$
28	1 6 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	oveq2d	$⊢ A \in dom arctan \to 1 - i (- A) = 1 - (- i A)$
32		subneg	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 - (- i A) = 1 + i A$
33	1 6 32	sylancr	$⊢ A \in dom arctan \to 1 - (- i A) = 1 + i A$
34	31 33	eqtrd	$⊢ A \in dom arctan \to 1 - i (- A) = 1 + i A$
35	34	fveq2d	$⊢ A \in dom arctan \to \log (1 - i (- A)) = \log (1 + i A)$
36	30 35	oveq12d	$⊢ A \in dom arctan \to \log (1 + i (- A)) - \log (1 - i (- A)) = \log (1 - i A) - \log (1 + i A)$
37	23 36	eqtr4d	$⊢ A \in dom arctan \to - (\log (1 + i A) - \log (1 - i A)) = \log (1 + i (- A)) - \log (1 - i (- A))$
38	37	fveq2d	$⊢ A \in dom arctan \to ℑ (- (\log (1 + i A) - \log (1 - i A))) = ℑ (\log (1 + i (- A)) - \log (1 - i (- A)))$
39	22 38	eqtr3d	$⊢ A \in dom arctan \to - ℑ (\log (1 + i A) - \log (1 - i A)) = ℑ (\log (1 + i (- A)) - \log (1 - i (- A)))$
40	39	adantr	$⊢ (A \in dom arctan \land ℜ (A) < 0) \to - ℑ (\log (1 + i A) - \log (1 - i A)) = ℑ (\log (1 + i (- A)) - \log (1 - i (- A)))$
41		atandmneg	$⊢ A \in dom arctan \to - A \in dom arctan$
42	17	lt0neg1d	$⊢ A \in dom arctan \to (ℜ (A) < 0 \leftrightarrow 0 < - ℜ (A))$
43	42	biimpa	$⊢ (A \in dom arctan \land ℜ (A) < 0) \to 0 < - ℜ (A)$
44	4	adantr	$⊢ (A \in dom arctan \land ℜ (A) < 0) \to A \in ℂ$
45	44	renegd	$⊢ (A \in dom arctan \land ℜ (A) < 0) \to ℜ (- A) = - ℜ (A)$
46	43 45	breqtrrd	$⊢ (A \in dom arctan \land ℜ (A) < 0) \to 0 < ℜ (- A)$
47		atanlogsublem	$⊢ (- A \in dom arctan \land 0 < ℜ (- A)) \to ℑ (\log (1 + i (- A)) - \log (1 - i (- A))) \in (- π, π)$
48	41 46 47	syl2an2r	$⊢ (A \in dom arctan \land ℜ (A) < 0) \to ℑ (\log (1 + i (- A)) - \log (1 - i (- A))) \in (- π, π)$
49		picn	$⊢ π \in ℂ$
50	49	negnegi	$⊢ - (- π) = π$
51	50	oveq2i	$⊢ (- π, - (- π)) = (- π, π)$
52	48 51	eleqtrrdi	$⊢ (A \in dom arctan \land ℜ (A) < 0) \to ℑ (\log (1 + i (- A)) - \log (1 - i (- A))) \in (- π, - (- π))$
53	40 52	eqeltrd	$⊢ (A \in dom arctan \land ℜ (A) < 0) \to - ℑ (\log (1 + i A) - \log (1 - i A)) \in (- π, - (- π))$
54		pire	$⊢ π \in ℝ$
55	54	renegcli	$⊢ - π \in ℝ$
56	15	adantr	$⊢ (A \in dom arctan \land ℜ (A) < 0) \to \log (1 + i A) - \log (1 - i A) \in ℂ$
57	56	imcld	$⊢ (A \in dom arctan \land ℜ (A) < 0) \to ℑ (\log (1 + i A) - \log (1 - i A)) \in ℝ$
58		iooneg	$⊢ (- π \in ℝ \land π \in ℝ \land ℑ (\log (1 + i A) - \log (1 - i A)) \in ℝ) \to (ℑ (\log (1 + i A) - \log (1 - i A)) \in (- π, π) \leftrightarrow - ℑ (\log (1 + i A) - \log (1 - i A)) \in (- π, - (- π)))$
59	55 54 57 58	mp3an12i	$⊢ (A \in dom arctan \land ℜ (A) < 0) \to (ℑ (\log (1 + i A) - \log (1 - i A)) \in (- π, π) \leftrightarrow - ℑ (\log (1 + i A) - \log (1 - i A)) \in (- π, - (- π)))$
60	53 59	mpbird	$⊢ (A \in dom arctan \land ℜ (A) < 0) \to ℑ (\log (1 + i A) - \log (1 - i A)) \in (- π, π)$
61		atanlogsublem	$⊢ (A \in dom arctan \land 0 < ℜ (A)) \to ℑ (\log (1 + i A) - \log (1 - i A)) \in (- π, π)$
62	60 61	jaodan	$⊢ (A \in dom arctan \land (ℜ (A) < 0 \lor 0 < ℜ (A))) \to ℑ (\log (1 + i A) - \log (1 - i A)) \in (- π, π)$
63	21 62	syldan	$⊢ (A \in dom arctan \land ℜ (A) \neq 0) \to ℑ (\log (1 + i A) - \log (1 - i A)) \in (- π, π)$
64		eliooord	$⊢ ℑ (\log (1 + i A) - \log (1 - i A)) \in (- π, π) \to (- π < ℑ (\log (1 + i A) - \log (1 - i A)) \land ℑ (\log (1 + i A) - \log (1 - i A)) < π)$
65	63 64	syl	$⊢ (A \in dom arctan \land ℜ (A) \neq 0) \to (- π < ℑ (\log (1 + i A) - \log (1 - i A)) \land ℑ (\log (1 + i A) - \log (1 - i A)) < π)$
66	65	simpld	$⊢ (A \in dom arctan \land ℜ (A) \neq 0) \to - π < ℑ (\log (1 + i A) - \log (1 - i A))$
67	65	simprd	$⊢ (A \in dom arctan \land ℜ (A) \neq 0) \to ℑ (\log (1 + i A) - \log (1 - i A)) < π$
68	16	imcld	$⊢ (A \in dom arctan \land ℜ (A) \neq 0) \to ℑ (\log (1 + i A) - \log (1 - i A)) \in ℝ$
69		ltle	$⊢ (ℑ (\log (1 + i A) - \log (1 - i A)) \in ℝ \land π \in ℝ) \to (ℑ (\log (1 + i A) - \log (1 - i A)) < π \to ℑ (\log (1 + i A) - \log (1 - i A)) \leq π)$
70	68 54 69	sylancl	$⊢ (A \in dom arctan \land ℜ (A) \neq 0) \to (ℑ (\log (1 + i A) - \log (1 - i A)) < π \to ℑ (\log (1 + i A) - \log (1 - i A)) \leq π)$
71	67 70	mpd	$⊢ (A \in dom arctan \land ℜ (A) \neq 0) \to ℑ (\log (1 + i A) - \log (1 - i A)) \leq π$
72		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 π)$
73	16 66 71 72	syl3anbrc	$⊢ (A \in dom arctan \land ℜ (A) \neq 0) \to \log (1 + i A) - \log (1 - i A) \in ran log$

Metamath Proof Explorer

Theorem atanlogsub

Proof