ang180lem3

Description: Lemma for ang180 . Since ang180lem1 shows that N is an integer and ang180lem2 shows that N is strictly between -u 2 and 1 , it follows that N e. { -u 1 , 0 } , and these two cases correspond to the two possible values for T . (Contributed by Mario Carneiro, 23-Sep-2014)

	Ref	Expression
Hypotheses	ang.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
	ang180lem1.2	$⊢ T = \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A$
	ang180lem1.3	$⊢ N = (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2})$
Assertion	ang180lem3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to T \in \{- i π, i π\}$

Proof

Step	Hyp	Ref	Expression
1		ang.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
2		ang180lem1.2	$⊢ T = \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A$
3		ang180lem1.3	$⊢ N = (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2})$
4		2cn	$⊢ 2 \in ℂ$
5		picn	$⊢ π \in ℂ$
6	4 5	mulcli	$⊢ 2 π \in ℂ$
7		2ne0	$⊢ 2 \neq 0$
8	6 4 7	divreci	$⊢ \frac{2 π}{2} = 2 π (\frac{1}{2})$
9	5 4 7	divcan3i	$⊢ \frac{2 π}{2} = π$
10	8 9	eqtr3i	$⊢ 2 π (\frac{1}{2}) = π$
11	1 2 3	ang180lem2	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- 2 < N \land N < 1)$
12	11	simprd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N < 1$
13		1e0p1	$⊢ 1 = 0 + 1$
14	12 13	breqtrdi	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N < 0 + 1$
15	1 2 3	ang180lem1	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (N \in ℤ \land \frac{T}{i} \in ℝ)$
16	15	simpld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N \in ℤ$
17		0z	$⊢ 0 \in ℤ$
18		zleltp1	$⊢ (N \in ℤ \land 0 \in ℤ) \to (N \leq 0 \leftrightarrow N < 0 + 1)$
19	16 17 18	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (N \leq 0 \leftrightarrow N < 0 + 1)$
20	14 19	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N \leq 0$
21	20	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to N \leq 0$
22		zlem1lt	$⊢ (0 \in ℤ \land N \in ℤ) \to (0 \leq N \leftrightarrow 0 - 1 < N)$
23	17 16 22	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (0 \leq N \leftrightarrow 0 - 1 < N)$
24		df-neg	$⊢ - 1 = 0 - 1$
25	24	breq1i	$⊢ - 1 < N \leftrightarrow 0 - 1 < N$
26	23 25	bitr4di	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (0 \leq N \leftrightarrow - 1 < N)$
27	26	biimpar	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to 0 \leq N$
28	16	zred	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N \in ℝ$
29	28	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to N \in ℝ$
30		0re	$⊢ 0 \in ℝ$
31		letri3	$⊢ (N \in ℝ \land 0 \in ℝ) \to (N = 0 \leftrightarrow (N \leq 0 \land 0 \leq N))$
32	29 30 31	sylancl	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to (N = 0 \leftrightarrow (N \leq 0 \land 0 \leq N))$
33	21 27 32	mpbir2and	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to N = 0$
34	3 33	syl5eqr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}) = 0$
35		ax-1cn	$⊢ 1 \in ℂ$
36		simp1	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \in ℂ$
37		subcl	$⊢ (1 \in ℂ \land A \in ℂ) \to 1 - A \in ℂ$
38	35 36 37	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 - A \in ℂ$
39		simp3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \neq 1$
40	39	necomd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 \neq A$
41		subeq0	$⊢ (1 \in ℂ \land A \in ℂ) \to (1 - A = 0 \leftrightarrow 1 = A)$
42	35 36 41	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (1 - A = 0 \leftrightarrow 1 = A)$
43	42	necon3bid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (1 - A \neq 0 \leftrightarrow 1 \neq A)$
44	40 43	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 - A \neq 0$
45	38 44	reccld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{1}{1 - A} \in ℂ$
46	38 44	recne0d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{1}{1 - A} \neq 0$
47	45 46	logcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{1}{1 - A}) \in ℂ$
48		subcl	$⊢ (A \in ℂ \land 1 \in ℂ) \to A - 1 \in ℂ$
49	36 35 48	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A - 1 \in ℂ$
50		simp2	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \neq 0$
51	49 36 50	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{A - 1}{A} \in ℂ$
52		subeq0	$⊢ (A \in ℂ \land 1 \in ℂ) \to (A - 1 = 0 \leftrightarrow A = 1)$
53	36 35 52	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (A - 1 = 0 \leftrightarrow A = 1)$
54	53	necon3bid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (A - 1 \neq 0 \leftrightarrow A \neq 1)$
55	39 54	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A - 1 \neq 0$
56	49 36 55 50	divne0d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{A - 1}{A} \neq 0$
57	51 56	logcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{A - 1}{A}) \in ℂ$
58	47 57	addcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) \in ℂ$
59		logcl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ℂ$
60	59	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log A \in ℂ$
61	58 60	addcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A \in ℂ$
62	2 61	eqeltrid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to T \in ℂ$
63		ax-icn	$⊢ i \in ℂ$
64	63	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to i \in ℂ$
65		ine0	$⊢ i \neq 0$
66	65	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to i \neq 0$
67	62 64 66	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{T}{i} \in ℂ$
68	6	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π \in ℂ$
69		pire	$⊢ π \in ℝ$
70		pipos	$⊢ 0 < π$
71	69 70	gt0ne0ii	$⊢ π \neq 0$
72	4 5 7 71	mulne0i	$⊢ 2 π \neq 0$
73	72	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π \neq 0$
74	67 68 73	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{\frac{T}{i}}{2 π} \in ℂ$
75	74	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{\frac{T}{i}}{2 π} \in ℂ$
76		halfcn	$⊢ \frac{1}{2} \in ℂ$
77		subeq0	$⊢ (\frac{\frac{T}{i}}{2 π} \in ℂ \land \frac{1}{2} \in ℂ) \to ((\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}) = 0 \leftrightarrow \frac{\frac{T}{i}}{2 π} = \frac{1}{2})$
78	75 76 77	sylancl	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to ((\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}) = 0 \leftrightarrow \frac{\frac{T}{i}}{2 π} = \frac{1}{2})$
79	34 78	mpbid	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{\frac{T}{i}}{2 π} = \frac{1}{2}$
80	67	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{T}{i} \in ℂ$
81	6	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to 2 π \in ℂ$
82	76	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{1}{2} \in ℂ$
83	72	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to 2 π \neq 0$
84	80 81 82 83	divmuld	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to (\frac{\frac{T}{i}}{2 π} = \frac{1}{2} \leftrightarrow 2 π (\frac{1}{2}) = \frac{T}{i})$
85	79 84	mpbid	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to 2 π (\frac{1}{2}) = \frac{T}{i}$
86	10 85	syl5reqr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{T}{i} = π$
87	62	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to T \in ℂ$
88	63	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to i \in ℂ$
89	5	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to π \in ℂ$
90	65	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to i \neq 0$
91	87 88 89 90	divmuld	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to (\frac{T}{i} = π \leftrightarrow i π = T)$
92	86 91	mpbid	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to i π = T$
93	92	eqcomd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to T = i π$
94	93	olcd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to (T = - i π \lor T = i π)$
95	5 63	mulneg1i	$⊢ (- π) i = - π i$
96	5 63	mulcomi	$⊢ π i = i π$
97	96	negeqi	$⊢ - π i = - i π$
98	95 97	eqtri	$⊢ (- π) i = - i π$
99	76 6	mulneg1i	$⊢ (- \frac{1}{2}) 2 π = - (\frac{1}{2}) 2 π$
100	35 4 7	divcan1i	$⊢ (\frac{1}{2}) \cdot 2 = 1$
101	100	oveq1i	$⊢ (\frac{1}{2}) \cdot 2 π = 1 π$
102	76 4 5	mulassi	$⊢ (\frac{1}{2}) \cdot 2 π = (\frac{1}{2}) 2 π$
103	5	mulid2i	$⊢ 1 π = π$
104	101 102 103	3eqtr3i	$⊢ (\frac{1}{2}) 2 π = π$
105	104	negeqi	$⊢ - (\frac{1}{2}) 2 π = - π$
106	99 105	eqtri	$⊢ (- \frac{1}{2}) 2 π = - π$
107	35 76	negsubdii	$⊢ - (1 - (\frac{1}{2})) = - 1 + (\frac{1}{2})$
108		1mhlfehlf	$⊢ 1 - (\frac{1}{2}) = \frac{1}{2}$
109	108	negeqi	$⊢ - (1 - (\frac{1}{2})) = - \frac{1}{2}$
110	107 109	eqtr3i	$⊢ - 1 + (\frac{1}{2}) = - \frac{1}{2}$
111		simpr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - 1 = N$
112	111 3	eqtrdi	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - 1 = (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2})$
113	112	oveq1d	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - 1 + (\frac{1}{2}) = (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}) + (\frac{1}{2})$
114	110 113	syl5eqr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - \frac{1}{2} = (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}) + (\frac{1}{2})$
115		npcan	$⊢ (\frac{\frac{T}{i}}{2 π} \in ℂ \land \frac{1}{2} \in ℂ) \to (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}) + (\frac{1}{2}) = \frac{\frac{T}{i}}{2 π}$
116	74 76 115	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}) + (\frac{1}{2}) = \frac{\frac{T}{i}}{2 π}$
117	116	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}) + (\frac{1}{2}) = \frac{\frac{T}{i}}{2 π}$
118	114 117	eqtrd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - \frac{1}{2} = \frac{\frac{T}{i}}{2 π}$
119	118	oveq1d	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to (- \frac{1}{2}) 2 π = (\frac{\frac{T}{i}}{2 π}) 2 π$
120	106 119	syl5eqr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - π = (\frac{\frac{T}{i}}{2 π}) 2 π$
121	67 68 73	divcan1d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{\frac{T}{i}}{2 π}) 2 π = \frac{T}{i}$
122	121	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to (\frac{\frac{T}{i}}{2 π}) 2 π = \frac{T}{i}$
123	120 122	eqtrd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - π = \frac{T}{i}$
124	123	oveq1d	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to (- π) i = (\frac{T}{i}) i$
125	98 124	syl5eqr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - i π = (\frac{T}{i}) i$
126	62 64 66	divcan1d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{T}{i}) i = T$
127	126	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to (\frac{T}{i}) i = T$
128	125 127	eqtr2d	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to T = - i π$
129	128	orcd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to (T = - i π \lor T = i π)$
130		df-2	$⊢ 2 = 1 + 1$
131	130	negeqi	$⊢ - 2 = - (1 + 1)$
132		negdi2	$⊢ (1 \in ℂ \land 1 \in ℂ) \to - (1 + 1) = - 1 - 1$
133	35 35 132	mp2an	$⊢ - (1 + 1) = - 1 - 1$
134	131 133	eqtri	$⊢ - 2 = - 1 - 1$
135	11	simpld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - 2 < N$
136	134 135	eqbrtrrid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - 1 - 1 < N$
137		neg1z	$⊢ - 1 \in ℤ$
138		zlem1lt	$⊢ (- 1 \in ℤ \land N \in ℤ) \to (- 1 \leq N \leftrightarrow - 1 - 1 < N)$
139	137 16 138	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- 1 \leq N \leftrightarrow - 1 - 1 < N)$
140	136 139	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - 1 \leq N$
141		neg1rr	$⊢ - 1 \in ℝ$
142		leloe	$⊢ (- 1 \in ℝ \land N \in ℝ) \to (- 1 \leq N \leftrightarrow (- 1 < N \lor - 1 = N))$
143	141 28 142	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- 1 \leq N \leftrightarrow (- 1 < N \lor - 1 = N))$
144	140 143	mpbid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- 1 < N \lor - 1 = N)$
145	94 129 144	mpjaodan	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (T = - i π \lor T = i π)$
146	2	ovexi	$⊢ T \in V$
147	146	elpr	$⊢ T \in \{- i π, i π\} \leftrightarrow (T = - i π \lor T = i π)$
148	145 147	sylibr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to T \in \{- i π, i π\}$

Metamath Proof Explorer

Theorem ang180lem3

Proof