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		2picn	$⊢ 2 π \in ℂ$
62	61	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π \in ℂ$
63		2cn	$⊢ 2 \in ℂ$
64		picn	$⊢ π \in ℂ$
65		2ne0	$⊢ 2 \neq 0$
66		pine0	$⊢ π \neq 0$
67	63 64 65 66	mulne0i	$⊢ 2 π \neq 0$
68	67	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π \neq 0$
69	60 62 68	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{\frac{T}{i}}{2 π} \in ℂ$
70	69	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{\frac{T}{i}}{2 π} \in ℂ$
71		halfcn	$⊢ \frac{1}{2} \in ℂ$
72		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})$
73	70 71 72	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})$
74	27 73	mpbid	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{\frac{T}{i}}{2 π} = \frac{1}{2}$
75	60	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{T}{i} \in ℂ$
76	61	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to 2 π \in ℂ$
77	71	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{1}{2} \in ℂ$
78	67	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to 2 π \neq 0$
79	75 76 77 78	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})$
80	74 79	mpbid	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to 2 π (\frac{1}{2}) = \frac{T}{i}$
81	61 63 65	divreci	$⊢ \frac{2 π}{2} = 2 π (\frac{1}{2})$
82	64 63 65	divcan3i	$⊢ \frac{2 π}{2} = π$
83	81 82	eqtr3i	$⊢ 2 π (\frac{1}{2}) = π$
84	80 83	eqtr3di	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to \frac{T}{i} = π$
85	55	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to T \in ℂ$
86	56	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to i \in ℂ$
87	64	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to π \in ℂ$
88	58	a1i	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to i \neq 0$
89	85 86 87 88	divmuld	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to (\frac{T}{i} = π \leftrightarrow i π = T)$
90	84 89	mpbid	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to i π = T$
91	90	eqcomd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to T = i π$
92	91	olcd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 < N) \to (T = - i π \lor T = i π)$
93	64 56	mulneg1i	$⊢ (- π) i = - π i$
94	64 56	mulcomi	$⊢ π i = i π$
95	94	negeqi	$⊢ - π i = - i π$
96	93 95	eqtri	$⊢ (- π) i = - i π$
97	71 61	mulneg1i	$⊢ (- \frac{1}{2}) 2 π = - (\frac{1}{2}) 2 π$
98	28 63 65	divcan1i	$⊢ (\frac{1}{2}) \cdot 2 = 1$
99	98	oveq1i	$⊢ (\frac{1}{2}) \cdot 2 π = 1 π$
100	71 63 64	mulassi	$⊢ (\frac{1}{2}) \cdot 2 π = (\frac{1}{2}) 2 π$
101	64	mullidi	$⊢ 1 π = π$
102	99 100 101	3eqtr3i	$⊢ (\frac{1}{2}) 2 π = π$
103	102	negeqi	$⊢ - (\frac{1}{2}) 2 π = - π$
104	97 103	eqtri	$⊢ (- \frac{1}{2}) 2 π = - π$
105	28 71	negsubdii	$⊢ - (1 - (\frac{1}{2})) = - 1 + (\frac{1}{2})$
106		1mhlfehlf	$⊢ 1 - (\frac{1}{2}) = \frac{1}{2}$
107	106	negeqi	$⊢ - (1 - (\frac{1}{2})) = - \frac{1}{2}$
108	105 107	eqtr3i	$⊢ - 1 + (\frac{1}{2}) = - \frac{1}{2}$
109		simpr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - 1 = N$
110	109 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})$
111	110	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})$
112	108 111	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})$
113		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 π}$
114	69 71 113	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 π}$
115	114	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 π}$
116	112 115	eqtrd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - \frac{1}{2} = \frac{\frac{T}{i}}{2 π}$
117	116	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 π$
118	104 117	eqtr3id	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - π = (\frac{\frac{T}{i}}{2 π}) 2 π$
119	60 62 68	divcan1d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{\frac{T}{i}}{2 π}) 2 π = \frac{T}{i}$
120	119	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to (\frac{\frac{T}{i}}{2 π}) 2 π = \frac{T}{i}$
121	118 120	eqtrd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - π = \frac{T}{i}$
122	121	oveq1d	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to (- π) i = (\frac{T}{i}) i$
123	96 122	eqtr3id	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to - i π = (\frac{T}{i}) i$
124	55 57 59	divcan1d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{T}{i}) i = T$
125	124	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to (\frac{T}{i}) i = T$
126	123 125	eqtr2d	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to T = - i π$
127	126	orcd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land - 1 = N) \to (T = - i π \lor T = i π)$
128		df-2	$⊢ 2 = 1 + 1$
129	128	negeqi	$⊢ - 2 = - (1 + 1)$
130		negdi2	$⊢ (1 \in ℂ \land 1 \in ℂ) \to - (1 + 1) = - 1 - 1$
131	28 28 130	mp2an	$⊢ - (1 + 1) = - 1 - 1$
132	129 131	eqtri	$⊢ - 2 = - 1 - 1$
133	4	simpld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - 2 < N$
134	132 133	eqbrtrrid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - 1 - 1 < N$
135		neg1z	$⊢ - 1 \in ℤ$
136		zlem1lt	$⊢ (- 1 \in ℤ \land N \in ℤ) \to (- 1 \leq N \leftrightarrow - 1 - 1 < N)$
137	135 9 136	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- 1 \leq N \leftrightarrow - 1 - 1 < N)$
138	134 137	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - 1 \leq N$
139		neg1rr	$⊢ - 1 \in ℝ$
140		leloe	$⊢ (- 1 \in ℝ \land N \in ℝ) \to (- 1 \leq N \leftrightarrow (- 1 < N \lor - 1 = N))$
141	139 21 140	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- 1 \leq N \leftrightarrow (- 1 < N \lor - 1 = N))$
142	138 141	mpbid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- 1 < N \lor - 1 = N)$
143	92 127 142	mpjaodan	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (T = - i π \lor T = i π)$
144	2	ovexi	$⊢ T \in V$
145	144	elpr	$⊢ T \in \{- i π, i π\} \leftrightarrow (T = - i π \lor T = i π)$
146	143 145	sylibr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to T \in \{- i π, i π\}$

Metamath Proof Explorer

Theorem ang180lem3

Proof