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

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 picn π
5 2re 2
6 pire π
7 5 6 remulcli 2π
8 7 recni 2π
9 2pos 0<2
10 pipos 0<π
11 5 6 9 10 mulgt0ii 0<2π
12 7 11 gt0ne0ii 2π0
13 8 12 pm3.2i 2π2π0
14 ax-icn i
15 ine0 i0
16 14 15 pm3.2i ii0
17 divcan5 π2π2π0ii0iπi2π=π2π
18 4 13 16 17 mp3an iπi2π=π2π
19 6 10 gt0ne0ii π0
20 recdiv 2π2π0ππ012ππ=π2π
21 8 12 4 19 20 mp4an 12ππ=π2π
22 5 recni 2
23 22 4 19 divcan4i 2ππ=2
24 23 oveq2i 12ππ=12
25 18 21 24 3eqtr2i iπi2π=12
26 25 oveq2i Ti2πiπi2π=Ti2π12
27 ax-1cn 1
28 simp1 AA0A1A
29 subcl 1A1A
30 27 28 29 sylancr AA0A11A
31 simp3 AA0A1A1
32 31 necomd AA0A11A
33 subeq0 1A1A=01=A
34 27 28 33 sylancr AA0A11A=01=A
35 34 necon3bid AA0A11A01A
36 32 35 mpbird AA0A11A0
37 30 36 reccld AA0A111A
38 30 36 recne0d AA0A111A0
39 37 38 logcld AA0A1log11A
40 subcl A1A1
41 28 27 40 sylancl AA0A1A1
42 simp2 AA0A1A0
43 41 28 42 divcld AA0A1A1A
44 subeq0 A1A1=0A=1
45 28 27 44 sylancl AA0A1A1=0A=1
46 45 necon3bid AA0A1A10A1
47 31 46 mpbird AA0A1A10
48 41 28 47 42 divne0d AA0A1A1A0
49 43 48 logcld AA0A1logA1A
50 39 49 addcld AA0A1log11A+logA1A
51 28 42 logcld AA0A1logA
52 50 51 addcld AA0A1log11A+logA1A+logA
53 2 52 eqeltrid AA0A1T
54 14 4 mulcli iπ
55 54 a1i AA0A1iπ
56 14 8 mulcli i2π
57 56 a1i AA0A1i2π
58 14 8 15 12 mulne0i i2π0
59 58 a1i AA0A1i2π0
60 53 55 57 59 divsubdird AA0A1Tiπi2π=Ti2πiπi2π
61 16 a1i AA0A1ii0
62 13 a1i AA0A12π2π0
63 divdiv1 Tii02π2π0Ti2π=Ti2π
64 53 61 62 63 syl3anc AA0A1Ti2π=Ti2π
65 64 oveq1d AA0A1Ti2π12=Ti2π12
66 3 65 eqtrid AA0A1N=Ti2π12
67 26 60 66 3eqtr4a AA0A1Tiπi2π=N
68 efsub TiπeTiπ=eTeiπ
69 53 54 68 sylancl AA0A1eTiπ=eTeiπ
70 efipi eiπ=1
71 70 oveq2i eTeiπ=eT1
72 2 fveq2i eT=elog11A+logA1A+logA
73 efadd log11A+logA1AlogAelog11A+logA1A+logA=elog11A+logA1AelogA
74 50 51 73 syl2anc AA0A1elog11A+logA1A+logA=elog11A+logA1AelogA
75 efadd log11AlogA1Aelog11A+logA1A=elog11AelogA1A
76 39 49 75 syl2anc AA0A1elog11A+logA1A=elog11AelogA1A
77 eflog 11A11A0elog11A=11A
78 37 38 77 syl2anc AA0A1elog11A=11A
79 eflog A1AA1A0elogA1A=A1A
80 43 48 79 syl2anc AA0A1elogA1A=A1A
81 78 80 oveq12d AA0A1elog11AelogA1A=11AA1A
82 37 43 mulcomd AA0A111AA1A=A1A11A
83 27 a1i AA0A11
84 83 30 36 div2negd AA0A111A=11A
85 negsubdi2 1A1A=A1
86 27 28 85 sylancr AA0A11A=A1
87 86 oveq2d AA0A111A=1A1
88 84 87 eqtr3d AA0A111A=1A1
89 88 oveq2d AA0A1A1A11A=A1A1A1
90 neg1cn 1
91 90 a1i AA0A11
92 91 41 28 47 42 dmdcand AA0A1A1A1A1=1A
93 82 89 92 3eqtrd AA0A111AA1A=1A
94 76 81 93 3eqtrd AA0A1elog11A+logA1A=1A
95 eflog AA0elogA=A
96 28 42 95 syl2anc AA0A1elogA=A
97 94 96 oveq12d AA0A1elog11A+logA1AelogA=1AA
98 91 28 42 divcan1d AA0A11AA=1
99 74 97 98 3eqtrd AA0A1elog11A+logA1A+logA=1
100 72 99 eqtrid AA0A1eT=1
101 100 oveq1d AA0A1eT1=11
102 neg1ne0 10
103 90 102 dividi 11=1
104 101 103 eqtrdi AA0A1eT1=1
105 71 104 eqtrid AA0A1eTeiπ=1
106 69 105 eqtrd AA0A1eTiπ=1
107 subcl TiπTiπ
108 53 54 107 sylancl AA0A1Tiπ
109 efeq1 TiπeTiπ=1Tiπi2π
110 108 109 syl AA0A1eTiπ=1Tiπi2π
111 106 110 mpbid AA0A1Tiπi2π
112 67 111 eqeltrrd AA0A1N
113 14 a1i AA0A1i
114 15 a1i AA0A1i0
115 53 113 114 divcld AA0A1Ti
116 8 a1i AA0A12π
117 12 a1i AA0A12π0
118 115 116 117 divcan1d AA0A1Ti2π2π=Ti
119 3 oveq1i N+12=Ti2π-12+12
120 115 116 117 divcld AA0A1Ti2π
121 halfre 12
122 121 recni 12
123 npcan Ti2π12Ti2π-12+12=Ti2π
124 120 122 123 sylancl AA0A1Ti2π-12+12=Ti2π
125 119 124 eqtrid AA0A1N+12=Ti2π
126 112 zred AA0A1N
127 readdcl N12N+12
128 126 121 127 sylancl AA0A1N+12
129 125 128 eqeltrrd AA0A1Ti2π
130 remulcl Ti2π2πTi2π2π
131 129 7 130 sylancl AA0A1Ti2π2π
132 118 131 eqeltrrd AA0A1Ti
133 112 132 jca AA0A1NTi