ang180lem2

Description: Lemma for ang180 . Show that the revolution number N is strictly between -u 2 and 1 . Both bounds are established by iterating using the bounds on the imaginary part of the logarithm, logimcl , but the resulting bound gives only N <_ 1 for the upper bound. The case N = 1 is not ruled out here, but it is in some sense an "edge case" that can only happen under very specific conditions; in particular we show that all the angle arguments A , 1 / ( 1 - A ) , ( A - 1 ) / A must lie on the negative real axis, which is a contradiction because clearly if A is negative then the other two are positive real. (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	ang180lem2	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- 2 < N \land N < 1)$

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		1re	$⊢ 1 \in ℝ$
6	5	rehalfcli	$⊢ \frac{1}{2} \in ℝ$
7	6	recni	$⊢ \frac{1}{2} \in ℂ$
8	4 7	negsubdii	$⊢ - (2 - (\frac{1}{2})) = - 2 + (\frac{1}{2})$
9		4div2e2	$⊢ \frac{4}{2} = 2$
10	9	oveq1i	$⊢ (\frac{4}{2}) - (\frac{1}{2}) = 2 - (\frac{1}{2})$
11		4cn	$⊢ 4 \in ℂ$
12		ax-1cn	$⊢ 1 \in ℂ$
13		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
14		divsubdir	$⊢ (4 \in ℂ \land 1 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{4 - 1}{2} = (\frac{4}{2}) - (\frac{1}{2})$
15	11 12 13 14	mp3an	$⊢ \frac{4 - 1}{2} = (\frac{4}{2}) - (\frac{1}{2})$
16		4m1e3	$⊢ 4 - 1 = 3$
17	16	oveq1i	$⊢ \frac{4 - 1}{2} = \frac{3}{2}$
18	15 17	eqtr3i	$⊢ (\frac{4}{2}) - (\frac{1}{2}) = \frac{3}{2}$
19	10 18	eqtr3i	$⊢ 2 - (\frac{1}{2}) = \frac{3}{2}$
20	19	negeqi	$⊢ - (2 - (\frac{1}{2})) = - \frac{3}{2}$
21	8 20	eqtr3i	$⊢ - 2 + (\frac{1}{2}) = - \frac{3}{2}$
22		3re	$⊢ 3 \in ℝ$
23	22	rehalfcli	$⊢ \frac{3}{2} \in ℝ$
24	23	recni	$⊢ \frac{3}{2} \in ℂ$
25		picn	$⊢ π \in ℂ$
26	24 4 25	mulassi	$⊢ (\frac{3}{2}) \cdot 2 π = (\frac{3}{2}) 2 π$
27		3cn	$⊢ 3 \in ℂ$
28		2ne0	$⊢ 2 \neq 0$
29	27 4 28	divcan1i	$⊢ (\frac{3}{2}) \cdot 2 = 3$
30	29	oveq1i	$⊢ (\frac{3}{2}) \cdot 2 π = 3 π$
31	26 30	eqtr3i	$⊢ (\frac{3}{2}) 2 π = 3 π$
32	31	negeqi	$⊢ - (\frac{3}{2}) 2 π = - 3 π$
33		2re	$⊢ 2 \in ℝ$
34		pire	$⊢ π \in ℝ$
35	33 34	remulcli	$⊢ 2 π \in ℝ$
36	35	recni	$⊢ 2 π \in ℂ$
37	24 36	mulneg1i	$⊢ (- \frac{3}{2}) 2 π = - (\frac{3}{2}) 2 π$
38	27 25	mulneg2i	$⊢ 3 (- π) = - 3 π$
39	32 37 38	3eqtr4i	$⊢ (- \frac{3}{2}) 2 π = 3 (- π)$
40	34	renegcli	$⊢ - π \in ℝ$
41	33 40	remulcli	$⊢ 2 (- π) \in ℝ$
42	41	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 (- π) \in ℝ$
43	40	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - π \in ℝ$
44		simp1	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \in ℂ$
45		subcl	$⊢ (1 \in ℂ \land A \in ℂ) \to 1 - A \in ℂ$
46	12 44 45	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 - A \in ℂ$
47		simp3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \neq 1$
48	47	necomd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 \neq A$
49		subeq0	$⊢ (1 \in ℂ \land A \in ℂ) \to (1 - A = 0 \leftrightarrow 1 = A)$
50	12 44 49	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (1 - A = 0 \leftrightarrow 1 = A)$
51	50	necon3bid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (1 - A \neq 0 \leftrightarrow 1 \neq A)$
52	48 51	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 - A \neq 0$
53	46 52	reccld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{1}{1 - A} \in ℂ$
54	46 52	recne0d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{1}{1 - A} \neq 0$
55	53 54	logcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{1}{1 - A}) \in ℂ$
56		subcl	$⊢ (A \in ℂ \land 1 \in ℂ) \to A - 1 \in ℂ$
57	44 12 56	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A - 1 \in ℂ$
58		simp2	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \neq 0$
59	57 44 58	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{A - 1}{A} \in ℂ$
60		subeq0	$⊢ (A \in ℂ \land 1 \in ℂ) \to (A - 1 = 0 \leftrightarrow A = 1)$
61	44 12 60	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (A - 1 = 0 \leftrightarrow A = 1)$
62	61	necon3bid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (A - 1 \neq 0 \leftrightarrow A \neq 1)$
63	47 62	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A - 1 \neq 0$
64	57 44 63 58	divne0d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{A - 1}{A} \neq 0$
65	59 64	logcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{A - 1}{A}) \in ℂ$
66	55 65	addcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) \in ℂ$
67	66	imcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) \in ℝ$
68		logcl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ℂ$
69	68	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log A \in ℂ$
70	69	imcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log A) \in ℝ$
71	55	imcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log (\frac{1}{1 - A})) \in ℝ$
72	65	imcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log (\frac{A - 1}{A})) \in ℝ$
73	53 54	logimcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- π < ℑ (\log (\frac{1}{1 - A})) \land ℑ (\log (\frac{1}{1 - A})) \leq π)$
74	73	simpld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - π < ℑ (\log (\frac{1}{1 - A}))$
75	59 64	logimcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- π < ℑ (\log (\frac{A - 1}{A})) \land ℑ (\log (\frac{A - 1}{A})) \leq π)$
76	75	simpld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - π < ℑ (\log (\frac{A - 1}{A}))$
77	43 43 71 72 74 76	lt2addd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - π + (- π) < ℑ (\log (\frac{1}{1 - A})) + ℑ (\log (\frac{A - 1}{A}))$
78		negpicn	$⊢ - π \in ℂ$
79	78	2timesi	$⊢ 2 (- π) = - π + (- π)$
80	79	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 (- π) = - π + (- π)$
81	55 65	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}))$
82	77 80 81	3brtr4d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 (- π) < ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}))$
83		logimcl	$⊢ (A \in ℂ \land A \neq 0) \to (- π < ℑ (\log A) \land ℑ (\log A) \leq π)$
84	83	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- π < ℑ (\log A) \land ℑ (\log A) \leq π)$
85	84	simpld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - π < ℑ (\log A)$
86	42 43 67 70 82 85	lt2addd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 (- π) + (- π) < ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) + ℑ (\log A)$
87		df-3	$⊢ 3 = 2 + 1$
88	87	oveq1i	$⊢ 3 (- π) = (2 + 1) (- π)$
89	4 12 78	adddiri	$⊢ (2 + 1) (- π) = 2 (- π) + 1 (- π)$
90	78	mullidi	$⊢ 1 (- π) = - π$
91	90	oveq2i	$⊢ 2 (- π) + 1 (- π) = 2 (- π) + (- π)$
92	88 89 91	3eqtri	$⊢ 3 (- π) = 2 (- π) + (- π)$
93	92	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 3 (- π) = 2 (- π) + (- π)$
94	2	fveq2i	$⊢ ℑ (T) = ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A)$
95	66 69	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)$
96	94 95	eqtrid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (T) = ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) + ℑ (\log A)$
97	86 93 96	3brtr4d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 3 (- π) < ℑ (T)$
98	66 69	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 ℂ$
99	2 98	eqeltrid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to T \in ℂ$
100		imval	$⊢ T \in ℂ \to ℑ (T) = ℜ (\frac{T}{i})$
101	99 100	syl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (T) = ℜ (\frac{T}{i})$
102	1 2 3	ang180lem1	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (N \in ℤ \land \frac{T}{i} \in ℝ)$
103	102	simprd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{T}{i} \in ℝ$
104	103	rered	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℜ (\frac{T}{i}) = \frac{T}{i}$
105	101 104	eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (T) = \frac{T}{i}$
106	97 105	breqtrd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 3 (- π) < \frac{T}{i}$
107	39 106	eqbrtrid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- \frac{3}{2}) 2 π < \frac{T}{i}$
108	23	renegcli	$⊢ - \frac{3}{2} \in ℝ$
109	108	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - \frac{3}{2} \in ℝ$
110	35	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π \in ℝ$
111		2pos	$⊢ 0 < 2$
112		pipos	$⊢ 0 < π$
113	33 34 111 112	mulgt0ii	$⊢ 0 < 2 π$
114	113	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 0 < 2 π$
115		ltmuldiv	$⊢ (- \frac{3}{2} \in ℝ \land \frac{T}{i} \in ℝ \land (2 π \in ℝ \land 0 < 2 π)) \to ((- \frac{3}{2}) 2 π < \frac{T}{i} \leftrightarrow - \frac{3}{2} < \frac{\frac{T}{i}}{2 π})$
116	109 103 110 114 115	syl112anc	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ((- \frac{3}{2}) 2 π < \frac{T}{i} \leftrightarrow - \frac{3}{2} < \frac{\frac{T}{i}}{2 π})$
117	107 116	mpbid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - \frac{3}{2} < \frac{\frac{T}{i}}{2 π}$
118	21 117	eqbrtrid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - 2 + (\frac{1}{2}) < \frac{\frac{T}{i}}{2 π}$
119	33	renegcli	$⊢ - 2 \in ℝ$
120	119	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - 2 \in ℝ$
121	6	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{1}{2} \in ℝ$
122	35 113	gt0ne0ii	$⊢ 2 π \neq 0$
123	122	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π \neq 0$
124	103 110 123	redivcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{\frac{T}{i}}{2 π} \in ℝ$
125	120 121 124	ltaddsubd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- 2 + (\frac{1}{2}) < \frac{\frac{T}{i}}{2 π} \leftrightarrow - 2 < (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}))$
126	118 125	mpbid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - 2 < (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2})$
127	126 3	breqtrrdi	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - 2 < N$
128	34	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to π \in ℝ$
129	73	simprd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log (\frac{1}{1 - A})) \leq π$
130	75	simprd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log (\frac{A - 1}{A})) \leq π$
131	71 72 128 128 129 130	le2addd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log (\frac{1}{1 - A})) + ℑ (\log (\frac{A - 1}{A})) \leq π + π$
132	25	2timesi	$⊢ 2 π = π + π$
133	132	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π = π + π$
134	131 81 133	3brtr4d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) \leq 2 π$
135	84	simprd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log A) \leq π$
136	67 70 110 128 134 135	le2addd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) + ℑ (\log A) \leq 2 π + π$
137	105 96	eqtr3d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{T}{i} = ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) + ℑ (\log A)$
138	87	oveq1i	$⊢ 3 π = (2 + 1) π$
139	4 12 25	adddiri	$⊢ (2 + 1) π = 2 π + 1 π$
140	25	mullidi	$⊢ 1 π = π$
141	140	oveq2i	$⊢ 2 π + 1 π = 2 π + π$
142	138 139 141	3eqtri	$⊢ 3 π = 2 π + π$
143	142	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 3 π = 2 π + π$
144	136 137 143	3brtr4d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{T}{i} \leq 3 π$
145	36	subid1i	$⊢ 2 π - 0 = 2 π$
146	145 122	eqnetri	$⊢ 2 π - 0 \neq 0$
147		negsub	$⊢ (1 \in ℂ \land A \in ℂ) \to 1 + (- A) = 1 - A$
148	12 44 147	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 + (- A) = 1 - A$
149	148	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to 1 + (- A) = 1 - A$
150		1rp	$⊢ 1 \in ℝ^{+}$
151	143 137	oveq12d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 3 π - (\frac{T}{i}) = 2 π + π - (ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) + ℑ (\log A))$
152	36	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π \in ℂ$
153	25	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to π \in ℂ$
154	67	recnd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) \in ℂ$
155	70	recnd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ℑ (\log A) \in ℂ$
156	152 153 154 155	addsub4d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π + π - (ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) + ℑ (\log A)) = (2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}))) + π - ℑ (\log A)$
157	151 156	eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 3 π - (\frac{T}{i}) = (2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}))) + π - ℑ (\log A)$
158	157	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to 3 π - (\frac{T}{i}) = (2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}))) + π - ℑ (\log A)$
159	22 34	remulcli	$⊢ 3 π \in ℝ$
160	159	recni	$⊢ 3 π \in ℂ$
161		ax-icn	$⊢ i \in ℂ$
162	161	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to i \in ℂ$
163		ine0	$⊢ i \neq 0$
164	163	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to i \neq 0$
165	99 162 164	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{T}{i} \in ℂ$
166		subeq0	$⊢ (3 π \in ℂ \land \frac{T}{i} \in ℂ) \to (3 π - (\frac{T}{i}) = 0 \leftrightarrow 3 π = \frac{T}{i})$
167	160 165 166	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (3 π - (\frac{T}{i}) = 0 \leftrightarrow 3 π = \frac{T}{i})$
168	167	biimpar	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to 3 π - (\frac{T}{i}) = 0$
169	158 168	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to (2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}))) + π - ℑ (\log A) = 0$
170		resubcl	$⊢ (2 π \in ℝ \land ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) \in ℝ) \to 2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) \in ℝ$
171	35 67 170	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) \in ℝ$
172		subge0	$⊢ (2 π \in ℝ \land ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) \in ℝ) \to (0 \leq 2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) \leftrightarrow ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) \leq 2 π)$
173	35 67 172	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (0 \leq 2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) \leftrightarrow ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) \leq 2 π)$
174	134 173	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 0 \leq 2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}))$
175		resubcl	$⊢ (π \in ℝ \land ℑ (\log A) \in ℝ) \to π - ℑ (\log A) \in ℝ$
176	34 70 175	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to π - ℑ (\log A) \in ℝ$
177		subge0	$⊢ (π \in ℝ \land ℑ (\log A) \in ℝ) \to (0 \leq π - ℑ (\log A) \leftrightarrow ℑ (\log A) \leq π)$
178	34 70 177	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (0 \leq π - ℑ (\log A) \leftrightarrow ℑ (\log A) \leq π)$
179	135 178	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 0 \leq π - ℑ (\log A)$
180		add20	$⊢ ((2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) \in ℝ \land 0 \leq 2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}))) \land (π - ℑ (\log A) \in ℝ \land 0 \leq π - ℑ (\log A))) \to ((2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}))) + π - ℑ (\log A) = 0 \leftrightarrow (2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) = 0 \land π - ℑ (\log A) = 0))$
181	171 174 176 179 180	syl22anc	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ((2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}))) + π - ℑ (\log A) = 0 \leftrightarrow (2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) = 0 \land π - ℑ (\log A) = 0))$
182	181	biimpa	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land (2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}))) + π - ℑ (\log A) = 0) \to (2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) = 0 \land π - ℑ (\log A) = 0)$
183	169 182	syldan	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to (2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) = 0 \land π - ℑ (\log A) = 0)$
184	183	simprd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to π - ℑ (\log A) = 0$
185	155	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to ℑ (\log A) \in ℂ$
186		subeq0	$⊢ (π \in ℂ \land ℑ (\log A) \in ℂ) \to (π - ℑ (\log A) = 0 \leftrightarrow π = ℑ (\log A))$
187	25 185 186	sylancr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to (π - ℑ (\log A) = 0 \leftrightarrow π = ℑ (\log A))$
188	184 187	mpbid	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to π = ℑ (\log A)$
189	188	eqcomd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to ℑ (\log A) = π$
190		lognegb	$⊢ (A \in ℂ \land A \neq 0) \to (- A \in ℝ^{+} \leftrightarrow ℑ (\log A) = π)$
191	190	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- A \in ℝ^{+} \leftrightarrow ℑ (\log A) = π)$
192	191	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to (- A \in ℝ^{+} \leftrightarrow ℑ (\log A) = π)$
193	189 192	mpbird	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to - A \in ℝ^{+}$
194		rpaddcl	$⊢ (1 \in ℝ^{+} \land - A \in ℝ^{+}) \to 1 + (- A) \in ℝ^{+}$
195	150 193 194	sylancr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to 1 + (- A) \in ℝ^{+}$
196	149 195	eqeltrrd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to 1 - A \in ℝ^{+}$
197	196	rpreccld	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to \frac{1}{1 - A} \in ℝ^{+}$
198	197	relogcld	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to \log (\frac{1}{1 - A}) \in ℝ$
199		negsubdi2	$⊢ (A \in ℂ \land 1 \in ℂ) \to - (A - 1) = 1 - A$
200	44 12 199	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - (A - 1) = 1 - A$
201	200	oveq1d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{- (A - 1)}{- A} = \frac{1 - A}{- A}$
202	57 44 58	div2negd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{- (A - 1)}{- A} = \frac{A - 1}{A}$
203	201 202	eqtr3d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{1 - A}{- A} = \frac{A - 1}{A}$
204	203	adantr	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to \frac{1 - A}{- A} = \frac{A - 1}{A}$
205	196 193	rpdivcld	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to \frac{1 - A}{- A} \in ℝ^{+}$
206	204 205	eqeltrrd	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to \frac{A - 1}{A} \in ℝ^{+}$
207	206	relogcld	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to \log (\frac{A - 1}{A}) \in ℝ$
208	198 207	readdcld	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) \in ℝ$
209	208	reim0d	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) = 0$
210	209	oveq2d	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to 2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) = 2 π - 0$
211	183	simpld	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to 2 π - ℑ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})) = 0$
212	210 211	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0 \land A \neq 1) \land 3 π = \frac{T}{i}) \to 2 π - 0 = 0$
213	212	ex	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (3 π = \frac{T}{i} \to 2 π - 0 = 0)$
214	213	necon3d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (2 π - 0 \neq 0 \to 3 π \neq \frac{T}{i})$
215	146 214	mpi	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 3 π \neq \frac{T}{i}$
216		ltlen	$⊢ (\frac{T}{i} \in ℝ \land 3 π \in ℝ) \to (\frac{T}{i} < 3 π \leftrightarrow (\frac{T}{i} \leq 3 π \land 3 π \neq \frac{T}{i}))$
217	103 159 216	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{T}{i} < 3 π \leftrightarrow (\frac{T}{i} \leq 3 π \land 3 π \neq \frac{T}{i}))$
218	144 215 217	mpbir2and	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{T}{i} < 3 π$
219	218 31	breqtrrdi	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{T}{i} < (\frac{3}{2}) 2 π$
220	23	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{3}{2} \in ℝ$
221		ltdivmul2	$⊢ (\frac{T}{i} \in ℝ \land \frac{3}{2} \in ℝ \land (2 π \in ℝ \land 0 < 2 π)) \to (\frac{\frac{T}{i}}{2 π} < \frac{3}{2} \leftrightarrow \frac{T}{i} < (\frac{3}{2}) 2 π)$
222	103 220 110 114 221	syl112anc	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{\frac{T}{i}}{2 π} < \frac{3}{2} \leftrightarrow \frac{T}{i} < (\frac{3}{2}) 2 π)$
223	219 222	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{\frac{T}{i}}{2 π} < \frac{3}{2}$
224	87	oveq1i	$⊢ \frac{3}{2} = \frac{2 + 1}{2}$
225	4 12 4 28	divdiri	$⊢ \frac{2 + 1}{2} = (\frac{2}{2}) + (\frac{1}{2})$
226		2div2e1	$⊢ \frac{2}{2} = 1$
227	226	oveq1i	$⊢ (\frac{2}{2}) + (\frac{1}{2}) = 1 + (\frac{1}{2})$
228	224 225 227	3eqtri	$⊢ \frac{3}{2} = 1 + (\frac{1}{2})$
229	223 228	breqtrdi	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{\frac{T}{i}}{2 π} < 1 + (\frac{1}{2})$
230	5	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 \in ℝ$
231	124 121 230	ltsubaddd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to ((\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}) < 1 \leftrightarrow \frac{\frac{T}{i}}{2 π} < 1 + (\frac{1}{2}))$
232	229 231	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}) < 1$
233	3 232	eqbrtrid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N < 1$
234	127 233	jca	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (- 2 < N \land N < 1)$

Metamath Proof Explorer

Theorem ang180lem2

Proof