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	1 2 3	ang180lem2	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- 2 < N \land N < 1)$
5	4	simprd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N < 1$
6		1e0p1	$⊢ 1 = 0 + 1$
7	5 6	breqtrdi	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N < 0 + 1$
8	1 2 3	ang180lem1	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (N \in ℤ \land \frac{T}{i} \in ℝ)$
9	8	simpld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N \in ℤ$
10		0z	$⊢ 0 \in ℤ$
11		zleltp1	$⊢ (N \in ℤ \land 0 \in ℤ) \to (N \leq 0 \leftrightarrow N < 0 + 1)$
12	9 10 11	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (N \leq 0 \leftrightarrow N < 0 + 1)$
13	7 12	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N \leq 0$
14	13	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to N \leq 0$
15		zlem1lt	$⊢ (0 \in ℤ \land N \in ℤ) \to (0 \leq N \leftrightarrow 0 - 1 < N)$
16	10 9 15	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (0 \leq N \leftrightarrow 0 - 1 < N)$
17		df-neg	$⊢ - 1 = 0 - 1$
18	17	breq1i	$⊢ - 1 < N \leftrightarrow 0 - 1 < N$
19	16 18	bitr4di	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (0 \leq N \leftrightarrow - 1 < N)$
20	19	biimpar	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to 0 \leq N$
21	9	zred	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N \in ℝ$
22	21	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to N \in ℝ$
23		0re	$⊢ 0 \in ℝ$
24		letri3	$⊢ (N \in ℝ \land 0 \in ℝ) \to (N = 0 \leftrightarrow (N \leq 0 \land 0 \leq N))$
25	22 23 24	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))$
26	14 20 25	mpbir2and	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to N = 0$
27	3 26	eqtr3id	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}) = 0$
28		ax-1cn	$⊢ 1 \in ℂ$
29		simp1	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \in ℂ$
30		subcl	$⊢ (1 \in ℂ \land A \in ℂ) \to 1 - A \in ℂ$
31	28 29 30	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 - A \in ℂ$
32		simp3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \neq 1$
33	32	necomd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 \neq A$
34		subeq0	$⊢ (1 \in ℂ \land A \in ℂ) \to (1 - A = 0 \leftrightarrow 1 = A)$
35	28 29 34	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (1 - A = 0 \leftrightarrow 1 = A)$
36	35	necon3bid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (1 - A \neq 0 \leftrightarrow 1 \neq A)$
37	33 36	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 - A \neq 0$
38	31 37	reccld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{1}{1 - A} \in ℂ$
39	31 37	recne0d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{1}{1 - A} \neq 0$
40	38 39	logcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{1}{1 - A}) \in ℂ$
41		subcl	$⊢ (A \in ℂ \land 1 \in ℂ) \to A - 1 \in ℂ$
42	29 28 41	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A - 1 \in ℂ$
43		simp2	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \neq 0$
44	42 29 43	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{A - 1}{A} \in ℂ$
45		subeq0	$⊢ (A \in ℂ \land 1 \in ℂ) \to (A - 1 = 0 \leftrightarrow A = 1)$
46	29 28 45	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (A - 1 = 0 \leftrightarrow A = 1)$
47	46	necon3bid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (A - 1 \neq 0 \leftrightarrow A \neq 1)$
48	32 47	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A - 1 \neq 0$
49	42 29 48 43	divne0d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{A - 1}{A} \neq 0$
50	44 49	logcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{A - 1}{A}) \in ℂ$
51	40 50	addcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) \in ℂ$
52		logcl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ℂ$
53	52	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log A \in ℂ$
54	51 53	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 ℂ$
55	2 54	eqeltrid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to T \in ℂ$
56		ax-icn	$⊢ i \in ℂ$
57	56	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to i \in ℂ$
58		ine0	$⊢ i \neq 0$
59	58	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to i \neq 0$
60	55 57 59	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{T}{i} \in ℂ$
61		2cn	$⊢ 2 \in ℂ$
62		picn	$⊢ π \in ℂ$
63	61 62	mulcli	$⊢ 2 π \in ℂ$
64	63	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π \in ℂ$
65		2ne0	$⊢ 2 \neq 0$
66		pire	$⊢ π \in ℝ$
67		pipos	$⊢ 0 < π$
68	66 67	gt0ne0ii	$⊢ π \neq 0$
69	61 62 65 68	mulne0i	$⊢ 2 π \neq 0$
70	69	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π \neq 0$
71	60 64 70	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{\frac{T}{i}}{2 π} \in ℂ$
72	71	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{\frac{T}{i}}{2 π} \in ℂ$
73		halfcn	$⊢ \frac{1}{2} \in ℂ$
74		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})$
75	72 73 74	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})$
76	27 75	mpbid	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{\frac{T}{i}}{2 π} = \frac{1}{2}$
77	60	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{T}{i} \in ℂ$
78	63	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to 2 π \in ℂ$
79	73	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{1}{2} \in ℂ$
80	69	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to 2 π \neq 0$
81	77 78 79 80	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})$
82	76 81	mpbid	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to 2 π (\frac{1}{2}) = \frac{T}{i}$
83	63 61 65	divreci	$⊢ \frac{2 π}{2} = 2 π (\frac{1}{2})$
84	62 61 65	divcan3i	$⊢ \frac{2 π}{2} = π$
85	83 84	eqtr3i	$⊢ 2 π (\frac{1}{2}) = π$
86	82 85	eqtr3di	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{T}{i} = π$
87	55	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to T \in ℂ$
88	56	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to i \in ℂ$
89	62	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to π \in ℂ$
90	58	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	62 56	mulneg1i	$⊢ (- π) i = - π i$
96	62 56	mulcomi	$⊢ π i = i π$
97	96	negeqi	$⊢ - π i = - i π$
98	95 97	eqtri	$⊢ (- π) i = - i π$
99	73 63	mulneg1i	$⊢ (- \frac{1}{2}) 2 π = - (\frac{1}{2}) 2 π$
100	28 61 65	divcan1i	$⊢ (\frac{1}{2}) \cdot 2 = 1$
101	100	oveq1i	$⊢ (\frac{1}{2}) \cdot 2 π = 1 π$
102	73 61 62	mulassi	$⊢ (\frac{1}{2}) \cdot 2 π = (\frac{1}{2}) 2 π$
103	62	mullidi	$⊢ 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	28 73	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	eqtr3id	$⊢ ((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	71 73 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	eqtr3id	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - π = (\frac{\frac{T}{i}}{2 π}) 2 π$
121	60 64 70	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	eqtr3id	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - i π = (\frac{T}{i}) i$
126	55 57 59	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	28 28 132	mp2an	$⊢ - (1 + 1) = - 1 - 1$
134	131 133	eqtri	$⊢ - 2 = - 1 - 1$
135	4	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 9 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 21 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