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 2picn ⊢ ( 2 · π ) ∈ ℂ
62 61 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 2 · π ) ∈ ℂ )
63 2cn ⊢ 2 ∈ ℂ
64 picn ⊢ π ∈ ℂ
65 2ne0 ⊢ 2 ≠ 0
66 pine0 ⊢ π ≠ 0
67 63 64 65 66 mulne0i ⊢ ( 2 · π ) ≠ 0
68 67 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 2 · π ) ≠ 0 )
69 60 62 68 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝑇 / i ) / ( 2 · π ) ) ∈ ℂ )
70 69 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( 𝑇 / i ) / ( 2 · π ) ) ∈ ℂ )
71 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
72 subeq0 ⊢ ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) = 0 ↔ ( ( 𝑇 / i ) / ( 2 · π ) ) = ( 1 / 2 ) ) )
73 70 71 72 sylancl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) = 0 ↔ ( ( 𝑇 / i ) / ( 2 · π ) ) = ( 1 / 2 ) ) )
74 27 73 mpbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( 𝑇 / i ) / ( 2 · π ) ) = ( 1 / 2 ) )
75 60 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 𝑇 / i ) ∈ ℂ )
76 61 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 2 · π ) ∈ ℂ )
77 71 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 1 / 2 ) ∈ ℂ )
78 67 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 2 · π ) ≠ 0 )
79 75 76 77 78 divmuld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( ( 𝑇 / i ) / ( 2 · π ) ) = ( 1 / 2 ) ↔ ( ( 2 · π ) · ( 1 / 2 ) ) = ( 𝑇 / i ) ) )
80 74 79 mpbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( 2 · π ) · ( 1 / 2 ) ) = ( 𝑇 / i ) )
81 61 63 65 divreci ⊢ ( ( 2 · π ) / 2 ) = ( ( 2 · π ) · ( 1 / 2 ) )
82 64 63 65 divcan3i ⊢ ( ( 2 · π ) / 2 ) = π
83 81 82 eqtr3i ⊢ ( ( 2 · π ) · ( 1 / 2 ) ) = π
84 80 83 eqtr3di ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 𝑇 / i ) = π )
85 55 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → 𝑇 ∈ ℂ )
86 56 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → i ∈ ℂ )
87 64 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → π ∈ ℂ )
88 58 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → i ≠ 0 )
89 85 86 87 88 divmuld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( ( 𝑇 / i ) = π ↔ ( i · π ) = 𝑇 ) )
90 84 89 mpbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( i · π ) = 𝑇 )
91 90 eqcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → 𝑇 = ( i · π ) )
92 91 olcd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 < 𝑁 ) → ( 𝑇 = - ( i · π ) ∨ 𝑇 = ( i · π ) ) )
93 64 56 mulneg1i ⊢ ( - π · i ) = - ( π · i )
94 64 56 mulcomi ⊢ ( π · i ) = ( i · π )
95 94 negeqi ⊢ - ( π · i ) = - ( i · π )
96 93 95 eqtri ⊢ ( - π · i ) = - ( i · π )
97 71 61 mulneg1i ⊢ ( - ( 1 / 2 ) · ( 2 · π ) ) = - ( ( 1 / 2 ) · ( 2 · π ) )
98 28 63 65 divcan1i ⊢ ( ( 1 / 2 ) · 2 ) = 1
99 98 oveq1i ⊢ ( ( ( 1 / 2 ) · 2 ) · π ) = ( 1 · π )
100 71 63 64 mulassi ⊢ ( ( ( 1 / 2 ) · 2 ) · π ) = ( ( 1 / 2 ) · ( 2 · π ) )
101 64 mullidi ⊢ ( 1 · π ) = π
102 99 100 101 3eqtr3i ⊢ ( ( 1 / 2 ) · ( 2 · π ) ) = π
103 102 negeqi ⊢ - ( ( 1 / 2 ) · ( 2 · π ) ) = - π
104 97 103 eqtri ⊢ ( - ( 1 / 2 ) · ( 2 · π ) ) = - π
105 28 71 negsubdii ⊢ - ( 1 − ( 1 / 2 ) ) = ( - 1 + ( 1 / 2 ) )
106 1mhlfehlf ⊢ ( 1 − ( 1 / 2 ) ) = ( 1 / 2 )
107 106 negeqi ⊢ - ( 1 − ( 1 / 2 ) ) = - ( 1 / 2 )
108 105 107 eqtr3i ⊢ ( - 1 + ( 1 / 2 ) ) = - ( 1 / 2 )
109 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - 1 = 𝑁 )
110 109 3 eqtrdi ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - 1 = ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) )
111 110 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( - 1 + ( 1 / 2 ) ) = ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) + ( 1 / 2 ) ) )
112 108 111 eqtr3id ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - ( 1 / 2 ) = ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) + ( 1 / 2 ) ) )
113 npcan ⊢ ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( 𝑇 / i ) / ( 2 · π ) ) )
114 69 71 113 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( 𝑇 / i ) / ( 2 · π ) ) )
115 114 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( 𝑇 / i ) / ( 2 · π ) ) )
116 112 115 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - ( 1 / 2 ) = ( ( 𝑇 / i ) / ( 2 · π ) ) )
117 116 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( - ( 1 / 2 ) · ( 2 · π ) ) = ( ( ( 𝑇 / i ) / ( 2 · π ) ) · ( 2 · π ) ) )
118 104 117 eqtr3id ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - π = ( ( ( 𝑇 / i ) / ( 2 · π ) ) · ( 2 · π ) ) )
119 60 62 68 divcan1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( 𝑇 / i ) / ( 2 · π ) ) · ( 2 · π ) ) = ( 𝑇 / i ) )
120 119 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( ( ( 𝑇 / i ) / ( 2 · π ) ) · ( 2 · π ) ) = ( 𝑇 / i ) )
121 118 120 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - π = ( 𝑇 / i ) )
122 121 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( - π · i ) = ( ( 𝑇 / i ) · i ) )
123 96 122 eqtr3id ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → - ( i · π ) = ( ( 𝑇 / i ) · i ) )
124 55 57 59 divcan1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝑇 / i ) · i ) = 𝑇 )
125 124 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( ( 𝑇 / i ) · i ) = 𝑇 )
126 123 125 eqtr2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → 𝑇 = - ( i · π ) )
127 126 orcd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ - 1 = 𝑁 ) → ( 𝑇 = - ( i · π ) ∨ 𝑇 = ( i · π ) ) )
128 df-2 ⊢ 2 = ( 1 + 1 )
129 128 negeqi ⊢ - 2 = - ( 1 + 1 )
130 negdi2 ⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ) → - ( 1 + 1 ) = ( - 1 − 1 ) )
131 28 28 130 mp2an ⊢ - ( 1 + 1 ) = ( - 1 − 1 )
132 129 131 eqtri ⊢ - 2 = ( - 1 − 1 )
133 4 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - 2 < 𝑁 )
134 132 133 eqbrtrrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 1 − 1 ) < 𝑁 )
135 neg1z ⊢ - 1 ∈ ℤ
136 zlem1lt ⊢ ( ( - 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 1 ≤ 𝑁 ↔ ( - 1 − 1 ) < 𝑁 ) )
137 135 9 136 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 1 ≤ 𝑁 ↔ ( - 1 − 1 ) < 𝑁 ) )
138 134 137 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - 1 ≤ 𝑁 )
139 neg1rr ⊢ - 1 ∈ ℝ
140 leloe ⊢ ( ( - 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( - 1 ≤ 𝑁 ↔ ( - 1 < 𝑁 ∨ - 1 = 𝑁 ) ) )
141 139 21 140 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 1 ≤ 𝑁 ↔ ( - 1 < 𝑁 ∨ - 1 = 𝑁 ) ) )
142 138 141 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 1 < 𝑁 ∨ - 1 = 𝑁 ) )
143 92 127 142 mpjaodan ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑇 = - ( i · π ) ∨ 𝑇 = ( i · π ) ) )
144 2 ovexi ⊢ 𝑇 ∈ V
145 144 elpr ⊢ ( 𝑇 ∈ { - ( i · π ) , ( i · π ) } ↔ ( 𝑇 = - ( i · π ) ∨ 𝑇 = ( i · π ) ) )
146 143 145 sylibr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑇 ∈ { - ( i · π ) , ( i · π ) } )