Step | Hyp | Ref
| Expression |
1 | | tru 1487 |
. 2
|
2 | | fveq2 6191 |
. . 3
|
3 | | fveq2 6191 |
. . 3
|
4 | | fveq2 6191 |
. . 3
|
5 | | ioossre 12235 |
. . 3
|
6 | | elioore 12205 |
. . . . 5
|
7 | 6 | recnd 10068 |
. . . . . 6
|
8 | 6 | rered 13964 |
. . . . . . 7
|
9 | | id 22 |
. . . . . . 7
|
10 | 8, 9 | eqeltrd 2701 |
. . . . . 6
|
11 | | cosne0 24276 |
. . . . . 6
|
12 | 7, 10, 11 | syl2anc 693 |
. . . . 5
|
13 | 6, 12 | retancld 14875 |
. . . 4
|
14 | 13 | adantl 482 |
. . 3
|
15 | 6 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
|
16 | 15 | adantr 481 |
. . . . . . . . . . 11
|
17 | 16 | recnd 10068 |
. . . . . . . . . 10
|
18 | 17 | negnegd 10383 |
. . . . . . . . 9
|
19 | 18 | fveq2d 6195 |
. . . . . . . 8
|
20 | 17 | negcld 10379 |
. . . . . . . . 9
|
21 | | cosneg 14877 |
. . . . . . . . . . 11
|
22 | 17, 21 | syl 17 |
. . . . . . . . . 10
|
23 | | simpl1 1064 |
. . . . . . . . . . 11
|
24 | 23, 12 | syl 17 |
. . . . . . . . . 10
|
25 | 22, 24 | eqnetrd 2861 |
. . . . . . . . 9
|
26 | | tanneg 14878 |
. . . . . . . . 9
|
27 | 20, 25, 26 | syl2anc 693 |
. . . . . . . 8
|
28 | 19, 27 | eqtr3d 2658 |
. . . . . . 7
|
29 | 15 | adantr 481 |
. . . . . . . . . . . . 13
|
30 | 29 | renegcld 10457 |
. . . . . . . . . . . 12
|
31 | 25 | adantrr 753 |
. . . . . . . . . . . 12
|
32 | 30, 31 | retancld 14875 |
. . . . . . . . . . 11
|
33 | 32 | renegcld 10457 |
. . . . . . . . . 10
|
34 | | 0red 10041 |
. . . . . . . . . 10
|
35 | | simp2 1062 |
. . . . . . . . . . . . 13
|
36 | 5, 35 | sseldi 3601 |
. . . . . . . . . . . 12
|
37 | 36 | adantr 481 |
. . . . . . . . . . 11
|
38 | | simpl2 1065 |
. . . . . . . . . . . 12
|
39 | | elioore 12205 |
. . . . . . . . . . . . . 14
|
40 | 39 | recnd 10068 |
. . . . . . . . . . . . 13
|
41 | 39 | rered 13964 |
. . . . . . . . . . . . . 14
|
42 | | id 22 |
. . . . . . . . . . . . . 14
|
43 | 41, 42 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
44 | | cosne0 24276 |
. . . . . . . . . . . . 13
|
45 | 40, 43, 44 | syl2anc 693 |
. . . . . . . . . . . 12
|
46 | 38, 45 | syl 17 |
. . . . . . . . . . 11
|
47 | 37, 46 | retancld 14875 |
. . . . . . . . . 10
|
48 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
49 | 29 | lt0neg1d 10597 |
. . . . . . . . . . . . . . 15
|
50 | 48, 49 | mpbid 222 |
. . . . . . . . . . . . . 14
|
51 | | simpl1 1064 |
. . . . . . . . . . . . . . . . 17
|
52 | | eliooord 12233 |
. . . . . . . . . . . . . . . . 17
|
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . 16
|
54 | 53 | simpld 475 |
. . . . . . . . . . . . . . 15
|
55 | | halfpire 24216 |
. . . . . . . . . . . . . . . 16
|
56 | | ltnegcon1 10529 |
. . . . . . . . . . . . . . . 16
|
57 | 55, 29, 56 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
58 | 54, 57 | mpbid 222 |
. . . . . . . . . . . . . 14
|
59 | | 0xr 10086 |
. . . . . . . . . . . . . . 15
|
60 | 55 | rexri 10097 |
. . . . . . . . . . . . . . 15
|
61 | | elioo2 12216 |
. . . . . . . . . . . . . . 15
|
62 | 59, 60, 61 | mp2an 708 |
. . . . . . . . . . . . . 14
|
63 | 30, 50, 58, 62 | syl3anbrc 1246 |
. . . . . . . . . . . . 13
|
64 | | tanrpcl 24256 |
. . . . . . . . . . . . 13
|
65 | 63, 64 | syl 17 |
. . . . . . . . . . . 12
|
66 | 65 | rpgt0d 11875 |
. . . . . . . . . . 11
|
67 | 32 | lt0neg2d 10598 |
. . . . . . . . . . 11
|
68 | 66, 67 | mpbid 222 |
. . . . . . . . . 10
|
69 | | simprr 796 |
. . . . . . . . . . . . 13
|
70 | | eliooord 12233 |
. . . . . . . . . . . . . . 15
|
71 | 38, 70 | syl 17 |
. . . . . . . . . . . . . 14
|
72 | 71 | simprd 479 |
. . . . . . . . . . . . 13
|
73 | | elioo2 12216 |
. . . . . . . . . . . . . 14
|
74 | 59, 60, 73 | mp2an 708 |
. . . . . . . . . . . . 13
|
75 | 37, 69, 72, 74 | syl3anbrc 1246 |
. . . . . . . . . . . 12
|
76 | | tanrpcl 24256 |
. . . . . . . . . . . 12
|
77 | 75, 76 | syl 17 |
. . . . . . . . . . 11
|
78 | 77 | rpgt0d 11875 |
. . . . . . . . . 10
|
79 | 33, 34, 47, 68, 78 | lttrd 10198 |
. . . . . . . . 9
|
80 | 79 | anassrs 680 |
. . . . . . . 8
|
81 | | simpl3 1066 |
. . . . . . . . . . . . 13
|
82 | 15 | adantr 481 |
. . . . . . . . . . . . . 14
|
83 | 36 | adantr 481 |
. . . . . . . . . . . . . 14
|
84 | 82, 83 | ltnegd 10605 |
. . . . . . . . . . . . 13
|
85 | 81, 84 | mpbid 222 |
. . . . . . . . . . . 12
|
86 | 83 | renegcld 10457 |
. . . . . . . . . . . . . 14
|
87 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
88 | 83 | le0neg1d 10599 |
. . . . . . . . . . . . . . 15
|
89 | 87, 88 | mpbid 222 |
. . . . . . . . . . . . . 14
|
90 | | simpl2 1065 |
. . . . . . . . . . . . . . . . 17
|
91 | 90, 70 | syl 17 |
. . . . . . . . . . . . . . . 16
|
92 | 91 | simpld 475 |
. . . . . . . . . . . . . . 15
|
93 | | ltnegcon1 10529 |
. . . . . . . . . . . . . . . 16
|
94 | 55, 83, 93 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
95 | 92, 94 | mpbid 222 |
. . . . . . . . . . . . . 14
|
96 | | 0re 10040 |
. . . . . . . . . . . . . . 15
|
97 | | elico2 12237 |
. . . . . . . . . . . . . . 15
|
98 | 96, 60, 97 | mp2an 708 |
. . . . . . . . . . . . . 14
|
99 | 86, 89, 95, 98 | syl3anbrc 1246 |
. . . . . . . . . . . . 13
|
100 | 82 | renegcld 10457 |
. . . . . . . . . . . . . 14
|
101 | | simp3 1063 |
. . . . . . . . . . . . . . . . . 18
|
102 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . 19
|
103 | | ltletr 10129 |
. . . . . . . . . . . . . . . . . . 19
|
104 | 15, 36, 102, 103 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
105 | 101, 104 | mpand 711 |
. . . . . . . . . . . . . . . . 17
|
106 | 105 | imp 445 |
. . . . . . . . . . . . . . . 16
|
107 | | ltle 10126 |
. . . . . . . . . . . . . . . . 17
|
108 | 82, 96, 107 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
109 | 106, 108 | mpd 15 |
. . . . . . . . . . . . . . 15
|
110 | 82 | le0neg1d 10599 |
. . . . . . . . . . . . . . 15
|
111 | 109, 110 | mpbid 222 |
. . . . . . . . . . . . . 14
|
112 | | simpl1 1064 |
. . . . . . . . . . . . . . . . 17
|
113 | 112, 52 | syl 17 |
. . . . . . . . . . . . . . . 16
|
114 | 113 | simpld 475 |
. . . . . . . . . . . . . . 15
|
115 | 55, 82, 56 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
116 | 114, 115 | mpbid 222 |
. . . . . . . . . . . . . 14
|
117 | | elico2 12237 |
. . . . . . . . . . . . . . 15
|
118 | 96, 60, 117 | mp2an 708 |
. . . . . . . . . . . . . 14
|
119 | 100, 111,
116, 118 | syl3anbrc 1246 |
. . . . . . . . . . . . 13
|
120 | | tanord1 24283 |
. . . . . . . . . . . . 13
|
121 | 99, 119, 120 | syl2anc 693 |
. . . . . . . . . . . 12
|
122 | 85, 121 | mpbid 222 |
. . . . . . . . . . 11
|
123 | 83 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
124 | | cosneg 14877 |
. . . . . . . . . . . . . . 15
|
125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . 14
|
126 | 90, 45 | syl 17 |
. . . . . . . . . . . . . 14
|
127 | 125, 126 | eqnetrd 2861 |
. . . . . . . . . . . . 13
|
128 | 86, 127 | retancld 14875 |
. . . . . . . . . . . 12
|
129 | 106, 25 | syldan 487 |
. . . . . . . . . . . . 13
|
130 | 100, 129 | retancld 14875 |
. . . . . . . . . . . 12
|
131 | 128, 130 | ltnegd 10605 |
. . . . . . . . . . 11
|
132 | 122, 131 | mpbid 222 |
. . . . . . . . . 10
|
133 | 123 | negnegd 10383 |
. . . . . . . . . . . 12
|
134 | 133 | fveq2d 6195 |
. . . . . . . . . . 11
|
135 | 123 | negcld 10379 |
. . . . . . . . . . . 12
|
136 | | tanneg 14878 |
. . . . . . . . . . . 12
|
137 | 135, 127,
136 | syl2anc 693 |
. . . . . . . . . . 11
|
138 | 134, 137 | eqtr3d 2658 |
. . . . . . . . . 10
|
139 | 132, 138 | breqtrrd 4681 |
. . . . . . . . 9
|
140 | 139 | adantlr 751 |
. . . . . . . 8
|
141 | | 0red 10041 |
. . . . . . . 8
|
142 | | simpl2 1065 |
. . . . . . . . 9
|
143 | 5, 142 | sseldi 3601 |
. . . . . . . 8
|
144 | 80, 140, 141, 143 | ltlecasei 10145 |
. . . . . . 7
|
145 | 28, 144 | eqbrtrd 4675 |
. . . . . 6
|
146 | | simpl3 1066 |
. . . . . . 7
|
147 | 15 | adantr 481 |
. . . . . . . . 9
|
148 | | simpr 477 |
. . . . . . . . 9
|
149 | | simpl1 1064 |
. . . . . . . . . . 11
|
150 | 149, 52 | syl 17 |
. . . . . . . . . 10
|
151 | 150 | simprd 479 |
. . . . . . . . 9
|
152 | | elico2 12237 |
. . . . . . . . . 10
|
153 | 96, 60, 152 | mp2an 708 |
. . . . . . . . 9
|
154 | 147, 148,
151, 153 | syl3anbrc 1246 |
. . . . . . . 8
|
155 | | simpl2 1065 |
. . . . . . . . . 10
|
156 | 5, 155 | sseldi 3601 |
. . . . . . . . 9
|
157 | | 0red 10041 |
. . . . . . . . . 10
|
158 | 147, 156,
146 | ltled 10185 |
. . . . . . . . . 10
|
159 | 157, 147,
156, 148, 158 | letrd 10194 |
. . . . . . . . 9
|
160 | 155, 70 | syl 17 |
. . . . . . . . . 10
|
161 | 160 | simprd 479 |
. . . . . . . . 9
|
162 | | elico2 12237 |
. . . . . . . . . 10
|
163 | 96, 60, 162 | mp2an 708 |
. . . . . . . . 9
|
164 | 156, 159,
161, 163 | syl3anbrc 1246 |
. . . . . . . 8
|
165 | | tanord1 24283 |
. . . . . . . 8
|
166 | 154, 164,
165 | syl2anc 693 |
. . . . . . 7
|
167 | 146, 166 | mpbid 222 |
. . . . . 6
|
168 | 145, 167,
15, 102 | ltlecasei 10145 |
. . . . 5
|
169 | 168 | 3expia 1267 |
. . . 4
|
170 | 169 | adantl 482 |
. . 3
|
171 | 2, 3, 4, 5, 14, 170 | ltord1 10554 |
. 2
|
172 | 1, 171 | mpan 706 |
1
|