Theorem logneg

Description: The natural logarithm of a negative real number. (Contributed by Mario Carneiro, 13-May-2014) (Revised by Mario Carneiro, 3-Apr-2015)

	Ref	Expression
Assertion	logneg	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ - 𝐴 ) = ( ( log ‘ 𝐴 ) + ( i · π ) ) )

Proof

Step	Hyp	Ref	Expression
1		relogcl	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
2	1	recnd	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℂ )
3		ax-icn	⊢ i ∈ ℂ
4		picn	⊢ π ∈ ℂ
5	3 4	mulcli	⊢ ( i · π ) ∈ ℂ
6		efadd	⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( i · π ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( i · π ) ) ) )
7	2 5 6	sylancl	⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( i · π ) ) ) )
8		efipi	⊢ ( exp ‘ ( i · π ) ) = - 1
9	8	oveq2i	⊢ ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( i · π ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) · - 1 )
10		reeflog	⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
11	10	oveq1d	⊢ ( 𝐴 ∈ ℝ+ → ( ( exp ‘ ( log ‘ 𝐴 ) ) · - 1 ) = ( 𝐴 · - 1 ) )
12	9 11	eqtrid	⊢ ( 𝐴 ∈ ℝ+ → ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( i · π ) ) ) = ( 𝐴 · - 1 ) )
13		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
14		neg1cn	⊢ - 1 ∈ ℂ
15		mulcom	⊢ ( ( 𝐴 ∈ ℂ ∧ - 1 ∈ ℂ ) → ( 𝐴 · - 1 ) = ( - 1 · 𝐴 ) )
16	13 14 15	sylancl	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 · - 1 ) = ( - 1 · 𝐴 ) )
17	13	mulm1d	⊢ ( 𝐴 ∈ ℝ+ → ( - 1 · 𝐴 ) = - 𝐴 )
18	16 17	eqtrd	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 · - 1 ) = - 𝐴 )
19	7 12 18	3eqtrd	⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) = - 𝐴 )
20	19	fveq2d	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) ) = ( log ‘ - 𝐴 ) )
21		addcl	⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( i · π ) ∈ ℂ ) → ( ( log ‘ 𝐴 ) + ( i · π ) ) ∈ ℂ )
22	2 5 21	sylancl	⊢ ( 𝐴 ∈ ℝ+ → ( ( log ‘ 𝐴 ) + ( i · π ) ) ∈ ℂ )
23		pipos	⊢ 0 < π
24		pire	⊢ π ∈ ℝ
25		lt0neg2	⊢ ( π ∈ ℝ → ( 0 < π ↔ - π < 0 ) )
26	24 25	ax-mp	⊢ ( 0 < π ↔ - π < 0 )
27	23 26	mpbi	⊢ - π < 0
28	24	renegcli	⊢ - π ∈ ℝ
29		0re	⊢ 0 ∈ ℝ
30	28 29 24	lttri	⊢ ( ( - π < 0 ∧ 0 < π ) → - π < π )
31	27 23 30	mp2an	⊢ - π < π
32		crim	⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ π ∈ ℝ ) → ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) = π )
33	1 24 32	sylancl	⊢ ( 𝐴 ∈ ℝ+ → ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) = π )
34	31 33	breqtrrid	⊢ ( 𝐴 ∈ ℝ+ → - π < ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) )
35	24	leidi	⊢ π ≤ π
36	33 35	eqbrtrdi	⊢ ( 𝐴 ∈ ℝ+ → ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) ≤ π )
37		ellogrn	⊢ ( ( ( log ‘ 𝐴 ) + ( i · π ) ) ∈ ran log ↔ ( ( ( log ‘ 𝐴 ) + ( i · π ) ) ∈ ℂ ∧ - π < ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) ∧ ( ℑ ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) ≤ π ) )
38	22 34 36 37	syl3anbrc	⊢ ( 𝐴 ∈ ℝ+ → ( ( log ‘ 𝐴 ) + ( i · π ) ) ∈ ran log )
39		logef	⊢ ( ( ( log ‘ 𝐴 ) + ( i · π ) ) ∈ ran log → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) ) = ( ( log ‘ 𝐴 ) + ( i · π ) ) )
40	38 39	syl	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) + ( i · π ) ) ) ) = ( ( log ‘ 𝐴 ) + ( i · π ) ) )
41	20 40	eqtr3d	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ - 𝐴 ) = ( ( log ‘ 𝐴 ) + ( i · π ) ) )