Proof of Theorem logcnlem3
Step | Hyp | Ref
| Expression |
1 | | pire 24210 |
. . . . . 6
|
2 | 1 | renegcli 10342 |
. . . . 5
|
3 | 2 | a1i 11 |
. . . 4
|
4 | | logcnlem.b |
. . . . . . . 8
|
5 | | logcn.d |
. . . . . . . . . 10
|
6 | 5 | ellogdm 24385 |
. . . . . . . . 9
|
7 | 6 | simplbi 476 |
. . . . . . . 8
|
8 | 4, 7 | syl 17 |
. . . . . . 7
|
9 | 5 | logdmn0 24386 |
. . . . . . . 8
|
10 | 4, 9 | syl 17 |
. . . . . . 7
|
11 | 8, 10 | logcld 24317 |
. . . . . 6
|
12 | 11 | imcld 13935 |
. . . . 5
|
13 | 12 | adantr 481 |
. . . 4
|
14 | | logcnlem.a |
. . . . . . . . 9
|
15 | 5 | ellogdm 24385 |
. . . . . . . . . 10
|
16 | 15 | simplbi 476 |
. . . . . . . . 9
|
17 | 14, 16 | syl 17 |
. . . . . . . 8
|
18 | 5 | logdmn0 24386 |
. . . . . . . . 9
|
19 | 14, 18 | syl 17 |
. . . . . . . 8
|
20 | 17, 19 | logcld 24317 |
. . . . . . 7
|
21 | 20 | imcld 13935 |
. . . . . 6
|
22 | 12, 21 | resubcld 10458 |
. . . . 5
|
23 | 22 | adantr 481 |
. . . 4
|
24 | 8, 10 | logimcld 24318 |
. . . . . 6
|
25 | 24 | simpld 475 |
. . . . 5
|
26 | 25 | adantr 481 |
. . . 4
|
27 | 12 | recnd 10068 |
. . . . . . 7
|
28 | 27 | adantr 481 |
. . . . . 6
|
29 | 28 | subid1d 10381 |
. . . . 5
|
30 | 21 | adantr 481 |
. . . . . 6
|
31 | | 0red 10041 |
. . . . . 6
|
32 | | argimlt0 24359 |
. . . . . . . . 9
|
33 | 17, 32 | sylan 488 |
. . . . . . . 8
|
34 | | eliooord 12233 |
. . . . . . . 8
|
35 | 33, 34 | syl 17 |
. . . . . . 7
|
36 | 35 | simprd 479 |
. . . . . 6
|
37 | 30, 31, 13, 36 | ltsub2dd 10640 |
. . . . 5
|
38 | 29, 37 | eqbrtrrd 4677 |
. . . 4
|
39 | 3, 13, 23, 26, 38 | lttrd 10198 |
. . 3
|
40 | 25 | adantr 481 |
. . . 4
|
41 | | reim0b 13859 |
. . . . . . . . . . 11
|
42 | 17, 41 | syl 17 |
. . . . . . . . . 10
|
43 | 15 | simprbi 480 |
. . . . . . . . . . 11
|
44 | 14, 43 | syl 17 |
. . . . . . . . . 10
|
45 | 42, 44 | sylbird 250 |
. . . . . . . . 9
|
46 | 45 | imp 445 |
. . . . . . . 8
|
47 | 46 | relogcld 24369 |
. . . . . . 7
|
48 | 47 | reim0d 13965 |
. . . . . 6
|
49 | 48 | oveq2d 6666 |
. . . . 5
|
50 | 27 | subid1d 10381 |
. . . . . 6
|
51 | 50 | adantr 481 |
. . . . 5
|
52 | 49, 51 | eqtrd 2656 |
. . . 4
|
53 | 40, 52 | breqtrrd 4681 |
. . 3
|
54 | 2 | a1i 11 |
. . . 4
|
55 | 21 | renegcld 10457 |
. . . . 5
|
56 | 55 | adantr 481 |
. . . 4
|
57 | 22 | adantr 481 |
. . . 4
|
58 | | argimgt0 24358 |
. . . . . . . 8
|
59 | 17, 58 | sylan 488 |
. . . . . . 7
|
60 | | eliooord 12233 |
. . . . . . 7
|
61 | 59, 60 | syl 17 |
. . . . . 6
|
62 | 61 | simprd 479 |
. . . . 5
|
63 | | ltneg 10528 |
. . . . . . 7
|
64 | 21, 1, 63 | sylancl 694 |
. . . . . 6
|
65 | 64 | adantr 481 |
. . . . 5
|
66 | 62, 65 | mpbid 222 |
. . . 4
|
67 | | df-neg 10269 |
. . . . 5
|
68 | 8 | adantr 481 |
. . . . . . . . 9
|
69 | 17, 8 | imsubd 13957 |
. . . . . . . . . . . . 13
|
70 | 69 | adantr 481 |
. . . . . . . . . . . 12
|
71 | 17, 8 | subcld 10392 |
. . . . . . . . . . . . . . 15
|
72 | 71 | imcld 13935 |
. . . . . . . . . . . . . 14
|
73 | 72 | adantr 481 |
. . . . . . . . . . . . 13
|
74 | 71 | abscld 14175 |
. . . . . . . . . . . . . 14
|
75 | 74 | adantr 481 |
. . . . . . . . . . . . 13
|
76 | 17 | adantr 481 |
. . . . . . . . . . . . . 14
|
77 | 76 | imcld 13935 |
. . . . . . . . . . . . 13
|
78 | | absimle 14049 |
. . . . . . . . . . . . . . . . 17
|
79 | 71, 78 | syl 17 |
. . . . . . . . . . . . . . . 16
|
80 | 72, 74 | absled 14169 |
. . . . . . . . . . . . . . . 16
|
81 | 79, 80 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
82 | 81 | simprd 479 |
. . . . . . . . . . . . . 14
|
83 | 82 | adantr 481 |
. . . . . . . . . . . . 13
|
84 | | logcnlem.s |
. . . . . . . . . . . . . . . . . 18
|
85 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . . 20
|
86 | 85 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
87 | 17 | imcld 13935 |
. . . . . . . . . . . . . . . . . . . . . 22
|
88 | 87 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
|
89 | 88 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . 20
|
90 | 89 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
91 | 86, 90 | ifclda 4120 |
. . . . . . . . . . . . . . . . . 18
|
92 | 84, 91 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . 17
|
93 | | logcnlem.t |
. . . . . . . . . . . . . . . . . 18
|
94 | 17 | abscld 14175 |
. . . . . . . . . . . . . . . . . . 19
|
95 | | logcnlem.r |
. . . . . . . . . . . . . . . . . . . . 21
|
96 | 95 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | | 1rp 11836 |
. . . . . . . . . . . . . . . . . . . . 21
|
98 | | rpaddcl 11854 |
. . . . . . . . . . . . . . . . . . . . 21
|
99 | 97, 95, 98 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
|
100 | 96, 99 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . . . . 19
|
101 | 94, 100 | remulcld 10070 |
. . . . . . . . . . . . . . . . . 18
|
102 | 93, 101 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . 17
|
103 | 92, 102 | ifcld 4131 |
. . . . . . . . . . . . . . . 16
|
104 | | logcnlem.l |
. . . . . . . . . . . . . . . 16
|
105 | | min1 12020 |
. . . . . . . . . . . . . . . . 17
|
106 | 92, 102, 105 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
107 | 74, 103, 92, 104, 106 | ltletrd 10197 |
. . . . . . . . . . . . . . 15
|
108 | 107 | adantr 481 |
. . . . . . . . . . . . . 14
|
109 | | gt0ne0 10493 |
. . . . . . . . . . . . . . . . 17
|
110 | 87, 109 | sylan 488 |
. . . . . . . . . . . . . . . 16
|
111 | 85, 42 | syl5ib 234 |
. . . . . . . . . . . . . . . . . . 19
|
112 | 111 | necon3ad 2807 |
. . . . . . . . . . . . . . . . . 18
|
113 | 112 | imp 445 |
. . . . . . . . . . . . . . . . 17
|
114 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . 18
|
115 | 84, 114 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
|
116 | 113, 115 | syl 17 |
. . . . . . . . . . . . . . . 16
|
117 | 110, 116 | syldan 487 |
. . . . . . . . . . . . . . 15
|
118 | | 0re 10040 |
. . . . . . . . . . . . . . . . . 18
|
119 | | ltle 10126 |
. . . . . . . . . . . . . . . . . 18
|
120 | 118, 87, 119 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
|
121 | 120 | imp 445 |
. . . . . . . . . . . . . . . 16
|
122 | 77, 121 | absidd 14161 |
. . . . . . . . . . . . . . 15
|
123 | 117, 122 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
124 | 108, 123 | breqtrd 4679 |
. . . . . . . . . . . . 13
|
125 | 73, 75, 77, 83, 124 | lelttrd 10195 |
. . . . . . . . . . . 12
|
126 | 70, 125 | eqbrtrrd 4677 |
. . . . . . . . . . 11
|
127 | 88 | adantr 481 |
. . . . . . . . . . . 12
|
128 | 127 | subid1d 10381 |
. . . . . . . . . . 11
|
129 | 126, 128 | breqtrrd 4681 |
. . . . . . . . . 10
|
130 | | 0red 10041 |
. . . . . . . . . . . 12
|
131 | 8 | imcld 13935 |
. . . . . . . . . . . 12
|
132 | 130, 131,
87 | ltsub2d 10637 |
. . . . . . . . . . 11
|
133 | 132 | adantr 481 |
. . . . . . . . . 10
|
134 | 129, 133 | mpbird 247 |
. . . . . . . . 9
|
135 | | argimgt0 24358 |
. . . . . . . . 9
|
136 | 68, 134, 135 | syl2anc 693 |
. . . . . . . 8
|
137 | | eliooord 12233 |
. . . . . . . 8
|
138 | 136, 137 | syl 17 |
. . . . . . 7
|
139 | 138 | simpld 475 |
. . . . . 6
|
140 | 130, 12, 21 | ltsub1d 10636 |
. . . . . . 7
|
141 | 140 | adantr 481 |
. . . . . 6
|
142 | 139, 141 | mpbid 222 |
. . . . 5
|
143 | 67, 142 | syl5eqbr 4688 |
. . . 4
|
144 | 54, 56, 57, 66, 143 | lttrd 10198 |
. . 3
|
145 | | lttri4 10122 |
. . . 4
|
146 | 87, 118, 145 | sylancl 694 |
. . 3
|
147 | 39, 53, 144, 146 | mpjao3dan 1395 |
. 2
|
148 | 1 | a1i 11 |
. . . 4
|
149 | 30 | renegcld 10457 |
. . . . 5
|
150 | 8 | adantr 481 |
. . . . . . . . . 10
|
151 | 88 | adantr 481 |
. . . . . . . . . . . . 13
|
152 | 151 | subid1d 10381 |
. . . . . . . . . . . 12
|
153 | 87 | adantr 481 |
. . . . . . . . . . . . . 14
|
154 | 74 | renegcld 10457 |
. . . . . . . . . . . . . . 15
|
155 | 154 | adantr 481 |
. . . . . . . . . . . . . 14
|
156 | 72 | adantr 481 |
. . . . . . . . . . . . . 14
|
157 | 74 | adantr 481 |
. . . . . . . . . . . . . . 15
|
158 | 107 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
159 | 118 | ltnri 10146 |
. . . . . . . . . . . . . . . . . . . 20
|
160 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
|
161 | 159, 160 | mtbiri 317 |
. . . . . . . . . . . . . . . . . . 19
|
162 | 161 | necon2ai 2823 |
. . . . . . . . . . . . . . . . . 18
|
163 | 162, 116 | sylan2 491 |
. . . . . . . . . . . . . . . . 17
|
164 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . . 20
|
165 | 87, 118, 164 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
|
166 | 165 | imp 445 |
. . . . . . . . . . . . . . . . . 18
|
167 | 153, 166 | absnidd 14152 |
. . . . . . . . . . . . . . . . 17
|
168 | 163, 167 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
169 | 158, 168 | breqtrd 4679 |
. . . . . . . . . . . . . . 15
|
170 | 157, 153,
169 | ltnegcon2d 10608 |
. . . . . . . . . . . . . 14
|
171 | 81 | simpld 475 |
. . . . . . . . . . . . . . 15
|
172 | 171 | adantr 481 |
. . . . . . . . . . . . . 14
|
173 | 153, 155,
156, 170, 172 | ltletrd 10197 |
. . . . . . . . . . . . 13
|
174 | 69 | adantr 481 |
. . . . . . . . . . . . 13
|
175 | 173, 174 | breqtrd 4679 |
. . . . . . . . . . . 12
|
176 | 152, 175 | eqbrtrd 4675 |
. . . . . . . . . . 11
|
177 | 150 | imcld 13935 |
. . . . . . . . . . . 12
|
178 | 177, 31, 153 | ltsub2d 10637 |
. . . . . . . . . . 11
|
179 | 176, 178 | mpbird 247 |
. . . . . . . . . 10
|
180 | | argimlt0 24359 |
. . . . . . . . . 10
|
181 | 150, 179,
180 | syl2anc 693 |
. . . . . . . . 9
|
182 | | eliooord 12233 |
. . . . . . . . 9
|
183 | 181, 182 | syl 17 |
. . . . . . . 8
|
184 | 183 | simprd 479 |
. . . . . . 7
|
185 | 13, 31, 30, 184 | ltsub1dd 10639 |
. . . . . 6
|
186 | 185, 67 | syl6breqr 4695 |
. . . . 5
|
187 | 35 | simpld 475 |
. . . . . 6
|
188 | | ltnegcon1 10529 |
. . . . . . 7
|
189 | 1, 30, 188 | sylancr 695 |
. . . . . 6
|
190 | 187, 189 | mpbid 222 |
. . . . 5
|
191 | 23, 149, 148, 186, 190 | lttrd 10198 |
. . . 4
|
192 | 23, 148, 191 | ltled 10185 |
. . 3
|
193 | 24 | simprd 479 |
. . . . 5
|
194 | 193 | adantr 481 |
. . . 4
|
195 | 52, 194 | eqbrtrd 4675 |
. . 3
|
196 | 1 | a1i 11 |
. . . 4
|
197 | 12 | adantr 481 |
. . . . 5
|
198 | | 0red 10041 |
. . . . . . 7
|
199 | 21 | adantr 481 |
. . . . . . 7
|
200 | 61 | simpld 475 |
. . . . . . 7
|
201 | 198, 199,
197, 200 | ltsub2dd 10640 |
. . . . . 6
|
202 | 27 | adantr 481 |
. . . . . . 7
|
203 | 202 | subid1d 10381 |
. . . . . 6
|
204 | 201, 203 | breqtrd 4679 |
. . . . 5
|
205 | 138 | simprd 479 |
. . . . 5
|
206 | 57, 197, 196, 204, 205 | lttrd 10198 |
. . . 4
|
207 | 57, 196, 206 | ltled 10185 |
. . 3
|
208 | 192, 195,
207, 146 | mpjao3dan 1395 |
. 2
|
209 | 147, 208 | jca 554 |
1
|