ang180lem4

Description: Lemma for ang180 . Reduce the statement to one variable. (Contributed by Mario Carneiro, 23-Sep-2014)

		Ref	Expression
	Hypothesis	ang.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
	Assertion	ang180lem4	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ((1 - A) F 1) + (A F (A - 1)) + (1 F A) \in \{- π, π\}$

Proof

Step	Hyp	Ref	Expression
1		ang.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
2		1cnd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 \in ℂ$
3		simp1	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \in ℂ$
4	2 3	subcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 - A \in ℂ$
5		simp3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \neq 1$
6	5	necomd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 \neq A$
7	2 3 6	subne0d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 - A \neq 0$
8		ax-1ne0	$⊢ 1 \neq 0$
9	8	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 \neq 0$
10	1 4 7 2 9	angvald	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (1 - A) F 1 = ℑ (\log (\frac{1}{1 - A}))$
11		simp2	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \neq 0$
12	3 2	subcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A - 1 \in ℂ$
13	3 2 5	subne0d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A - 1 \neq 0$
14	1 3 11 12 13	angvald	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A F (A - 1) = ℑ (\log (\frac{A - 1}{A}))$
15	10 14	oveq12d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ((1 - A) F 1) + (A F (A - 1)) = ℑ (\log (\frac{1}{1 - A})) + ℑ (\log (\frac{A - 1}{A}))$
16	2 4 7	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{1}{1 - A} \in ℂ$
17	4 7	recne0d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{1}{1 - A} \neq 0$
18	16 17	logcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{1}{1 - A}) \in ℂ$
19	12 3 11	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{A - 1}{A} \in ℂ$
20	12 3 13 11	divne0d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{A - 1}{A} \neq 0$
21	19 20	logcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{A - 1}{A}) \in ℂ$
22	18 21	imaddd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) = ℑ (\log (\frac{1}{1 - A})) + ℑ (\log (\frac{A - 1}{A}))$
23	15 22	eqtr4d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ((1 - A) F 1) + (A F (A - 1)) = ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}))$
24	1 2 9 3 11	angvald	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 F A = ℑ (\log (\frac{A}{1}))$
25	3	div1d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{A}{1} = A$
26	25	fveq2d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{A}{1}) = \log A$
27	26	fveq2d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log (\frac{A}{1})) = ℑ (\log A)$
28	24 27	eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 F A = ℑ (\log A)$
29	23 28	oveq12d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ((1 - A) F 1) + (A F (A - 1)) + (1 F A) = ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) + ℑ (\log A)$
30	18 21	addcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) \in ℂ$
31	3 11	logcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log A \in ℂ$
32	30 31	imaddd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A) = ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) + ℑ (\log A)$
33	29 32	eqtr4d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ((1 - A) F 1) + (A F (A - 1)) + (1 F A) = ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A)$
34		eqid	$⊢ \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A = \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A$
35		eqid	$⊢ (\frac{\frac{\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A}{i}}{2 π}) - (\frac{1}{2}) = (\frac{\frac{\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A}{i}}{2 π}) - (\frac{1}{2})$
36	1 34 35	ang180lem3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A \in \{- i π, i π\}$
37		fveq2	$⊢ \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A = - i π \to ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A) = ℑ (- i π)$
38		ax-icn	$⊢ i \in ℂ$
39		picn	$⊢ π \in ℂ$
40	38 39	mulcli	$⊢ i π \in ℂ$
41	40	imnegi	$⊢ ℑ (- i π) = - ℑ (i π)$
42	40	addlidi	$⊢ 0 + i π = i π$
43	42	fveq2i	$⊢ ℑ (0 + i π) = ℑ (i π)$
44		0re	$⊢ 0 \in ℝ$
45		pire	$⊢ π \in ℝ$
46	44 45	crimi	$⊢ ℑ (0 + i π) = π$
47	43 46	eqtr3i	$⊢ ℑ (i π) = π$
48	47	negeqi	$⊢ - ℑ (i π) = - π$
49	41 48	eqtri	$⊢ ℑ (- i π) = - π$
50	37 49	eqtrdi	$⊢ \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A = - i π \to ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A) = - π$
51		fveq2	$⊢ \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A = i π \to ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A) = ℑ (i π)$
52	51 47	eqtrdi	$⊢ \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A = i π \to ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A) = π$
53	50 52	orim12i	$⊢ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A = - i π \lor \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A = i π) \to (ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A) = - π \lor ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A) = π)$
54		ovex	$⊢ \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A \in V$
55	54	elpr	$⊢ \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A \in \{- i π, i π\} \leftrightarrow (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A = - i π \lor \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A = i π)$
56		fvex	$⊢ ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A) \in V$
57	56	elpr	$⊢ ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A) \in \{- π, π\} \leftrightarrow (ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A) = - π \lor ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A) = π)$
58	53 55 57	3imtr4i	$⊢ \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A \in \{- i π, i π\} \to ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A) \in \{- π, π\}$
59	36 58	syl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A) \in \{- π, π\}$
60	33 59	eqeltrd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ((1 - A) F 1) + (A F (A - 1)) + (1 F A) \in \{- π, π\}$

Metamath Proof Explorer

Theorem ang180lem4

Proof