Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lvsovso Unicode version

Theorem lvsovso 25729
 Description: If the limit values of two convergent numerical functions are strictly ordered, the values of the functions are strictly ordered for some element of the filter. Bourbaki TG IV.18 prop. 2. (Contributed by FL, 6-Dec-2010.) (Revised by Mario Carneiro, 8-Aug-2015.)
Hypotheses
Ref Expression
lvsovso.l1
lvsovso.l2
lvsovso.j
Assertion
Ref Expression
lvsovso
Distinct variable groups:   ,,   ,,   ,,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem lvsovso
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl1 958 . . . 4
2 simpl2 959 . . . 4
31, 2jca 518 . . 3
4 simpr1 961 . . 3
5 lvsovso.l2 . . . . . . . . . . . . . . 15
6 lvsovso.j . . . . . . . . . . . . . . 15
75, 6limnumrr 25725 . . . . . . . . . . . . . 14
87recnd 8877 . . . . . . . . . . . . 13
983expia 1153 . . . . . . . . . . . 12
109com12 27 . . . . . . . . . . 11
11103ad2ant2 977 . . . . . . . . . 10
1211com12 27 . . . . . . . . 9
13123adant2 974 . . . . . . . 8
1413imp 418 . . . . . . 7
15 lvsovso.l1 . . . . . . . . . . . . . . 15
1615, 6limnumrr 25725 . . . . . . . . . . . . . 14
1716recnd 8877 . . . . . . . . . . . . 13
18173expia 1153 . . . . . . . . . . . 12
1918com12 27 . . . . . . . . . . 11
20193ad2ant1 976 . . . . . . . . . 10
2120com12 27 . . . . . . . . 9
22213adant3 975 . . . . . . . 8
2322imp 418 . . . . . . 7
2414, 23subcld 9173 . . . . . 6
2524abscld 11934 . . . . 5
2625rehalfcld 9974 . . . 4
27 simpr3 963 . . . . . . . 8
28163expia 1153 . . . . . . . . . . . . . 14
2928com12 27 . . . . . . . . . . . . 13
30293ad2ant1 976 . . . . . . . . . . . 12
3130com12 27 . . . . . . . . . . 11
32313adant3 975 . . . . . . . . . 10
3332imp 418 . . . . . . . . 9
3473expia 1153 . . . . . . . . . . . . . 14
3534com12 27 . . . . . . . . . . . . 13
36353ad2ant2 977 . . . . . . . . . . . 12
3736com12 27 . . . . . . . . . . 11
38373adant2 974 . . . . . . . . . 10
3938imp 418 . . . . . . . . 9
4033, 39posdifd 9375 . . . . . . . 8
4127, 40mpbid 201 . . . . . . 7
4241gt0ne0d 9353 . . . . . 6
43 absgt0 11824 . . . . . . 7
4424, 43syl 15 . . . . . 6
4542, 44mpbid 201 . . . . 5
46 halfpos2 9957 . . . . . 6
4725, 46syl 15 . . . . 5
4845, 47mpbid 201 . . . 4
4926, 48elrpd 10404 . . 3
50 simpl3 960 . . . 4
511, 50jca 518 . . 3
52 simpr2 962 . . 3
53 eqid 2296 . . . . 5
5415, 6, 53flfneicn 25728 . . . 4
55 eqid 2296 . . . . 5
565, 6, 55flfneicn 25728 . . . 4
5754, 56anim12i 549 . . 3
583, 4, 49, 51, 52, 49, 57syl33anc 1197 . 2
59 filin 17565 . . . . . . . . . . . . . . 15
60 inss1 3402 . . . . . . . . . . . . . . . . . 18
61 inss2 3403 . . . . . . . . . . . . . . . . . 18
62 imass2 5065 . . . . . . . . . . . . . . . . . . 19
63 imass2 5065 . . . . . . . . . . . . . . . . . . 19
6462, 63anim12i 549 . . . . . . . . . . . . . . . . . 18
6560, 61, 64mp2an 653 . . . . . . . . . . . . . . . . 17
66 sstr2 3199 . . . . . . . . . . . . . . . . . 18
67 sstr2 3199 . . . . . . . . . . . . . . . . . 18
6866, 67im2anan9 808 . . . . . . . . . . . . . . . . 17
6965, 68ax-mp 8 . . . . . . . . . . . . . . . 16
702ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
71 simprl1 1000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
72 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
73 filelss 17563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7471, 72, 73syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7574sselda 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
76 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7770, 75, 76syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7839adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7926adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8078, 79resubcld 9227 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8180adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8250ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
83 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8482, 75, 83syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8577, 81, 843jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . 25
86 ffun 5407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
87863ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
88733adant1 973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
89 fdm 5409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
90893ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
9188, 90sseqtr4d 3228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
9287, 91jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
93923exp 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9493impcom 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
95943adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
96 funfvima2 5770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9795, 96syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
98973imp 1145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
99 ffun 5407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
100993ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
101100adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
102733ad2antl1 1117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
103 simpl3 960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
104 fdm 5409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
105103, 104syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
106102, 105sseqtr4d 3228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
107 funfvima2 5770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
108101, 106, 107syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1091083impia 1148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
11098, 109jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1111103exp 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112111adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
113112com12 27 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
114113adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
115114imp31 421 . . . . . . . . . . . . . . . . . . . . . . . . . 26
116 recn 8843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
117 recn 8843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
118 subcl 9067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
119116, 117, 118syl2anr 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
120119abscld 11934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
121120recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
122121halfcld 9972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1231223adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1241173ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
125123, 124, 123add12d 9049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1261213adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1271262halvesd 9973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
128 resubcl 9127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
129128ancoms 439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1301293adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
131 0re 8854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
132129, 131jctil 523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1331323adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
134 posdif 9283 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
135134biimp3a 1281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
136 ltle 8926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
137133, 135, 136sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
138130, 137absidd 11921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
139127, 138eqtr2d 2329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
140116adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
141117adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
142120rehalfcld 9974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
143 recn 8843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
144143, 143jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
145 addcl 8835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
146142, 144, 1453syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
147140, 141, 1463jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1481473adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
149 subadd 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
150148, 149syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
151139, 150mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
152125, 151eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
153129recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
154153abscld 11934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
155154recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
156155halfcld 9972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
157117, 143anim12i 549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
158142, 157syldan 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
159 addcl 8835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
160158, 159syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
161140, 156, 1603jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1621613adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
163 subadd 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
164162, 163syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
165152, 164mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
16633, 39, 27, 165syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
167 ssel2 3188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
168 eliooord 10726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
169167, 168syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
170169simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
171 ssel2 3188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
172 eliooord 10726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
173171, 172syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
174173simpld 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
175170, 174anim12i 549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
176175an4s 799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
177176ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178 breq2 4043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
179178anbi1d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
180179imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
181177, 180syl5ibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
182166, 181syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
183182com12 27 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
184183adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
185184imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
186185adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26
187115, 186mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . 25
18885, 187jca 518 . . . . . . . . . . . . . . . . . . . . . . . 24
189188ex 423 . . . . . . . . . . . . . . . . . . . . . . 23
190 lttr 8915 . . . . . . . . . . . . . . . . . . . . . . . 24
191190imp 418 . . . . . . . . . . . . . . . . . . . . . . 23
192189, 191syl6 29 . . . . . . . . . . . . . . . . . . . . . 22
193192ralrimiv 2638 . . . . . . . . . . . . . . . . . . . . 21
194193ex 423 . . . . . . . . . . . . . . . . . . . 20
195 raleq 2749 . . . . . . . . . . . . . . . . . . . . . 22
196195rspcev 2897 . . . . . . . . . . . . . . . . . . . . 21
197196expcom 424 . . . . . . . . . . . . . . . . . . . 20
198194, 197syl6 29 . . . . . . . . . . . . . . . . . . 19