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 
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
ang180lem1.2 
|- T = ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) )
ang180lem1.3 
|- N = ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) )
Assertion ang180lem1 
|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( N e. ZZ /\ ( T / _i ) e. RR ) )

Proof

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