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 F=x0,y0logyx
ang180lem1.2 T=log11A+logA1A+logA
ang180lem1.3 N=Ti2π12
Assertion ang180lem3 AA0A1Tiπiπ

Proof

Step Hyp Ref Expression
1 ang.1 F=x0,y0logyx
2 ang180lem1.2 T=log11A+logA1A+logA
3 ang180lem1.3 N=Ti2π12
4 1 2 3 ang180lem2 AA0A12<NN<1
5 4 simprd AA0A1N<1
6 1e0p1 1=0+1
7 5 6 breqtrdi AA0A1N<0+1
8 1 2 3 ang180lem1 AA0A1NTi
9 8 simpld AA0A1N
10 0z 0
11 zleltp1 N0N0N<0+1
12 9 10 11 sylancl AA0A1N0N<0+1
13 7 12 mpbird AA0A1N0
14 13 adantr AA0A11<NN0
15 zlem1lt 0N0N01<N
16 10 9 15 sylancr AA0A10N01<N
17 df-neg 1=01
18 17 breq1i 1<N01<N
19 16 18 bitr4di AA0A10N1<N
20 19 biimpar AA0A11<N0N
21 9 zred AA0A1N
22 21 adantr AA0A11<NN
23 0re 0
24 letri3 N0N=0N00N
25 22 23 24 sylancl AA0A11<NN=0N00N
26 14 20 25 mpbir2and AA0A11<NN=0
27 3 26 eqtr3id AA0A11<NTi2π12=0
28 ax-1cn 1
29 simp1 AA0A1A
30 subcl 1A1A
31 28 29 30 sylancr AA0A11A
32 simp3 AA0A1A1
33 32 necomd AA0A11A
34 subeq0 1A1A=01=A
35 28 29 34 sylancr AA0A11A=01=A
36 35 necon3bid AA0A11A01A
37 33 36 mpbird AA0A11A0
38 31 37 reccld AA0A111A
39 31 37 recne0d AA0A111A0
40 38 39 logcld AA0A1log11A
41 subcl A1A1
42 29 28 41 sylancl AA0A1A1
43 simp2 AA0A1A0
44 42 29 43 divcld AA0A1A1A
45 subeq0 A1A1=0A=1
46 29 28 45 sylancl AA0A1A1=0A=1
47 46 necon3bid AA0A1A10A1
48 32 47 mpbird AA0A1A10
49 42 29 48 43 divne0d AA0A1A1A0
50 44 49 logcld AA0A1logA1A
51 40 50 addcld AA0A1log11A+logA1A
52 logcl AA0logA
53 52 3adant3 AA0A1logA
54 51 53 addcld AA0A1log11A+logA1A+logA
55 2 54 eqeltrid AA0A1T
56 ax-icn i
57 56 a1i AA0A1i
58 ine0 i0
59 58 a1i AA0A1i0
60 55 57 59 divcld AA0A1Ti
61 2cn 2
62 picn π
63 61 62 mulcli 2π
64 63 a1i AA0A12π
65 2ne0 20
66 pire π
67 pipos 0<π
68 66 67 gt0ne0ii π0
69 61 62 65 68 mulne0i 2π0
70 69 a1i AA0A12π0
71 60 64 70 divcld AA0A1Ti2π
72 71 adantr AA0A11<NTi2π
73 halfcn 12
74 subeq0 Ti2π12Ti2π12=0Ti2π=12
75 72 73 74 sylancl AA0A11<NTi2π12=0Ti2π=12
76 27 75 mpbid AA0A11<NTi2π=12
77 60 adantr AA0A11<NTi
78 63 a1i AA0A11<N2π
79 73 a1i AA0A11<N12
80 69 a1i AA0A11<N2π0
81 77 78 79 80 divmuld AA0A11<NTi2π=122π12=Ti
82 76 81 mpbid AA0A11<N2π12=Ti
83 63 61 65 divreci 2π2=2π12
84 62 61 65 divcan3i 2π2=π
85 83 84 eqtr3i 2π12=π
86 82 85 eqtr3di AA0A11<NTi=π
87 55 adantr AA0A11<NT
88 56 a1i AA0A11<Ni
89 62 a1i AA0A11<Nπ
90 58 a1i AA0A11<Ni0
91 87 88 89 90 divmuld AA0A11<NTi=πiπ=T
92 86 91 mpbid AA0A11<Niπ=T
93 92 eqcomd AA0A11<NT=iπ
94 93 olcd AA0A11<NT=iπT=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 122π=122π
100 28 61 65 divcan1i 122=1
101 100 oveq1i 122π=1π
102 73 61 62 mulassi 122π=122π
103 62 mulid2i 1π=π
104 101 102 103 3eqtr3i 122π=π
105 104 negeqi 122π=π
106 99 105 eqtri 122π=π
107 28 73 negsubdii 112=-1+12
108 1mhlfehlf 112=12
109 108 negeqi 112=12
110 107 109 eqtr3i -1+12=12
111 simpr AA0A11=N1=N
112 111 3 eqtrdi AA0A11=N1=Ti2π12
113 112 oveq1d AA0A11=N-1+12=Ti2π-12+12
114 110 113 eqtr3id AA0A11=N12=Ti2π-12+12
115 npcan Ti2π12Ti2π-12+12=Ti2π
116 71 73 115 sylancl AA0A1Ti2π-12+12=Ti2π
117 116 adantr AA0A11=NTi2π-12+12=Ti2π
118 114 117 eqtrd AA0A11=N12=Ti2π
119 118 oveq1d AA0A11=N122π=Ti2π2π
120 106 119 eqtr3id AA0A11=Nπ=Ti2π2π
121 60 64 70 divcan1d AA0A1Ti2π2π=Ti
122 121 adantr AA0A11=NTi2π2π=Ti
123 120 122 eqtrd AA0A11=Nπ=Ti
124 123 oveq1d AA0A11=Nπi=Tii
125 98 124 eqtr3id AA0A11=Niπ=Tii
126 55 57 59 divcan1d AA0A1Tii=T
127 126 adantr AA0A11=NTii=T
128 125 127 eqtr2d AA0A11=NT=iπ
129 128 orcd AA0A11=NT=iπT=iπ
130 df-2 2=1+1
131 130 negeqi 2=1+1
132 negdi2 111+1=-1-1
133 28 28 132 mp2an 1+1=-1-1
134 131 133 eqtri 2=-1-1
135 4 simpld AA0A12<N
136 134 135 eqbrtrrid AA0A1-1-1<N
137 neg1z 1
138 zlem1lt 1N1N-1-1<N
139 137 9 138 sylancr AA0A11N-1-1<N
140 136 139 mpbird AA0A11N
141 neg1rr 1
142 leloe 1N1N1<N1=N
143 141 21 142 sylancr AA0A11N1<N1=N
144 140 143 mpbid AA0A11<N1=N
145 94 129 144 mpjaodan AA0A1T=iπT=iπ
146 2 ovexi TV
147 146 elpr TiπiπT=iπT=iπ
148 145 147 sylibr AA0A1Tiπiπ