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 1 2 3 ang180lem2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 2 < 𝑁 ∧ 𝑁 < 1 ) )
5 4 simprd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑁 < 1 )
6 1e0p1 ⊢ 1 = ( 0 + 1 )
7 5 6 breqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑁 < ( 0 + 1 ) )
8 1 2 3 ang180lem1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑁 ∈ ℤ ∧ ( 𝑇 / i ) ∈ ℝ ) )
9 8 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑁 ∈ ℤ )
10 0z ⊢ 0 ∈ ℤ
11 zleltp1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 𝑁 ≤ 0 ↔ 𝑁 < ( 0 + 1 ) ) )
12 9 10 11 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑁 ≤ 0 ↔ 𝑁 < ( 0 + 1 ) ) )
13 7 12 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑁 ≤ 0 )
14 13 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → 𝑁 ≤ 0 )
15 zlem1lt ⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ≤ 𝑁 ↔ ( 0 − 1 ) < 𝑁 ) )
16 10 9 15 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 0 ≤ 𝑁 ↔ ( 0 − 1 ) < 𝑁 ) )
17 df-neg ⊢ - 1 = ( 0 − 1 )
18 17 breq1i ⊢ ( - 1 < 𝑁 ↔ ( 0 − 1 ) < 𝑁 )
19 16 18 bitr4di ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 0 ≤ 𝑁 ↔ - 1 < 𝑁 ) )
20 19 biimpar ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → 0 ≤ 𝑁 )
21 9 zred ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑁 ∈ ℝ )
22 21 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → 𝑁 ∈ ℝ )
23 0re ⊢ 0 ∈ ℝ
24 letri3 ⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝑁 = 0 ↔ ( 𝑁 ≤ 0 ∧ 0 ≤ 𝑁 ) ) )
25 22 23 24 sylancl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 𝑁 = 0 ↔ ( 𝑁 ≤ 0 ∧ 0 ≤ 𝑁 ) ) )
26 14 20 25 mpbir2and ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → 𝑁 = 0 )
27 3 26 eqtr3id ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) = 0 )
28 ax-1cn ⊢ 1 ∈ ℂ
29 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ∈ ℂ )
30 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 − 𝐴 ) ∈ ℂ )
31 28 29 30 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 − 𝐴 ) ∈ ℂ )
32 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ≠ 1 )
33 32 necomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 1 ≠ 𝐴 )
34 subeq0 ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
35 28 29 34 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
36 35 necon3bid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 1 − 𝐴 ) ≠ 0 ↔ 1 ≠ 𝐴 ) )
37 33 36 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 − 𝐴 ) ≠ 0 )
38 31 37 reccld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 / ( 1 − 𝐴 ) ) ∈ ℂ )
39 31 37 recne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 / ( 1 − 𝐴 ) ) ≠ 0 )
40 38 39 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ∈ ℂ )
41 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 − 1 ) ∈ ℂ )
42 29 28 41 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝐴 − 1 ) ∈ ℂ )
43 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ≠ 0 )
44 42 29 43 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) / 𝐴 ) ∈ ℂ )
45 subeq0 ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 − 1 ) = 0 ↔ 𝐴 = 1 ) )
46 29 28 45 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) = 0 ↔ 𝐴 = 1 ) )
47 46 necon3bid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) ≠ 0 ↔ 𝐴 ≠ 1 ) )
48 32 47 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝐴 − 1 ) ≠ 0 )
49 42 29 48 43 divne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) / 𝐴 ) ≠ 0 )
50 44 49 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ∈ ℂ )
51 40 50 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ∈ ℂ )
52 logcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
53 52 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ 𝐴 ) ∈ ℂ )
54 51 53 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ∈ ℂ )
55 2 54 eqeltrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑇 ∈ ℂ )
56 ax-icn ⊢ i ∈ ℂ
57 56 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → i ∈ ℂ )
58 ine0 ⊢ i ≠ 0
59 58 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → i ≠ 0 )
60 55 57 59 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑇 / i ) ∈ ℂ )
61 2cn ⊢ 2 ∈ ℂ
62 picn ⊢ π ∈ ℂ
63 61 62 mulcli ⊢ ( 2 · π ) ∈ ℂ
64 63 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 2 · π ) ∈ ℂ )
65 2ne0 ⊢ 2 ≠ 0
66 pire ⊢ π ∈ ℝ
67 pipos ⊢ 0 < π
68 66 67 gt0ne0ii ⊢ π ≠ 0
69 61 62 65 68 mulne0i ⊢ ( 2 · π ) ≠ 0
70 69 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 2 · π ) ≠ 0 )
71 60 64 70 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝑇 / i ) / ( 2 · π ) ) ∈ ℂ )
72 71 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( 𝑇 / i ) / ( 2 · π ) ) ∈ ℂ )
73 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
74 subeq0 ⊢ ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) = 0 ↔ ( ( 𝑇 / i ) / ( 2 · π ) ) = ( 1 / 2 ) ) )
75 72 73 74 sylancl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) = 0 ↔ ( ( 𝑇 / i ) / ( 2 · π ) ) = ( 1 / 2 ) ) )
76 27 75 mpbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( 𝑇 / i ) / ( 2 · π ) ) = ( 1 / 2 ) )
77 60 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 𝑇 / i ) ∈ ℂ )
78 63 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 2 · π ) ∈ ℂ )
79 73 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 1 / 2 ) ∈ ℂ )
80 69 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 2 · π ) ≠ 0 )
81 77 78 79 80 divmuld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( ( 𝑇 / i ) / ( 2 · π ) ) = ( 1 / 2 ) ↔ ( ( 2 · π ) · ( 1 / 2 ) ) = ( 𝑇 / i ) ) )
82 76 81 mpbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( 2 · π ) · ( 1 / 2 ) ) = ( 𝑇 / i ) )
83 63 61 65 divreci ⊢ ( ( 2 · π ) / 2 ) = ( ( 2 · π ) · ( 1 / 2 ) )
84 62 61 65 divcan3i ⊢ ( ( 2 · π ) / 2 ) = π
85 83 84 eqtr3i ⊢ ( ( 2 · π ) · ( 1 / 2 ) ) = π
86 82 85 eqtr3di ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 𝑇 / i ) = π )
87 55 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → 𝑇 ∈ ℂ )
88 56 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → i ∈ ℂ )
89 62 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → π ∈ ℂ )
90 58 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 62 56 mulneg1i ⊢ ( - π · i ) = - ( π · i )
96 62 56 mulcomi ⊢ ( π · i ) = ( i · π )
97 96 negeqi ⊢ - ( π · i ) = - ( i · π )
98 95 97 eqtri ⊢ ( - π · i ) = - ( i · π )
99 73 63 mulneg1i ⊢ ( - ( 1 / 2 ) · ( 2 · π ) ) = - ( ( 1 / 2 ) · ( 2 · π ) )
100 28 61 65 divcan1i ⊢ ( ( 1 / 2 ) · 2 ) = 1
101 100 oveq1i ⊢ ( ( ( 1 / 2 ) · 2 ) · π ) = ( 1 · π )
102 73 61 62 mulassi ⊢ ( ( ( 1 / 2 ) · 2 ) · π ) = ( ( 1 / 2 ) · ( 2 · π ) )
103 62 mulid2i ⊢ ( 1 · π ) = π
104 101 102 103 3eqtr3i ⊢ ( ( 1 / 2 ) · ( 2 · π ) ) = π
105 104 negeqi ⊢ - ( ( 1 / 2 ) · ( 2 · π ) ) = - π
106 99 105 eqtri ⊢ ( - ( 1 / 2 ) · ( 2 · π ) ) = - π
107 28 73 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 71 73 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 60 64 70 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 55 57 59 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 28 28 132 mp2an ⊢ - ( 1 + 1 ) = ( - 1 − 1 )
134 131 133 eqtri ⊢ - 2 = ( - 1 − 1 )
135 4 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - 2 < 𝑁 )
136 134 135 eqbrtrrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 1 − 1 ) < 𝑁 )
137 neg1z ⊢ - 1 ∈ ℤ
138 zlem1lt ⊢ ( ( - 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 1 ≤ 𝑁 ↔ ( - 1 − 1 ) < 𝑁 ) )
139 137 9 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 21 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 · π ) } )