Theorem logneg2

Description: The logarithm of the negative of a number with positive imaginary part is _i x. _pi less than the original. (Compare logneg .) (Contributed by Mario Carneiro, 3-Apr-2015)

	Ref	Expression
Assertion	logneg2	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( log ‘ - 𝐴 ) = ( ( log ‘ 𝐴 ) − ( i · π ) ) )

Proof

Step	Hyp	Ref	Expression
1		imcl	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
2		gt0ne0	⊢ ( ( ( ℑ ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ 𝐴 ) ≠ 0 )
3	1 2	sylan	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ 𝐴 ) ≠ 0 )
4		fveq2	⊢ ( 𝐴 = 0 → ( ℑ ‘ 𝐴 ) = ( ℑ ‘ 0 ) )
5		im0	⊢ ( ℑ ‘ 0 ) = 0
6	4 5	eqtrdi	⊢ ( 𝐴 = 0 → ( ℑ ‘ 𝐴 ) = 0 )
7	6	necon3i	⊢ ( ( ℑ ‘ 𝐴 ) ≠ 0 → 𝐴 ≠ 0 )
8	3 7	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → 𝐴 ≠ 0 )
9		logcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
10	8 9	syldan	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( log ‘ 𝐴 ) ∈ ℂ )
11		ax-icn	⊢ i ∈ ℂ
12		picn	⊢ π ∈ ℂ
13	11 12	mulcli	⊢ ( i · π ) ∈ ℂ
14		efsub	⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( i · π ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) / ( exp ‘ ( i · π ) ) ) )
15	10 13 14	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( exp ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) / ( exp ‘ ( i · π ) ) ) )
16		eflog	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
17	8 16	syldan	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
18		efipi	⊢ ( exp ‘ ( i · π ) ) = - 1
19	18	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( exp ‘ ( i · π ) ) = - 1 )
20	17 19	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( exp ‘ ( log ‘ 𝐴 ) ) / ( exp ‘ ( i · π ) ) ) = ( 𝐴 / - 1 ) )
21		ax-1cn	⊢ 1 ∈ ℂ
22		ax-1ne0	⊢ 1 ≠ 0
23		divneg2	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ) → - ( 𝐴 / 1 ) = ( 𝐴 / - 1 ) )
24	21 22 23	mp3an23	⊢ ( 𝐴 ∈ ℂ → - ( 𝐴 / 1 ) = ( 𝐴 / - 1 ) )
25		div1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 / 1 ) = 𝐴 )
26	25	negeqd	⊢ ( 𝐴 ∈ ℂ → - ( 𝐴 / 1 ) = - 𝐴 )
27	24 26	eqtr3d	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 / - 1 ) = - 𝐴 )
28	27	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 𝐴 / - 1 ) = - 𝐴 )
29	15 20 28	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( exp ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) = - 𝐴 )
30	29	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) ) = ( log ‘ - 𝐴 ) )
31		subcl	⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( i · π ) ∈ ℂ ) → ( ( log ‘ 𝐴 ) − ( i · π ) ) ∈ ℂ )
32	10 13 31	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( log ‘ 𝐴 ) − ( i · π ) ) ∈ ℂ )
33		argimgt0	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( 0 (,) π ) )
34		eliooord	⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( 0 (,) π ) → ( 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) < π ) )
35	33 34	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) < π ) )
36	35	simpld	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) )
37		imcl	⊢ ( ( log ‘ 𝐴 ) ∈ ℂ → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
38	10 37	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
39		pire	⊢ π ∈ ℝ
40	39	renegcli	⊢ - π ∈ ℝ
41		ltaddpos2	⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ - π ∈ ℝ ) → ( 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) ↔ - π < ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + - π ) ) )
42	38 40 41	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 0 < ( ℑ ‘ ( log ‘ 𝐴 ) ) ↔ - π < ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + - π ) ) )
43	36 42	mpbid	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → - π < ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + - π ) )
44	38	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
45		negsub	⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ ∧ π ∈ ℂ ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + - π ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) )
46	44 12 45	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) + - π ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) )
47	43 46	breqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → - π < ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) )
48		imsub	⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( i · π ) ∈ ℂ ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − ( ℑ ‘ ( i · π ) ) ) )
49	10 13 48	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − ( ℑ ‘ ( i · π ) ) ) )
50		reim	⊢ ( π ∈ ℂ → ( ℜ ‘ π ) = ( ℑ ‘ ( i · π ) ) )
51	12 50	ax-mp	⊢ ( ℜ ‘ π ) = ( ℑ ‘ ( i · π ) )
52		rere	⊢ ( π ∈ ℝ → ( ℜ ‘ π ) = π )
53	39 52	ax-mp	⊢ ( ℜ ‘ π ) = π
54	51 53	eqtr3i	⊢ ( ℑ ‘ ( i · π ) ) = π
55	54	oveq2i	⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − ( ℑ ‘ ( i · π ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π )
56	49 55	eqtrdi	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) )
57	47 56	breqtrrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → - π < ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) )
58		resubcl	⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) ∈ ℝ )
59	38 39 58	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) ∈ ℝ )
60	39	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → π ∈ ℝ )
61		0re	⊢ 0 ∈ ℝ
62		pipos	⊢ 0 < π
63	61 39 62	ltleii	⊢ 0 ≤ π
64		subge02	⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( 0 ≤ π ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
65	38 39 64	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( 0 ≤ π ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
66	63 65	mpbii	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) )
67		logimcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
68	8 67	syldan	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
69	68	simprd	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π )
70	59 38 60 66 69	letrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) − π ) ≤ π )
71	56 70	eqbrtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) ≤ π )
72		ellogrn	⊢ ( ( ( log ‘ 𝐴 ) − ( i · π ) ) ∈ ran log ↔ ( ( ( log ‘ 𝐴 ) − ( i · π ) ) ∈ ℂ ∧ - π < ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) ∧ ( ℑ ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) ≤ π ) )
73	32 57 71 72	syl3anbrc	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( ( log ‘ 𝐴 ) − ( i · π ) ) ∈ ran log )
74		logef	⊢ ( ( ( log ‘ 𝐴 ) − ( i · π ) ) ∈ ran log → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) ) = ( ( log ‘ 𝐴 ) − ( i · π ) ) )
75	73 74	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) − ( i · π ) ) ) ) = ( ( log ‘ 𝐴 ) − ( i · π ) ) )
76	30 75	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 < ( ℑ ‘ 𝐴 ) ) → ( log ‘ - 𝐴 ) = ( ( log ‘ 𝐴 ) − ( i · π ) ) )