Metamath Proof Explorer

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 syl5eq ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 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 syl5eq ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 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 syl5eq ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 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 syl5eq ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 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 ) ∈ ℝ ) )