logimul

Description: Multiplying a number by _i increases the logarithm of the number by _i _pi / 2 . (Contributed by Mario Carneiro, 4-Apr-2015)

		Ref	Expression
	Assertion	logimul	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to \log i A = \log A + i (\frac{π}{2})$

Proof

Step	Hyp	Ref	Expression
1		logcl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ℂ$
2	1	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to \log A \in ℂ$
3		ax-icn	$⊢ i \in ℂ$
4		halfpire	$⊢ \frac{π}{2} \in ℝ$
5	4	recni	$⊢ \frac{π}{2} \in ℂ$
6	3 5	mulcli	$⊢ i (\frac{π}{2}) \in ℂ$
7		efadd	$⊢ (\log A \in ℂ \land i (\frac{π}{2}) \in ℂ) \to e^{\log A + i (\frac{π}{2})} = e^{\log A} e^{i (\frac{π}{2})}$
8	2 6 7	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to e^{\log A + i (\frac{π}{2})} = e^{\log A} e^{i (\frac{π}{2})}$
9		eflog	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = A$
10	9	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to e^{\log A} = A$
11		efhalfpi	$⊢ e^{i (\frac{π}{2})} = i$
12	11	a1i	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to e^{i (\frac{π}{2})} = i$
13	10 12	oveq12d	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to e^{\log A} e^{i (\frac{π}{2})} = A i$
14		simp1	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to A \in ℂ$
15		mulcom	$⊢ (A \in ℂ \land i \in ℂ) \to A i = i A$
16	14 3 15	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to A i = i A$
17	8 13 16	3eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to e^{\log A + i (\frac{π}{2})} = i A$
18	17	fveq2d	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to \log e^{\log A + i (\frac{π}{2})} = \log i A$
19		addcl	$⊢ (\log A \in ℂ \land i (\frac{π}{2}) \in ℂ) \to \log A + i (\frac{π}{2}) \in ℂ$
20	2 6 19	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to \log A + i (\frac{π}{2}) \in ℂ$
21		pire	$⊢ π \in ℝ$
22	21	renegcli	$⊢ - π \in ℝ$
23	22	a1i	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to - π \in ℝ$
24	2	imcld	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to ℑ (\log A) \in ℝ$
25		readdcl	$⊢ (ℑ (\log A) \in ℝ \land \frac{π}{2} \in ℝ) \to ℑ (\log A) + (\frac{π}{2}) \in ℝ$
26	24 4 25	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to ℑ (\log A) + (\frac{π}{2}) \in ℝ$
27		logimcl	$⊢ (A \in ℂ \land A \neq 0) \to (- π < ℑ (\log A) \land ℑ (\log A) \leq π)$
28	27	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to (- π < ℑ (\log A) \land ℑ (\log A) \leq π)$
29	28	simpld	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to - π < ℑ (\log A)$
30		pirp	$⊢ π \in ℝ^{+}$
31		rphalfcl	$⊢ π \in ℝ^{+} \to \frac{π}{2} \in ℝ^{+}$
32	30 31	ax-mp	$⊢ \frac{π}{2} \in ℝ^{+}$
33		ltaddrp	$⊢ (ℑ (\log A) \in ℝ \land \frac{π}{2} \in ℝ^{+}) \to ℑ (\log A) < ℑ (\log A) + (\frac{π}{2})$
34	24 32 33	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to ℑ (\log A) < ℑ (\log A) + (\frac{π}{2})$
35	23 24 26 29 34	lttrd	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to - π < ℑ (\log A) + (\frac{π}{2})$
36		imadd	$⊢ (\log A \in ℂ \land i (\frac{π}{2}) \in ℂ) \to ℑ (\log A + i (\frac{π}{2})) = ℑ (\log A) + ℑ (i (\frac{π}{2}))$
37	2 6 36	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to ℑ (\log A + i (\frac{π}{2})) = ℑ (\log A) + ℑ (i (\frac{π}{2}))$
38		reim	$⊢ \frac{π}{2} \in ℂ \to ℜ (\frac{π}{2}) = ℑ (i (\frac{π}{2}))$
39	5 38	ax-mp	$⊢ ℜ (\frac{π}{2}) = ℑ (i (\frac{π}{2}))$
40		rere	$⊢ \frac{π}{2} \in ℝ \to ℜ (\frac{π}{2}) = \frac{π}{2}$
41	4 40	ax-mp	$⊢ ℜ (\frac{π}{2}) = \frac{π}{2}$
42	39 41	eqtr3i	$⊢ ℑ (i (\frac{π}{2})) = \frac{π}{2}$
43	42	oveq2i	$⊢ ℑ (\log A) + ℑ (i (\frac{π}{2})) = ℑ (\log A) + (\frac{π}{2})$
44	37 43	eqtrdi	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to ℑ (\log A + i (\frac{π}{2})) = ℑ (\log A) + (\frac{π}{2})$
45	35 44	breqtrrd	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to - π < ℑ (\log A + i (\frac{π}{2}))$
46		argrege0	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to ℑ (\log A) \in [- \frac{π}{2}, \frac{π}{2}]$
47	4	renegcli	$⊢ - \frac{π}{2} \in ℝ$
48	47 4	elicc2i	$⊢ ℑ (\log A) \in [- \frac{π}{2}, \frac{π}{2}] \leftrightarrow (ℑ (\log A) \in ℝ \land - \frac{π}{2} \leq ℑ (\log A) \land ℑ (\log A) \leq \frac{π}{2})$
49	48	simp3bi	$⊢ ℑ (\log A) \in [- \frac{π}{2}, \frac{π}{2}] \to ℑ (\log A) \leq \frac{π}{2}$
50	46 49	syl	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to ℑ (\log A) \leq \frac{π}{2}$
51	21	recni	$⊢ π \in ℂ$
52		pidiv2halves	$⊢ (\frac{π}{2}) + (\frac{π}{2}) = π$
53	51 5 5 52	subaddrii	$⊢ π - (\frac{π}{2}) = \frac{π}{2}$
54	50 53	breqtrrdi	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to ℑ (\log A) \leq π - (\frac{π}{2})$
55	4	a1i	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to \frac{π}{2} \in ℝ$
56	21	a1i	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to π \in ℝ$
57		leaddsub	$⊢ (ℑ (\log A) \in ℝ \land \frac{π}{2} \in ℝ \land π \in ℝ) \to (ℑ (\log A) + (\frac{π}{2}) \leq π \leftrightarrow ℑ (\log A) \leq π - (\frac{π}{2}))$
58	24 55 56 57	syl3anc	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to (ℑ (\log A) + (\frac{π}{2}) \leq π \leftrightarrow ℑ (\log A) \leq π - (\frac{π}{2}))$
59	54 58	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to ℑ (\log A) + (\frac{π}{2}) \leq π$
60	44 59	eqbrtrd	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to ℑ (\log A + i (\frac{π}{2})) \leq π$
61		ellogrn	$⊢ \log A + i (\frac{π}{2}) \in ran log \leftrightarrow (\log A + i (\frac{π}{2}) \in ℂ \land - π < ℑ (\log A + i (\frac{π}{2})) \land ℑ (\log A + i (\frac{π}{2})) \leq π)$
62	20 45 60 61	syl3anbrc	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to \log A + i (\frac{π}{2}) \in ran log$
63		logef	$⊢ \log A + i (\frac{π}{2}) \in ran log \to \log e^{\log A + i (\frac{π}{2})} = \log A + i (\frac{π}{2})$
64	62 63	syl	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to \log e^{\log A + i (\frac{π}{2})} = \log A + i (\frac{π}{2})$
65	18 64	eqtr3d	$⊢ (A \in ℂ \land A \neq 0 \land 0 \leq ℜ (A)) \to \log i A = \log A + i (\frac{π}{2})$

Metamath Proof Explorer

Theorem logimul

Proof