Proof of Theorem ang180lem3
Step | Hyp | Ref
| Expression |
1 | | 2cn 11091 |
. . . . . . . . . 10
|
2 | | picn 24211 |
. . . . . . . . . 10
|
3 | 1, 2 | mulcli 10045 |
. . . . . . . . 9
|
4 | | 2ne0 11113 |
. . . . . . . . 9
|
5 | 3, 1, 4 | divreci 10770 |
. . . . . . . 8
|
6 | 2, 1, 4 | divcan3i 10771 |
. . . . . . . 8
|
7 | 5, 6 | eqtr3i 2646 |
. . . . . . 7
|
8 | | ang180lem1.3 |
. . . . . . . . . 10
|
9 | | ang.1 |
. . . . . . . . . . . . . . . 16
|
10 | | ang180lem1.2 |
. . . . . . . . . . . . . . . 16
|
11 | 9, 10, 8 | ang180lem2 24540 |
. . . . . . . . . . . . . . 15
|
12 | 11 | simprd 479 |
. . . . . . . . . . . . . 14
|
13 | | 1e0p1 11552 |
. . . . . . . . . . . . . 14
|
14 | 12, 13 | syl6breq 4694 |
. . . . . . . . . . . . 13
|
15 | 9, 10, 8 | ang180lem1 24539 |
. . . . . . . . . . . . . . 15
|
16 | 15 | simpld 475 |
. . . . . . . . . . . . . 14
|
17 | | 0z 11388 |
. . . . . . . . . . . . . 14
|
18 | | zleltp1 11428 |
. . . . . . . . . . . . . 14
|
19 | 16, 17, 18 | sylancl 694 |
. . . . . . . . . . . . 13
|
20 | 14, 19 | mpbird 247 |
. . . . . . . . . . . 12
|
21 | 20 | adantr 481 |
. . . . . . . . . . 11
|
22 | | zlem1lt 11429 |
. . . . . . . . . . . . . 14
|
23 | 17, 16, 22 | sylancr 695 |
. . . . . . . . . . . . 13
|
24 | | df-neg 10269 |
. . . . . . . . . . . . . 14
|
25 | 24 | breq1i 4660 |
. . . . . . . . . . . . 13
|
26 | 23, 25 | syl6bbr 278 |
. . . . . . . . . . . 12
|
27 | 26 | biimpar 502 |
. . . . . . . . . . 11
|
28 | 16 | zred 11482 |
. . . . . . . . . . . . 13
|
29 | 28 | adantr 481 |
. . . . . . . . . . . 12
|
30 | | 0re 10040 |
. . . . . . . . . . . 12
|
31 | | letri3 10123 |
. . . . . . . . . . . 12
|
32 | 29, 30, 31 | sylancl 694 |
. . . . . . . . . . 11
|
33 | 21, 27, 32 | mpbir2and 957 |
. . . . . . . . . 10
|
34 | 8, 33 | syl5eqr 2670 |
. . . . . . . . 9
|
35 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . 19
|
36 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . 19
|
37 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . 19
|
38 | 35, 36, 37 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
|
39 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . 20
|
40 | 39 | necomd 2849 |
. . . . . . . . . . . . . . . . . . 19
|
41 | | subeq0 10307 |
. . . . . . . . . . . . . . . . . . . . 21
|
42 | 35, 36, 41 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
|
43 | 42 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . 19
|
44 | 40, 43 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
|
45 | 38, 44 | reccld 10794 |
. . . . . . . . . . . . . . . . 17
|
46 | 38, 44 | recne0d 10795 |
. . . . . . . . . . . . . . . . 17
|
47 | 45, 46 | logcld 24317 |
. . . . . . . . . . . . . . . 16
|
48 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . 19
|
49 | 36, 35, 48 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
|
50 | | simp2 1062 |
. . . . . . . . . . . . . . . . . 18
|
51 | 49, 36, 50 | divcld 10801 |
. . . . . . . . . . . . . . . . 17
|
52 | | subeq0 10307 |
. . . . . . . . . . . . . . . . . . . . 21
|
53 | 36, 35, 52 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . 20
|
54 | 53 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . 19
|
55 | 39, 54 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
|
56 | 49, 36, 55, 50 | divne0d 10817 |
. . . . . . . . . . . . . . . . 17
|
57 | 51, 56 | logcld 24317 |
. . . . . . . . . . . . . . . 16
|
58 | 47, 57 | addcld 10059 |
. . . . . . . . . . . . . . 15
|
59 | | logcl 24315 |
. . . . . . . . . . . . . . . 16
|
60 | 59 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
|
61 | 58, 60 | addcld 10059 |
. . . . . . . . . . . . . 14
|
62 | 10, 61 | syl5eqel 2705 |
. . . . . . . . . . . . 13
|
63 | | ax-icn 9995 |
. . . . . . . . . . . . . 14
|
64 | 63 | a1i 11 |
. . . . . . . . . . . . 13
|
65 | | ine0 10465 |
. . . . . . . . . . . . . 14
|
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
|
67 | 62, 64, 66 | divcld 10801 |
. . . . . . . . . . . 12
|
68 | 3 | a1i 11 |
. . . . . . . . . . . 12
|
69 | | pire 24210 |
. . . . . . . . . . . . . . 15
|
70 | | pipos 24212 |
. . . . . . . . . . . . . . 15
|
71 | 69, 70 | gt0ne0ii 10564 |
. . . . . . . . . . . . . 14
|
72 | 1, 2, 4, 71 | mulne0i 10670 |
. . . . . . . . . . . . 13
|
73 | 72 | a1i 11 |
. . . . . . . . . . . 12
|
74 | 67, 68, 73 | divcld 10801 |
. . . . . . . . . . 11
|
75 | 74 | adantr 481 |
. . . . . . . . . 10
|
76 | | halfcn 11247 |
. . . . . . . . . 10
|
77 | | subeq0 10307 |
. . . . . . . . . 10
|
78 | 75, 76, 77 | sylancl 694 |
. . . . . . . . 9
|
79 | 34, 78 | mpbid 222 |
. . . . . . . 8
|
80 | 67 | adantr 481 |
. . . . . . . . 9
|
81 | 3 | a1i 11 |
. . . . . . . . 9
|
82 | 76 | a1i 11 |
. . . . . . . . 9
|
83 | 72 | a1i 11 |
. . . . . . . . 9
|
84 | 80, 81, 82, 83 | divmuld 10823 |
. . . . . . . 8
|
85 | 79, 84 | mpbid 222 |
. . . . . . 7
|
86 | 7, 85 | syl5reqr 2671 |
. . . . . 6
|
87 | 62 | adantr 481 |
. . . . . . 7
|
88 | 63 | a1i 11 |
. . . . . . 7
|
89 | 2 | a1i 11 |
. . . . . . 7
|
90 | 65 | a1i 11 |
. . . . . . 7
|
91 | 87, 88, 89, 90 | divmuld 10823 |
. . . . . 6
|
92 | 86, 91 | mpbid 222 |
. . . . 5
|
93 | 92 | eqcomd 2628 |
. . . 4
|
94 | 93 | olcd 408 |
. . 3
|
95 | 2, 63 | mulneg1i 10476 |
. . . . . . 7
|
96 | 2, 63 | mulcomi 10046 |
. . . . . . . 8
|
97 | 96 | negeqi 10274 |
. . . . . . 7
|
98 | 95, 97 | eqtri 2644 |
. . . . . 6
|
99 | 76, 3 | mulneg1i 10476 |
. . . . . . . . . 10
|
100 | 35, 1, 4 | divcan1i 10769 |
. . . . . . . . . . . . 13
|
101 | 100 | oveq1i 6660 |
. . . . . . . . . . . 12
|
102 | 76, 1, 2 | mulassi 10049 |
. . . . . . . . . . . 12
|
103 | 2 | mulid2i 10043 |
. . . . . . . . . . . 12
|
104 | 101, 102,
103 | 3eqtr3i 2652 |
. . . . . . . . . . 11
|
105 | 104 | negeqi 10274 |
. . . . . . . . . 10
|
106 | 99, 105 | eqtri 2644 |
. . . . . . . . 9
|
107 | 35, 76 | negsubdii 10366 |
. . . . . . . . . . . . 13
|
108 | | 1mhlfehlf 11251 |
. . . . . . . . . . . . . 14
|
109 | 108 | negeqi 10274 |
. . . . . . . . . . . . 13
|
110 | 107, 109 | eqtr3i 2646 |
. . . . . . . . . . . 12
|
111 | | simpr 477 |
. . . . . . . . . . . . . 14
|
112 | 111, 8 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
113 | 112 | oveq1d 6665 |
. . . . . . . . . . . 12
|
114 | 110, 113 | syl5eqr 2670 |
. . . . . . . . . . 11
|
115 | | npcan 10290 |
. . . . . . . . . . . . 13
|
116 | 74, 76, 115 | sylancl 694 |
. . . . . . . . . . . 12
|
117 | 116 | adantr 481 |
. . . . . . . . . . 11
|
118 | 114, 117 | eqtrd 2656 |
. . . . . . . . . 10
|
119 | 118 | oveq1d 6665 |
. . . . . . . . 9
|
120 | 106, 119 | syl5eqr 2670 |
. . . . . . . 8
|
121 | 67, 68, 73 | divcan1d 10802 |
. . . . . . . . 9
|
122 | 121 | adantr 481 |
. . . . . . . 8
|
123 | 120, 122 | eqtrd 2656 |
. . . . . . 7
|
124 | 123 | oveq1d 6665 |
. . . . . 6
|
125 | 98, 124 | syl5eqr 2670 |
. . . . 5
|
126 | 62, 64, 66 | divcan1d 10802 |
. . . . . 6
|
127 | 126 | adantr 481 |
. . . . 5
|
128 | 125, 127 | eqtr2d 2657 |
. . . 4
|
129 | 128 | orcd 407 |
. . 3
|
130 | | df-2 11079 |
. . . . . . . 8
|
131 | 130 | negeqi 10274 |
. . . . . . 7
|
132 | | negdi2 10339 |
. . . . . . . 8
|
133 | 35, 35, 132 | mp2an 708 |
. . . . . . 7
|
134 | 131, 133 | eqtri 2644 |
. . . . . 6
|
135 | 11 | simpld 475 |
. . . . . 6
|
136 | 134, 135 | syl5eqbrr 4689 |
. . . . 5
|
137 | | neg1z 11413 |
. . . . . 6
|
138 | | zlem1lt 11429 |
. . . . . 6
|
139 | 137, 16, 138 | sylancr 695 |
. . . . 5
|
140 | 136, 139 | mpbird 247 |
. . . 4
|
141 | | neg1rr 11125 |
. . . . 5
|
142 | | leloe 10124 |
. . . . 5
|
143 | 141, 28, 142 | sylancr 695 |
. . . 4
|
144 | 140, 143 | mpbid 222 |
. . 3
|
145 | 94, 129, 144 | mpjaodan 827 |
. 2
|
146 | | ovex 6678 |
. . . 4
|
147 | 10, 146 | eqeltri 2697 |
. . 3
|
148 | 147 | elpr 4198 |
. 2
|
149 | 145, 148 | sylibr 224 |
1
|