Theorem 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	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log )

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	⊢ 1 ∈ ℂ
2		ax-icn	⊢ i ∈ ℂ
3		atandm2	⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
4	3	simp1bi	⊢ ( 𝐴 ∈ dom arctan → 𝐴 ∈ ℂ )
5		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
6	2 4 5	sylancr	⊢ ( 𝐴 ∈ dom arctan → ( i · 𝐴 ) ∈ ℂ )
7		addcl	⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
8	1 6 7	sylancr	⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
9	3	simp3bi	⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ≠ 0 )
10	8 9	logcld	⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ )
11		subcl	⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
12	1 6 11	sylancr	⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
13	3	simp2bi	⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ≠ 0 )
14	12 13	logcld	⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ )
15	10 14	subcld	⊢ ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ )
16	15	adantr	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ )
17	4	recld	⊢ ( 𝐴 ∈ dom arctan → ( ℜ ‘ 𝐴 ) ∈ ℝ )
18		0re	⊢ 0 ∈ ℝ
19		lttri2	⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ℜ ‘ 𝐴 ) ≠ 0 ↔ ( ( ℜ ‘ 𝐴 ) < 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) ) )
20	17 18 19	sylancl	⊢ ( 𝐴 ∈ dom arctan → ( ( ℜ ‘ 𝐴 ) ≠ 0 ↔ ( ( ℜ ‘ 𝐴 ) < 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) ) )
21	20	biimpa	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ℜ ‘ 𝐴 ) < 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) )
22	15	imnegd	⊢ ( 𝐴 ∈ dom arctan → ( ℑ ‘ - ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) )
23	10 14	negsubdi2d	⊢ ( 𝐴 ∈ dom arctan → - ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
24		mulneg2	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
25	2 4 24	sylancr	⊢ ( 𝐴 ∈ dom arctan → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
26	25	oveq2d	⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · - 𝐴 ) ) = ( 1 + - ( i · 𝐴 ) ) )
27		negsub	⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + - ( i · 𝐴 ) ) = ( 1 − ( i · 𝐴 ) ) )
28	1 6 27	sylancr	⊢ ( 𝐴 ∈ dom arctan → ( 1 + - ( i · 𝐴 ) ) = ( 1 − ( i · 𝐴 ) ) )
29	26 28	eqtrd	⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · - 𝐴 ) ) = ( 1 − ( i · 𝐴 ) ) )
30	29	fveq2d	⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) = ( log ‘ ( 1 − ( i · 𝐴 ) ) ) )
31	25	oveq2d	⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · - 𝐴 ) ) = ( 1 − - ( i · 𝐴 ) ) )
32		subneg	⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − - ( i · 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
33	1 6 32	sylancr	⊢ ( 𝐴 ∈ dom arctan → ( 1 − - ( i · 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
34	31 33	eqtrd	⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · - 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
35	34	fveq2d	⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) = ( log ‘ ( 1 + ( i · 𝐴 ) ) ) )
36	30 35	oveq12d	⊢ ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) = ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
37	23 36	eqtr4d	⊢ ( 𝐴 ∈ dom arctan → - ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) )
38	37	fveq2d	⊢ ( 𝐴 ∈ dom arctan → ( ℑ ‘ - ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) )
39	22 38	eqtr3d	⊢ ( 𝐴 ∈ dom arctan → - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) )
40	39	adantr	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) )
41		atandmneg	⊢ ( 𝐴 ∈ dom arctan → - 𝐴 ∈ dom arctan )
42	17	lt0neg1d	⊢ ( 𝐴 ∈ dom arctan → ( ( ℜ ‘ 𝐴 ) < 0 ↔ 0 < - ( ℜ ‘ 𝐴 ) ) )
43	42	biimpa	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → 0 < - ( ℜ ‘ 𝐴 ) )
44	4	adantr	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → 𝐴 ∈ ℂ )
45	44	renegd	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℜ ‘ - 𝐴 ) = - ( ℜ ‘ 𝐴 ) )
46	43 45	breqtrrd	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → 0 < ( ℜ ‘ - 𝐴 ) )
47		atanlogsublem	⊢ ( ( - 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ - 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )
48	41 46 47	syl2an2r	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )
49		picn	⊢ π ∈ ℂ
50	49	negnegi	⊢ - - π = π
51	50	oveq2i	⊢ ( - π (,) - - π ) = ( - π (,) π )
52	48 51	eleqtrrdi	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) ∈ ( - π (,) - - π ) )
53	40 52	eqeltrd	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) - - π ) )
54		pire	⊢ π ∈ ℝ
55	54	renegcli	⊢ - π ∈ ℝ
56	15	adantr	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ )
57	56	imcld	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ℝ )
58		iooneg	⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ∧ ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ℝ ) → ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) ↔ - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) - - π ) ) )
59	55 54 57 58	mp3an12i	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) ↔ - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) - - π ) ) )
60	53 59	mpbird	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )
61		atanlogsublem	⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )
62	60 61	jaodan	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ( ℜ ‘ 𝐴 ) < 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )
63	21 62	syldan	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )
64		eliooord	⊢ ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) → ( - π < ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∧ ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π ) )
65	63 64	syl	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( - π < ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∧ ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π ) )
66	65	simpld	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → - π < ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) )
67	65	simprd	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π )
68	16	imcld	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ℝ )
69		ltle	⊢ ( ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ≤ π ) )
70	68 54 69	sylancl	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ≤ π ) )
71	67 70	mpd	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ≤ π )
72		ellogrn	⊢ ( ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log ↔ ( ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ ∧ - π < ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∧ ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ≤ π ) )
73	16 66 71 72	syl3anbrc	⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log )