ang180lem1

Description: Lemma for ang180 . Show that the "revolution number" N is an integer, using efeq1 to show that since the product of the three arguments A , 1 / ( 1 - A ) , ( A - 1 ) / A is -u 1 , the sum of the logarithms must be an integer multiple of 2pi i away from _pi _i = log ( -u 1 ) . (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	ang180lem1	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (N \in ℤ \land \frac{T}{i} \in ℝ)$

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		picn	$⊢ π \in ℂ$
5		2re	$⊢ 2 \in ℝ$
6		pire	$⊢ π \in ℝ$
7	5 6	remulcli	$⊢ 2 π \in ℝ$
8	7	recni	$⊢ 2 π \in ℂ$
9		2pos	$⊢ 0 < 2$
10		pipos	$⊢ 0 < π$
11	5 6 9 10	mulgt0ii	$⊢ 0 < 2 π$
12	7 11	gt0ne0ii	$⊢ 2 π \neq 0$
13	8 12	pm3.2i	$⊢ (2 π \in ℂ \land 2 π \neq 0)$
14		ax-icn	$⊢ i \in ℂ$
15		ine0	$⊢ i \neq 0$
16	14 15	pm3.2i	$⊢ (i \in ℂ \land i \neq 0)$
17		divcan5	$⊢ (π \in ℂ \land (2 π \in ℂ \land 2 π \neq 0) \land (i \in ℂ \land i \neq 0)) \to \frac{i π}{i 2 π} = \frac{π}{2 π}$
18	4 13 16 17	mp3an	$⊢ \frac{i π}{i 2 π} = \frac{π}{2 π}$
19	6 10	gt0ne0ii	$⊢ π \neq 0$
20		recdiv	$⊢ ((2 π \in ℂ \land 2 π \neq 0) \land (π \in ℂ \land π \neq 0)) \to \frac{1}{\frac{2 π}{π}} = \frac{π}{2 π}$
21	8 12 4 19 20	mp4an	$⊢ \frac{1}{\frac{2 π}{π}} = \frac{π}{2 π}$
22	5	recni	$⊢ 2 \in ℂ$
23	22 4 19	divcan4i	$⊢ \frac{2 π}{π} = 2$
24	23	oveq2i	$⊢ \frac{1}{\frac{2 π}{π}} = \frac{1}{2}$
25	18 21 24	3eqtr2i	$⊢ \frac{i π}{i 2 π} = \frac{1}{2}$
26	25	oveq2i	$⊢ (\frac{T}{i 2 π}) - (\frac{i π}{i 2 π}) = (\frac{T}{i 2 π}) - (\frac{1}{2})$
27		ax-1cn	$⊢ 1 \in ℂ$
28		simp1	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \in ℂ$
29		subcl	$⊢ (1 \in ℂ \land A \in ℂ) \to 1 - A \in ℂ$
30	27 28 29	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 - A \in ℂ$
31		simp3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \neq 1$
32	31	necomd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 \neq A$
33		subeq0	$⊢ (1 \in ℂ \land A \in ℂ) \to (1 - A = 0 \leftrightarrow 1 = A)$
34	27 28 33	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (1 - A = 0 \leftrightarrow 1 = A)$
35	34	necon3bid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (1 - A \neq 0 \leftrightarrow 1 \neq A)$
36	32 35	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 - A \neq 0$
37	30 36	reccld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{1}{1 - A} \in ℂ$
38	30 36	recne0d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{1}{1 - A} \neq 0$
39	37 38	logcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{1}{1 - A}) \in ℂ$
40		subcl	$⊢ (A \in ℂ \land 1 \in ℂ) \to A - 1 \in ℂ$
41	28 27 40	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A - 1 \in ℂ$
42		simp2	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \neq 0$
43	41 28 42	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{A - 1}{A} \in ℂ$
44		subeq0	$⊢ (A \in ℂ \land 1 \in ℂ) \to (A - 1 = 0 \leftrightarrow A = 1)$
45	28 27 44	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (A - 1 = 0 \leftrightarrow A = 1)$
46	45	necon3bid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (A - 1 \neq 0 \leftrightarrow A \neq 1)$
47	31 46	mpbird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A - 1 \neq 0$
48	41 28 47 42	divne0d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{A - 1}{A} \neq 0$
49	43 48	logcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{A - 1}{A}) \in ℂ$
50	39 49	addcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) \in ℂ$
51	28 42	logcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log A \in ℂ$
52	50 51	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 ℂ$
53	2 52	eqeltrid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to T \in ℂ$
54	14 4	mulcli	$⊢ i π \in ℂ$
55	54	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to i π \in ℂ$
56	14 8	mulcli	$⊢ i 2 π \in ℂ$
57	56	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to i 2 π \in ℂ$
58	14 8 15 12	mulne0i	$⊢ i 2 π \neq 0$
59	58	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to i 2 π \neq 0$
60	53 55 57 59	divsubdird	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{T - i π}{i 2 π} = (\frac{T}{i 2 π}) - (\frac{i π}{i 2 π})$
61	16	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (i \in ℂ \land i \neq 0)$
62	13	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (2 π \in ℂ \land 2 π \neq 0)$
63		divdiv1	$⊢ (T \in ℂ \land (i \in ℂ \land i \neq 0) \land (2 π \in ℂ \land 2 π \neq 0)) \to \frac{\frac{T}{i}}{2 π} = \frac{T}{i 2 π}$
64	53 61 62 63	syl3anc	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{\frac{T}{i}}{2 π} = \frac{T}{i 2 π}$
65	64	oveq1d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}) = (\frac{T}{i 2 π}) - (\frac{1}{2})$
66	3 65	syl5eq	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N = (\frac{T}{i 2 π}) - (\frac{1}{2})$
67	26 60 66	3eqtr4a	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{T - i π}{i 2 π} = N$
68		efsub	$⊢ (T \in ℂ \land i π \in ℂ) \to e^{T - i π} = \frac{e^{T}}{e^{i π}}$
69	53 54 68	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to e^{T - i π} = \frac{e^{T}}{e^{i π}}$
70		efipi	$⊢ e^{i π} = - 1$
71	70	oveq2i	$⊢ \frac{e^{T}}{e^{i π}} = \frac{e^{T}}{- 1}$
72	2	fveq2i	$⊢ e^{T} = e^{\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A}$
73		efadd	$⊢ (\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) \in ℂ \land \log A \in ℂ) \to e^{\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A} = e^{\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})} e^{\log A}$
74	50 51 73	syl2anc	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to e^{\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A} = e^{\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})} e^{\log A}$
75		efadd	$⊢ (\log (\frac{1}{1 - A}) \in ℂ \land \log (\frac{A - 1}{A}) \in ℂ) \to e^{\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})} = e^{\log (\frac{1}{1 - A})} e^{\log (\frac{A - 1}{A})}$
76	39 49 75	syl2anc	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to e^{\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})} = e^{\log (\frac{1}{1 - A})} e^{\log (\frac{A - 1}{A})}$
77		eflog	$⊢ (\frac{1}{1 - A} \in ℂ \land \frac{1}{1 - A} \neq 0) \to e^{\log (\frac{1}{1 - A})} = \frac{1}{1 - A}$
78	37 38 77	syl2anc	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to e^{\log (\frac{1}{1 - A})} = \frac{1}{1 - A}$
79		eflog	$⊢ (\frac{A - 1}{A} \in ℂ \land \frac{A - 1}{A} \neq 0) \to e^{\log (\frac{A - 1}{A})} = \frac{A - 1}{A}$
80	43 48 79	syl2anc	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to e^{\log (\frac{A - 1}{A})} = \frac{A - 1}{A}$
81	78 80	oveq12d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to e^{\log (\frac{1}{1 - A})} e^{\log (\frac{A - 1}{A})} = (\frac{1}{1 - A}) (\frac{A - 1}{A})$
82	37 43	mulcomd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{1}{1 - A}) (\frac{A - 1}{A}) = (\frac{A - 1}{A}) (\frac{1}{1 - A})$
83	27	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 1 \in ℂ$
84	83 30 36	div2negd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{- 1}{- (1 - A)} = \frac{1}{1 - A}$
85		negsubdi2	$⊢ (1 \in ℂ \land A \in ℂ) \to - (1 - A) = A - 1$
86	27 28 85	sylancr	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - (1 - A) = A - 1$
87	86	oveq2d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{- 1}{- (1 - A)} = \frac{- 1}{A - 1}$
88	84 87	eqtr3d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{1}{1 - A} = \frac{- 1}{A - 1}$
89	88	oveq2d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{A - 1}{A}) (\frac{1}{1 - A}) = (\frac{A - 1}{A}) (\frac{- 1}{A - 1})$
90		neg1cn	$⊢ - 1 \in ℂ$
91	90	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to - 1 \in ℂ$
92	91 41 28 47 42	dmdcand	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{A - 1}{A}) (\frac{- 1}{A - 1}) = \frac{- 1}{A}$
93	82 89 92	3eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{1}{1 - A}) (\frac{A - 1}{A}) = \frac{- 1}{A}$
94	76 81 93	3eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to e^{\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})} = \frac{- 1}{A}$
95		eflog	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = A$
96	28 42 95	syl2anc	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to e^{\log A} = A$
97	94 96	oveq12d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to e^{\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A})} e^{\log A} = (\frac{- 1}{A}) A$
98	91 28 42	divcan1d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{- 1}{A}) A = - 1$
99	74 97 98	3eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to e^{\log (\frac{1}{1 - A}) + \log (\frac{A - 1}{A}) + \log A} = - 1$
100	72 99	syl5eq	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to e^{T} = - 1$
101	100	oveq1d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{e^{T}}{- 1} = \frac{- 1}{- 1}$
102		neg1ne0	$⊢ - 1 \neq 0$
103	90 102	dividi	$⊢ \frac{- 1}{- 1} = 1$
104	101 103	eqtrdi	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{e^{T}}{- 1} = 1$
105	71 104	syl5eq	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{e^{T}}{e^{i π}} = 1$
106	69 105	eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to e^{T - i π} = 1$
107		subcl	$⊢ (T \in ℂ \land i π \in ℂ) \to T - i π \in ℂ$
108	53 54 107	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to T - i π \in ℂ$
109		efeq1	$⊢ T - i π \in ℂ \to (e^{T - i π} = 1 \leftrightarrow \frac{T - i π}{i 2 π} \in ℤ)$
110	108 109	syl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (e^{T - i π} = 1 \leftrightarrow \frac{T - i π}{i 2 π} \in ℤ)$
111	106 110	mpbid	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{T - i π}{i 2 π} \in ℤ$
112	67 111	eqeltrrd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N \in ℤ$
113	14	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to i \in ℂ$
114	15	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to i \neq 0$
115	53 113 114	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{T}{i} \in ℂ$
116	8	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π \in ℂ$
117	12	a1i	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to 2 π \neq 0$
118	115 116 117	divcan1d	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{\frac{T}{i}}{2 π}) 2 π = \frac{T}{i}$
119	3	oveq1i	$⊢ N + (\frac{1}{2}) = (\frac{\frac{T}{i}}{2 π}) - (\frac{1}{2}) + (\frac{1}{2})$
120	115 116 117	divcld	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{\frac{T}{i}}{2 π} \in ℂ$
121		halfre	$⊢ \frac{1}{2} \in ℝ$
122	121	recni	$⊢ \frac{1}{2} \in ℂ$
123		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 π}$
124	120 122 123	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 π}$
125	119 124	syl5eq	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N + (\frac{1}{2}) = \frac{\frac{T}{i}}{2 π}$
126	112	zred	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N \in ℝ$
127		readdcl	$⊢ (N \in ℝ \land \frac{1}{2} \in ℝ) \to N + (\frac{1}{2}) \in ℝ$
128	126 121 127	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to N + (\frac{1}{2}) \in ℝ$
129	125 128	eqeltrrd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{\frac{T}{i}}{2 π} \in ℝ$
130		remulcl	$⊢ (\frac{\frac{T}{i}}{2 π} \in ℝ \land 2 π \in ℝ) \to (\frac{\frac{T}{i}}{2 π}) 2 π \in ℝ$
131	129 7 130	sylancl	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\frac{\frac{T}{i}}{2 π}) 2 π \in ℝ$
132	118 131	eqeltrrd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \frac{T}{i} \in ℝ$
133	112 132	jca	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (N \in ℤ \land \frac{T}{i} \in ℝ)$

Metamath Proof Explorer

Theorem ang180lem1

Proof