Theorem 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	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
	ang180lem1.2	⊢ 𝑇 = ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) )
	ang180lem1.3	⊢ 𝑁 = ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) )
Assertion	ang180lem1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑁 ∈ ℤ ∧ ( 𝑇 / i ) ∈ ℝ ) )

Proof

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