Metamath Proof Explorer

Theorem 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 ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
ang180lem1.2 ⊢ 𝑇 = ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) )
ang180lem1.3 ⊢ 𝑁 = ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) )
Assertion ang180lem3 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑇 ∈ { - ( i · π ) , ( 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 2cn ⊢ 2 ∈ ℂ
5 picn ⊢ π ∈ ℂ
6 4 5 mulcli ⊢ ( 2 · π ) ∈ ℂ
7 2ne0 ⊢ 2 ≠ 0
8 6 4 7 divreci ⊢ ( ( 2 · π ) / 2 ) = ( ( 2 · π ) · ( 1 / 2 ) )
9 5 4 7 divcan3i ⊢ ( ( 2 · π ) / 2 ) = π
10 8 9 eqtr3i ⊢ ( ( 2 · π ) · ( 1 / 2 ) ) = π
11 1 2 3 ang180lem2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 2 < 𝑁 ∧ 𝑁 < 1 ) )
12 11 simprd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑁 < 1 )
13 1e0p1 ⊢ 1 = ( 0 + 1 )
14 12 13 breqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑁 < ( 0 + 1 ) )
15 1 2 3 ang180lem1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑁 ∈ ℤ ∧ ( 𝑇 / i ) ∈ ℝ ) )
16 15 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑁 ∈ ℤ )
17 0z ⊢ 0 ∈ ℤ
18 zleltp1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 𝑁 ≤ 0 ↔ 𝑁 < ( 0 + 1 ) ) )
19 16 17 18 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑁 ≤ 0 ↔ 𝑁 < ( 0 + 1 ) ) )
20 14 19 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑁 ≤ 0 )
21 20 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → 𝑁 ≤ 0 )
22 zlem1lt ⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ≤ 𝑁 ↔ ( 0 − 1 ) < 𝑁 ) )
23 17 16 22 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 0 ≤ 𝑁 ↔ ( 0 − 1 ) < 𝑁 ) )
24 df-neg ⊢ - 1 = ( 0 − 1 )
25 24 breq1i ⊢ ( - 1 < 𝑁 ↔ ( 0 − 1 ) < 𝑁 )
26 23 25 bitr4di ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 0 ≤ 𝑁 ↔ - 1 < 𝑁 ) )
27 26 biimpar ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → 0 ≤ 𝑁 )
28 16 zred ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑁 ∈ ℝ )
29 28 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → 𝑁 ∈ ℝ )
30 0re ⊢ 0 ∈ ℝ
31 letri3 ⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝑁 = 0 ↔ ( 𝑁 ≤ 0 ∧ 0 ≤ 𝑁 ) ) )
32 29 30 31 sylancl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 𝑁 = 0 ↔ ( 𝑁 ≤ 0 ∧ 0 ≤ 𝑁 ) ) )
33 21 27 32 mpbir2and ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → 𝑁 = 0 )
34 3 33 eqtr3id ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) = 0 )
35 ax-1cn ⊢ 1 ∈ ℂ
36 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ∈ ℂ )
37 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 − 𝐴 ) ∈ ℂ )
38 35 36 37 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 − 𝐴 ) ∈ ℂ )
39 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ≠ 1 )
40 39 necomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 1 ≠ 𝐴 )
41 subeq0 ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
42 35 36 41 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
43 42 necon3bid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 1 − 𝐴 ) ≠ 0 ↔ 1 ≠ 𝐴 ) )
44 40 43 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 − 𝐴 ) ≠ 0 )
45 38 44 reccld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 / ( 1 − 𝐴 ) ) ∈ ℂ )
46 38 44 recne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 / ( 1 − 𝐴 ) ) ≠ 0 )
47 45 46 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ∈ ℂ )
48 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 − 1 ) ∈ ℂ )
49 36 35 48 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝐴 − 1 ) ∈ ℂ )
50 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ≠ 0 )
51 49 36 50 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) / 𝐴 ) ∈ ℂ )
52 subeq0 ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 − 1 ) = 0 ↔ 𝐴 = 1 ) )
53 36 35 52 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) = 0 ↔ 𝐴 = 1 ) )
54 53 necon3bid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) ≠ 0 ↔ 𝐴 ≠ 1 ) )
55 39 54 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝐴 − 1 ) ≠ 0 )
56 49 36 55 50 divne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) / 𝐴 ) ≠ 0 )
57 51 56 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ∈ ℂ )
58 47 57 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ∈ ℂ )
59 logcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
60 59 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ 𝐴 ) ∈ ℂ )
61 58 60 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ∈ ℂ )
62 2 61 eqeltrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑇 ∈ ℂ )
63 ax-icn ⊢ i ∈ ℂ
64 63 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → i ∈ ℂ )
65 ine0 ⊢ i ≠ 0
66 65 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → i ≠ 0 )
67 62 64 66 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑇 / i ) ∈ ℂ )
68 6 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 2 · π ) ∈ ℂ )
69 pire ⊢ π ∈ ℝ
70 pipos ⊢ 0 < π
71 69 70 gt0ne0ii ⊢ π ≠ 0
72 4 5 7 71 mulne0i ⊢ ( 2 · π ) ≠ 0
73 72 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 2 · π ) ≠ 0 )
74 67 68 73 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝑇 / i ) / ( 2 · π ) ) ∈ ℂ )
75 74 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( 𝑇 / i ) / ( 2 · π ) ) ∈ ℂ )
76 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
77 subeq0 ⊢ ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) = 0 ↔ ( ( 𝑇 / i ) / ( 2 · π ) ) = ( 1 / 2 ) ) )
78 75 76 77 sylancl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) = 0 ↔ ( ( 𝑇 / i ) / ( 2 · π ) ) = ( 1 / 2 ) ) )
79 34 78 mpbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( 𝑇 / i ) / ( 2 · π ) ) = ( 1 / 2 ) )
80 67 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 𝑇 / i ) ∈ ℂ )
81 6 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 2 · π ) ∈ ℂ )
82 76 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 1 / 2 ) ∈ ℂ )
83 72 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 2 · π ) ≠ 0 )
84 80 81 82 83 divmuld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( ( 𝑇 / i ) / ( 2 · π ) ) = ( 1 / 2 ) ↔ ( ( 2 · π ) · ( 1 / 2 ) ) = ( 𝑇 / i ) ) )
85 79 84 mpbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( 2 · π ) · ( 1 / 2 ) ) = ( 𝑇 / i ) )
86 10 85 syl5reqr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 𝑇 / i ) = π )
87 62 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → 𝑇 ∈ ℂ )
88 63 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → i ∈ ℂ )
89 5 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → π ∈ ℂ )
90 65 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → i ≠ 0 )
91 87 88 89 90 divmuld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( 𝑇 / i ) = π ↔ ( i · π ) = 𝑇 ) )
92 86 91 mpbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( i · π ) = 𝑇 )
93 92 eqcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → 𝑇 = ( i · π ) )
94 93 olcd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 𝑇 = - ( i · π ) ∨ 𝑇 = ( i · π ) ) )
95 5 63 mulneg1i ⊢ ( - π · i ) = - ( π · i )
96 5 63 mulcomi ⊢ ( π · i ) = ( i · π )
97 96 negeqi ⊢ - ( π · i ) = - ( i · π )
98 95 97 eqtri ⊢ ( - π · i ) = - ( i · π )
99 76 6 mulneg1i ⊢ ( - ( 1 / 2 ) · ( 2 · π ) ) = - ( ( 1 / 2 ) · ( 2 · π ) )
100 35 4 7 divcan1i ⊢ ( ( 1 / 2 ) · 2 ) = 1
101 100 oveq1i ⊢ ( ( ( 1 / 2 ) · 2 ) · π ) = ( 1 · π )
102 76 4 5 mulassi ⊢ ( ( ( 1 / 2 ) · 2 ) · π ) = ( ( 1 / 2 ) · ( 2 · π ) )
103 5 mulid2i ⊢ ( 1 · π ) = π
104 101 102 103 3eqtr3i ⊢ ( ( 1 / 2 ) · ( 2 · π ) ) = π
105 104 negeqi ⊢ - ( ( 1 / 2 ) · ( 2 · π ) ) = - π
106 99 105 eqtri ⊢ ( - ( 1 / 2 ) · ( 2 · π ) ) = - π
107 35 76 negsubdii ⊢ - ( 1 − ( 1 / 2 ) ) = ( - 1 + ( 1 / 2 ) )
108 1mhlfehlf ⊢ ( 1 − ( 1 / 2 ) ) = ( 1 / 2 )
109 108 negeqi ⊢ - ( 1 − ( 1 / 2 ) ) = - ( 1 / 2 )
110 107 109 eqtr3i ⊢ ( - 1 + ( 1 / 2 ) ) = - ( 1 / 2 )
111 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - 1 = 𝑁 )
112 111 3 eqtrdi ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - 1 = ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) )
113 112 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( - 1 + ( 1 / 2 ) ) = ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) + ( 1 / 2 ) ) )
114 110 113 eqtr3id ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - ( 1 / 2 ) = ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) + ( 1 / 2 ) ) )
115 npcan ⊢ ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( 𝑇 / i ) / ( 2 · π ) ) )
116 74 76 115 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( 𝑇 / i ) / ( 2 · π ) ) )
117 116 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( 𝑇 / i ) / ( 2 · π ) ) )
118 114 117 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - ( 1 / 2 ) = ( ( 𝑇 / i ) / ( 2 · π ) ) )
119 118 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( - ( 1 / 2 ) · ( 2 · π ) ) = ( ( ( 𝑇 / i ) / ( 2 · π ) ) · ( 2 · π ) ) )
120 106 119 eqtr3id ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - π = ( ( ( 𝑇 / i ) / ( 2 · π ) ) · ( 2 · π ) ) )
121 67 68 73 divcan1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( 𝑇 / i ) / ( 2 · π ) ) · ( 2 · π ) ) = ( 𝑇 / i ) )
122 121 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( ( ( 𝑇 / i ) / ( 2 · π ) ) · ( 2 · π ) ) = ( 𝑇 / i ) )
123 120 122 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - π = ( 𝑇 / i ) )
124 123 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( - π · i ) = ( ( 𝑇 / i ) · i ) )
125 98 124 eqtr3id ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - ( i · π ) = ( ( 𝑇 / i ) · i ) )
126 62 64 66 divcan1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝑇 / i ) · i ) = 𝑇 )
127 126 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( ( 𝑇 / i ) · i ) = 𝑇 )
128 125 127 eqtr2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → 𝑇 = - ( i · π ) )
129 128 orcd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( 𝑇 = - ( i · π ) ∨ 𝑇 = ( i · π ) ) )
130 df-2 ⊢ 2 = ( 1 + 1 )
131 130 negeqi ⊢ - 2 = - ( 1 + 1 )
132 negdi2 ⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ) → - ( 1 + 1 ) = ( - 1 − 1 ) )
133 35 35 132 mp2an ⊢ - ( 1 + 1 ) = ( - 1 − 1 )
134 131 133 eqtri ⊢ - 2 = ( - 1 − 1 )
135 11 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - 2 < 𝑁 )
136 134 135 eqbrtrrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 1 − 1 ) < 𝑁 )
137 neg1z ⊢ - 1 ∈ ℤ
138 zlem1lt ⊢ ( ( - 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 1 ≤ 𝑁 ↔ ( - 1 − 1 ) < 𝑁 ) )
139 137 16 138 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 1 ≤ 𝑁 ↔ ( - 1 − 1 ) < 𝑁 ) )
140 136 139 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - 1 ≤ 𝑁 )
141 neg1rr ⊢ - 1 ∈ ℝ
142 leloe ⊢ ( ( - 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( - 1 ≤ 𝑁 ↔ ( - 1 < 𝑁 ∨ - 1 = 𝑁 ) ) )
143 141 28 142 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 1 ≤ 𝑁 ↔ ( - 1 < 𝑁 ∨ - 1 = 𝑁 ) ) )
144 140 143 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 1 < 𝑁 ∨ - 1 = 𝑁 ) )
145 94 129 144 mpjaodan ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑇 = - ( i · π ) ∨ 𝑇 = ( i · π ) ) )
146 2 ovexi ⊢ 𝑇 ∈ V
147 146 elpr ⊢ ( 𝑇 ∈ { - ( i · π ) , ( i · π ) } ↔ ( 𝑇 = - ( i · π ) ∨ 𝑇 = ( i · π ) ) )
148 145 147 sylibr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑇 ∈ { - ( i · π ) , ( i · π ) } )