Theorem lvsovso 15038

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.

Hypotheses

Ref	Expression
lvsovso.1	|- Y = U.F
lvsovso.2	|- L1 = U.((J fLimf F)` F1)
lvsovso.3	|- L2 = U.((J fLimf F)` F2)
lvsovso.4	|- J = (topGen` ran (,))

Assertion

Ref	Expression
lvsovso	|- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> E.a e. F A.x e. a (F1` x) < (F2` x))

Distinct variable groups:   F,a,x   a,F₁,x   a,F₂,x   x,J   x,L₁   x,L₂   x,Y

Proof of Theorem lvsovso

Step	Hyp	Ref	Expression
1		simpl1 879	. . . 4 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> F e. Fil)
2		simpl2 880	. . . 4 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> F1:Y-->RR)
3	1, 2	jca 310	. . 3 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (F e. Fil /\ F1:Y-->RR))
4		simpr1 882	. . 3 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> ((J fLimf F)` F1) =/= (/))
5		elrp 7233	. . . 4 |- (((abs` (L2 - L1)) / 2) e. RR+ <-> (((abs` (L2 - L1)) / 2) e. RR /\ 0 < ((abs` (L2 - L1)) / 2)))
6		lvsovso.1	. . . . . . . . . . . . . . 15 |- Y = U.F
7		lvsovso.3	. . . . . . . . . . . . . . 15 |- L2 = U.((J fLimf F)` F2)
8		lvsovso.4	. . . . . . . . . . . . . . 15 |- J = (topGen` ran (,))
9	6, 7, 8	limnumrr 15034	. . . . . . . . . . . . . 14 |- ((F e. Fil /\ F2:Y-->RR /\ ((J fLimf F)` F2) =/= (/)) -> L2 e. RR)
10	9	recnd 6468	. . . . . . . . . . . . 13 |- ((F e. Fil /\ F2:Y-->RR /\ ((J fLimf F)` F2) =/= (/)) -> L2 e. CC)
11	10	3expia 1069	. . . . . . . . . . . 12 |- ((F e. Fil /\ F2:Y-->RR) -> (((J fLimf F)` F2) =/= (/) -> L2 e. CC))
12	11	com12 14	. . . . . . . . . . 11 |- (((J fLimf F)` F2) =/= (/) -> ((F e. Fil /\ F2:Y-->RR) -> L2 e. CC))
13	12	3ad2ant2 898	. . . . . . . . . 10 |- ((((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2) -> ((F e. Fil /\ F2:Y-->RR) -> L2 e. CC))
14	13	com12 14	. . . . . . . . 9 |- ((F e. Fil /\ F2:Y-->RR) -> ((((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2) -> L2 e. CC))
15	14	3adant2 895	. . . . . . . 8 |- ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) -> ((((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2) -> L2 e. CC))
16	15	imp 377	. . . . . . 7 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> L2 e. CC)
17		lvsovso.2	. . . . . . . . . . . . . . 15 |- L1 = U.((J fLimf F)` F1)
18	6, 17, 8	limnumrr 15034	. . . . . . . . . . . . . 14 |- ((F e. Fil /\ F1:Y-->RR /\ ((J fLimf F)` F1) =/= (/)) -> L1 e. RR)
19	18	recnd 6468	. . . . . . . . . . . . 13 |- ((F e. Fil /\ F1:Y-->RR /\ ((J fLimf F)` F1) =/= (/)) -> L1 e. CC)
20	19	3expia 1069	. . . . . . . . . . . 12 |- ((F e. Fil /\ F1:Y-->RR) -> (((J fLimf F)` F1) =/= (/) -> L1 e. CC))
21	20	com12 14	. . . . . . . . . . 11 |- (((J fLimf F)` F1) =/= (/) -> ((F e. Fil /\ F1:Y-->RR) -> L1 e. CC))
22	21	3ad2ant1 897	. . . . . . . . . 10 |- ((((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2) -> ((F e. Fil /\ F1:Y-->RR) -> L1 e. CC))
23	22	com12 14	. . . . . . . . 9 |- ((F e. Fil /\ F1:Y-->RR) -> ((((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2) -> L1 e. CC))
24	23	3adant3 896	. . . . . . . 8 |- ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) -> ((((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2) -> L1 e. CC))
25	24	imp 377	. . . . . . 7 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> L1 e. CC)
26		subcl 6524	. . . . . . 7 |- ((L2 e. CC /\ L1 e. CC) -> (L2 - L1) e. CC)
27	16, 25, 26	syl11anc 524	. . . . . 6 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (L2 - L1) e. CC)
28		abscl 8084	. . . . . 6 |- ((L2 - L1) e. CC -> (abs` (L2 - L1)) e. RR)
29	27, 28	syl 12	. . . . 5 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (abs` (L2 - L1)) e. RR)
30		rehalfcl 7220	. . . . 5 |- ((abs` (L2 - L1)) e. RR -> ((abs` (L2 - L1)) / 2) e. RR)
31	29, 30	syl 12	. . . 4 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> ((abs` (L2 - L1)) / 2) e. RR)
32	9	3expia 1069	. . . . . . . . . . . . 13 |- ((F e. Fil /\ F2:Y-->RR) -> (((J fLimf F)` F2) =/= (/) -> L2 e. RR))
33	32	com12 14	. . . . . . . . . . . 12 |- (((J fLimf F)` F2) =/= (/) -> ((F e. Fil /\ F2:Y-->RR) -> L2 e. RR))
34	33	3ad2ant2 898	. . . . . . . . . . 11 |- ((((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2) -> ((F e. Fil /\ F2:Y-->RR) -> L2 e. RR))
35	34	com12 14	. . . . . . . . . 10 |- ((F e. Fil /\ F2:Y-->RR) -> ((((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2) -> L2 e. RR))
36	35	3adant2 895	. . . . . . . . 9 |- ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) -> ((((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2) -> L2 e. RR))
37	36	imp 377	. . . . . . . 8 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> L2 e. RR)
38	18	3expia 1069	. . . . . . . . . . . . 13 |- ((F e. Fil /\ F1:Y-->RR) -> (((J fLimf F)` F1) =/= (/) -> L1 e. RR))
39	38	com12 14	. . . . . . . . . . . 12 |- (((J fLimf F)` F1) =/= (/) -> ((F e. Fil /\ F1:Y-->RR) -> L1 e. RR))
40	39	3ad2ant1 897	. . . . . . . . . . 11 |- ((((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2) -> ((F e. Fil /\ F1:Y-->RR) -> L1 e. RR))
41	40	com12 14	. . . . . . . . . 10 |- ((F e. Fil /\ F1:Y-->RR) -> ((((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2) -> L1 e. RR))
42	41	3adant3 896	. . . . . . . . 9 |- ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) -> ((((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2) -> L1 e. RR))
43	42	imp 377	. . . . . . . 8 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> L1 e. RR)
44		resubcl 6601	. . . . . . . 8 |- ((L2 e. RR /\ L1 e. RR) -> (L2 - L1) e. RR)
45	37, 43, 44	syl11anc 524	. . . . . . 7 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (L2 - L1) e. RR)
46		simpr3 884	. . . . . . . 8 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> L1 < L2)
47		posdif 6843	. . . . . . . . 9 |- ((L1 e. RR /\ L2 e. RR) -> (L1 < L2 <-> 0 < (L2 - L1)))
48	43, 37, 47	syl11anc 524	. . . . . . . 8 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (L1 < L2 <-> 0 < (L2 - L1)))
49	46, 48	mpbid 212	. . . . . . 7 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> 0 < (L2 - L1))
50		gt0ne0 6800	. . . . . . 7 |- (((L2 - L1) e. RR /\ 0 < (L2 - L1)) -> (L2 - L1) =/= 0)
51	45, 49, 50	syl11anc 524	. . . . . 6 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (L2 - L1) =/= 0)
52		absgt0 8145	. . . . . . 7 |- ((L2 - L1) e. CC -> ((L2 - L1) =/= 0 <-> 0 < (abs` (L2 - L1))))
53	27, 52	syl 12	. . . . . 6 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> ((L2 - L1) =/= 0 <-> 0 < (abs` (L2 - L1))))
54	51, 53	mpbid 212	. . . . 5 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> 0 < (abs` (L2 - L1)))
55		halfpos2 7223	. . . . . 6 |- ((abs` (L2 - L1)) e. RR -> (0 < (abs` (L2 - L1)) <-> 0 < ((abs` (L2 - L1)) / 2)))
56	29, 55	syl 12	. . . . 5 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (0 < (abs` (L2 - L1)) <-> 0 < ((abs` (L2 - L1)) / 2)))
57	54, 56	mpbid 212	. . . 4 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> 0 < ((abs` (L2 - L1)) / 2))
58	5, 31, 57	sylanbrc 527	. . 3 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> ((abs` (L2 - L1)) / 2) e. RR+)
59		simpl3 881	. . . 4 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> F2:Y-->RR)
60	1, 59	jca 310	. . 3 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (F e. Fil /\ F2:Y-->RR))
61		simpr2 883	. . 3 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> ((J fLimf F)` F2) =/= (/))
62		eqid 1884	. . . . 5 |- ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) = ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2)))
63	6, 17, 8, 62	flimfneicn 15037	. . . 4 |- (((F e. Fil /\ F1:Y-->RR) /\ ((J fLimf F)` F1) =/= (/) /\ ((abs` (L2 - L1)) / 2) e. RR+) -> E.r e. F (F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))))
64		eqid 1884	. . . . 5 |- ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))) = ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))
65	6, 7, 8, 64	flimfneicn 15037	. . . 4 |- (((F e. Fil /\ F2:Y-->RR) /\ ((J fLimf F)` F2) =/= (/) /\ ((abs` (L2 - L1)) / 2) e. RR+) -> E.s e. F (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))))
66	63, 65	anim12i 360	. . 3 |- ((((F e. Fil /\ F1:Y-->RR) /\ ((J fLimf F)` F1) =/= (/) /\ ((abs` (L2 - L1)) / 2) e. RR+) /\ ((F e. Fil /\ F2:Y-->RR) /\ ((J fLimf F)` F2) =/= (/) /\ ((abs` (L2 - L1)) / 2) e. RR+)) -> (E.r e. F (F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ E.s e. F (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))))
67	3, 4, 58, 60, 61, 58, 66	syl33anc 1115	. 2 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (E.r e. F (F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ E.s e. F (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))))
68		filint 10269	. . . . . . . . . . . . . . 15 |- ((F e. Fil /\ r e. F /\ s e. F) -> (r i^i s) e. F)
69	2	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) /\ x e. (r i^i s)) -> F1:Y-->RR)
70		elunii 3182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((x e. (r i^i s) /\ (r i^i s) e. F) -> x e. U.F)
71	70, 6	syl6eleqr 1982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((x e. (r i^i s) /\ (r i^i s) e. F) -> x e. Y)
72	71	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((r i^i s) e. F -> (x e. (r i^i s) -> x e. Y))
73	72	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) -> (x e. (r i^i s) -> x e. Y))
74	73	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) /\ x e. (r i^i s)) -> x e. Y)
75		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((F1:Y-->RR /\ x e. Y) -> (F1` x) e. RR)
76	69, 74, 75	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) /\ x e. (r i^i s)) -> (F1` x) e. RR)
77	37	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) -> L2 e. RR)
78	31	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) -> ((abs` (L2 - L1)) / 2) e. RR)
79		resubcl 6601	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((L2 e. RR /\ ((abs` (L2 - L1)) / 2) e. RR) -> (L2 - ((abs` (L2 - L1)) / 2)) e. RR)
80	77, 78, 79	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) -> (L2 - ((abs` (L2 - L1)) / 2)) e. RR)
81	80	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) /\ x e. (r i^i s)) -> (L2 - ((abs` (L2 - L1)) / 2)) e. RR)
82	59	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) /\ x e. (r i^i s)) -> F2:Y-->RR)
83		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((F2:Y-->RR /\ x e. Y) -> (F2` x) e. RR)
84	82, 74, 83	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) /\ x e. (r i^i s)) -> (F2` x) e. RR)
85	76, 81, 84	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) /\ x e. (r i^i s)) -> ((F1` x) e. RR /\ (L2 - ((abs` (L2 - L1)) / 2)) e. RR /\ (F2` x) e. RR))
86		ffun 4565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (F1:Y-->RR -> Fun F1)
87	86	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((F1:Y-->RR /\ F e. Fil /\ (r i^i s) e. F) -> Fun F1)
88		elssuni 3206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((r i^i s) e. F -> (r i^i s) C_ U.F)
89		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (U.F = Y -> ((r i^i s) C_ U.F <-> (r i^i s) C_ Y))
90	89	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (U.F = Y -> ((r i^i s) C_ U.F -> (r i^i s) C_ Y))
91	90	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (Y = U.F -> ((r i^i s) C_ U.F -> (r i^i s) C_ Y))
92	6, 91	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((r i^i s) C_ U.F -> (r i^i s) C_ Y)
93		fdm 4567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (F1:Y-->RR -> dom F1 = Y)
94	93	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (F1:Y-->RR -> Y = dom F1)
95	94	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (F1:Y-->RR -> ((r i^i s) C_ Y <-> (r i^i s) C_ dom F1))
96	95	biimpcd 172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((r i^i s) C_ Y -> (F1:Y-->RR -> (r i^i s) C_ dom F1))
97	88, 92, 96	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((r i^i s) e. F -> (F1:Y-->RR -> (r i^i s) C_ dom F1))
98	97	impcom 378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((F1:Y-->RR /\ (r i^i s) e. F) -> (r i^i s) C_ dom F1)
99	98	3adant2 895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((F1:Y-->RR /\ F e. Fil /\ (r i^i s) e. F) -> (r i^i s) C_ dom F1)
100	87, 99	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((F1:Y-->RR /\ F e. Fil /\ (r i^i s) e. F) -> (Fun F1 /\ (r i^i s) C_ dom F1))
101	100	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (F1:Y-->RR -> (F e. Fil -> ((r i^i s) e. F -> (Fun F1 /\ (r i^i s) C_ dom F1))))
102	101	impcom 378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((F e. Fil /\ F1:Y-->RR) -> ((r i^i s) e. F -> (Fun F1 /\ (r i^i s) C_ dom F1)))
103	102	3adant3 896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) -> ((r i^i s) e. F -> (Fun F1 /\ (r i^i s) C_ dom F1)))
104		funfvima2 4829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((Fun F1 /\ (r i^i s) C_ dom F1) -> (x e. (r i^i s) -> (F1` x) e. (F1"(r i^i s))))
105	103, 104	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) -> ((r i^i s) e. F -> (x e. (r i^i s) -> (F1` x) e. (F1"(r i^i s)))))
106	105	3imp 1061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (r i^i s) e. F /\ x e. (r i^i s)) -> (F1` x) e. (F1"(r i^i s)))
107		ffun 4565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (F2:Y-->RR -> Fun F2)
108	107	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) -> Fun F2)
109	108	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (r i^i s) e. F) -> Fun F2)
110		fdm 4567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (F2:Y-->RR -> dom F2 = Y)
111	110	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (F2:Y-->RR -> Y = dom F2)
112	111	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (F2:Y-->RR -> ((r i^i s) C_ Y <-> (r i^i s) C_ dom F2))
113	112	biimpcd 172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((r i^i s) C_ Y -> (F2:Y-->RR -> (r i^i s) C_ dom F2))
114	88, 92, 113	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((r i^i s) e. F -> (F2:Y-->RR -> (r i^i s) C_ dom F2))
115	114	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (F2:Y-->RR -> ((r i^i s) e. F -> (r i^i s) C_ dom F2))
116	115	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) -> ((r i^i s) e. F -> (r i^i s) C_ dom F2))
117	116	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (r i^i s) e. F) -> (r i^i s) C_ dom F2)
118		funfvima2 4829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((Fun F2 /\ (r i^i s) C_ dom F2) -> (x e. (r i^i s) -> (F2` x) e. (F2"(r i^i s))))
119	109, 117, 118	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (r i^i s) e. F) -> (x e. (r i^i s) -> (F2` x) e. (F2"(r i^i s))))
120	119	3impia 1064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (r i^i s) e. F /\ x e. (r i^i s)) -> (F2` x) e. (F2"(r i^i s)))
121	106, 120	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (r i^i s) e. F /\ x e. (r i^i s)) -> ((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))))
122	121	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) -> ((r i^i s) e. F -> (x e. (r i^i s) -> ((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))))))
123	122	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> ((r i^i s) e. F -> (x e. (r i^i s) -> ((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))))))
124	123	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((r i^i s) e. F -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (x e. (r i^i s) -> ((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))))))
125	124	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (x e. (r i^i s) -> ((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))))))
126	125	imp31 389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) /\ x e. (r i^i s)) -> ((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))))
127		recn 6466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (L2 e. RR -> L2 e. CC)
128		recn 6466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (L1 e. RR -> L1 e. CC)
129	127, 128	anim12i 360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((L2 e. RR /\ L1 e. RR) -> (L2 e. CC /\ L1 e. CC))
130	129	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((L1 e. RR /\ L2 e. RR) -> (L2 e. CC /\ L1 e. CC))
131	130, 26, 28	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((L1 e. RR /\ L2 e. RR) -> (abs` (L2 - L1)) e. RR)
132		recn 6466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((abs` (L2 - L1)) e. RR -> (abs` (L2 - L1)) e. CC)
133		halfcl 7219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((abs` (L2 - L1)) e. CC -> ((abs` (L2 - L1)) / 2) e. CC)
134	131, 132, 133	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((L1 e. RR /\ L2 e. RR) -> ((abs` (L2 - L1)) / 2) e. CC)
135	134	3adant3 896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> ((abs` (L2 - L1)) / 2) e. CC)
136	128	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> L1 e. CC)
137		add12 6489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((abs` (L2 - L1)) / 2) e. CC /\ L1 e. CC /\ ((abs` (L2 - L1)) / 2) e. CC) -> (((abs` (L2 - L1)) / 2) + (L1 + ((abs` (L2 - L1)) / 2))) = (L1 + (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2))))
138	135, 136, 135, 137	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> (((abs` (L2 - L1)) / 2) + (L1 + ((abs` (L2 - L1)) / 2))) = (L1 + (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2))))
139	130, 26	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((L1 e. RR /\ L2 e. RR) -> (L2 - L1) e. CC)
140	139, 28, 132	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((L1 e. RR /\ L2 e. RR) -> (abs` (L2 - L1)) e. CC)
141	140	3adant3 896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> (abs` (L2 - L1)) e. CC)
142		2halves 7225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((abs` (L2 - L1)) e. CC -> (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2)) = (abs` (L2 - L1)))
143	141, 142	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2)) = (abs` (L2 - L1)))
144	44	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((L1 e. RR /\ L2 e. RR) -> (L2 - L1) e. RR)
145	144	3adant3 896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> (L2 - L1) e. RR)
146		0re 6603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- 0 e. RR
147	144, 146	jctil 316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((L1 e. RR /\ L2 e. RR) -> (0 e. RR /\ (L2 - L1) e. RR))
148	147	3adant3 896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> (0 e. RR /\ (L2 - L1) e. RR))
149	47	biimp3a 1194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> 0 < (L2 - L1))
150		ltle 6690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((0 e. RR /\ (L2 - L1) e. RR) -> (0 < (L2 - L1) -> 0 <_ (L2 - L1)))
151	148, 149, 150	sylc 83	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> 0 <_ (L2 - L1))
152		absid 8113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((L2 - L1) e. RR /\ 0 <_ (L2 - L1)) -> (abs` (L2 - L1)) = (L2 - L1))
153	145, 151, 152	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> (abs` (L2 - L1)) = (L2 - L1))
154	143, 153	eqtr2d 1926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> (L2 - L1) = (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2)))
155	127	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((L1 e. RR /\ L2 e. RR) -> L2 e. CC)
156	128	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((L1 e. RR /\ L2 e. RR) -> L1 e. CC)
157	139, 28, 30	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((L1 e. RR /\ L2 e. RR) -> ((abs` (L2 - L1)) / 2) e. RR)
158		recn 6466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((abs` (L2 - L1)) / 2) e. RR -> ((abs` (L2 - L1)) / 2) e. CC)
159	158, 158	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((abs` (L2 - L1)) / 2) e. RR -> (((abs` (L2 - L1)) / 2) e. CC /\ ((abs` (L2 - L1)) / 2) e. CC))
160		addcl 6454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((((abs` (L2 - L1)) / 2) e. CC /\ ((abs` (L2 - L1)) / 2) e. CC) -> (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2)) e. CC)
161	157, 159, 160	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((L1 e. RR /\ L2 e. RR) -> (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2)) e. CC)
162	155, 156, 161	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((L1 e. RR /\ L2 e. RR) -> (L2 e. CC /\ L1 e. CC /\ (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2)) e. CC))
163	162	3adant3 896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> (L2 e. CC /\ L1 e. CC /\ (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2)) e. CC))
164		subadd 6532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((L2 e. CC /\ L1 e. CC /\ (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2)) e. CC) -> ((L2 - L1) = (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2)) <-> (L1 + (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2))) = L2))
165	163, 164	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> ((L2 - L1) = (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2)) <-> (L1 + (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2))) = L2))
166	154, 165	mpbid 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> (L1 + (((abs` (L2 - L1)) / 2) + ((abs` (L2 - L1)) / 2))) = L2)
167	138, 166	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> (((abs` (L2 - L1)) / 2) + (L1 + ((abs` (L2 - L1)) / 2))) = L2)
168		recn 6466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((L2 - L1) e. RR -> (L2 - L1) e. CC)
169	144, 168, 28	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((L1 e. RR /\ L2 e. RR) -> (abs` (L2 - L1)) e. RR)
170	169, 132, 133	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((L1 e. RR /\ L2 e. RR) -> ((abs` (L2 - L1)) / 2) e. CC)
171		simpl 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((L1 e. RR /\ L2 e. RR) -> L1 e. RR)
172	171, 157	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((L1 e. RR /\ L2 e. RR) -> (L1 e. RR /\ ((abs` (L2 - L1)) / 2) e. RR))
173	128, 158	anim12i 360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((L1 e. RR /\ ((abs` (L2 - L1)) / 2) e. RR) -> (L1 e. CC /\ ((abs` (L2 - L1)) / 2) e. CC))
174		addcl 6454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((L1 e. CC /\ ((abs` (L2 - L1)) / 2) e. CC) -> (L1 + ((abs` (L2 - L1)) / 2)) e. CC)
175	172, 173, 174	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((L1 e. RR /\ L2 e. RR) -> (L1 + ((abs` (L2 - L1)) / 2)) e. CC)
176	155, 170, 175	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((L1 e. RR /\ L2 e. RR) -> (L2 e. CC /\ ((abs` (L2 - L1)) / 2) e. CC /\ (L1 + ((abs` (L2 - L1)) / 2)) e. CC))
177	176	3adant3 896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> (L2 e. CC /\ ((abs` (L2 - L1)) / 2) e. CC /\ (L1 + ((abs` (L2 - L1)) / 2)) e. CC))
178		subadd 6532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((L2 e. CC /\ ((abs` (L2 - L1)) / 2) e. CC /\ (L1 + ((abs` (L2 - L1)) / 2)) e. CC) -> ((L2 - ((abs` (L2 - L1)) / 2)) = (L1 + ((abs` (L2 - L1)) / 2)) <-> (((abs` (L2 - L1)) / 2) + (L1 + ((abs` (L2 - L1)) / 2))) = L2))
179	177, 178	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> ((L2 - ((abs` (L2 - L1)) / 2)) = (L1 + ((abs` (L2 - L1)) / 2)) <-> (((abs` (L2 - L1)) / 2) + (L1 + ((abs` (L2 - L1)) / 2))) = L2))
180	167, 179	mpbird 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((L1 e. RR /\ L2 e. RR /\ L1 < L2) -> (L2 - ((abs` (L2 - L1)) / 2)) = (L1 + ((abs` (L2 - L1)) / 2)))
181	43, 37, 46, 180	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (L2 - ((abs` (L2 - L1)) / 2)) = (L1 + ((abs` (L2 - L1)) / 2)))
182		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((L2 - ((abs` (L2 - L1)) / 2)) = (L1 + ((abs` (L2 - L1)) / 2)) -> ((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) <-> (F1` x) < (L1 + ((abs` (L2 - L1)) / 2))))
183	182	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((L2 - ((abs` (L2 - L1)) / 2)) = (L1 + ((abs` (L2 - L1)) / 2)) -> (((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x)) <-> ((F1` x) < (L1 + ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x))))
184	183	imbi2d 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((L2 - ((abs` (L2 - L1)) / 2)) = (L1 + ((abs` (L2 - L1)) / 2)) -> ((((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))) -> ((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x))) <-> (((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))) -> ((F1` x) < (L1 + ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x)))))
185		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F1` x) e. (F1"(r i^i s))) -> (F1` x) e. ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))))
186		elioooord 14855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((F1` x) e. ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) -> ((L1 - ((abs` (L2 - L1)) / 2)) < (F1` x) /\ (F1` x) < (L1 + ((abs` (L2 - L1)) / 2))))
187		simpr 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((L1 - ((abs` (L2 - L1)) / 2)) < (F1` x) /\ (F1` x) < (L1 + ((abs` (L2 - L1)) / 2))) -> (F1` x) < (L1 + ((abs` (L2 - L1)) / 2)))
188	185, 186, 187	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F1` x) e. (F1"(r i^i s))) -> (F1` x) < (L1 + ((abs` (L2 - L1)) / 2)))
189		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))) /\ (F2` x) e. (F2"(r i^i s))) -> (F2` x) e. ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))))
190		elioooord 14855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((F2` x) e. ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))) -> ((L2 - ((abs` (L2 - L1)) / 2)) < (F2` x) /\ (F2` x) < (L2 + ((abs` (L2 - L1)) / 2))))
191		simpl 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((L2 - ((abs` (L2 - L1)) / 2)) < (F2` x) /\ (F2` x) < (L2 + ((abs` (L2 - L1)) / 2))) -> (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x))
192	189, 190, 191	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))) /\ (F2` x) e. (F2"(r i^i s))) -> (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x))
193	188, 192	anim12i 360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F1` x) e. (F1"(r i^i s))) /\ ((F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))) /\ (F2` x) e. (F2"(r i^i s)))) -> ((F1` x) < (L1 + ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x)))
194	193	an4s 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ ((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s)))) -> ((F1` x) < (L1 + ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x)))
195	194	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> (((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))) -> ((F1` x) < (L1 + ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x))))
196	184, 195	syl5bir 227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((L2 - ((abs` (L2 - L1)) / 2)) = (L1 + ((abs` (L2 - L1)) / 2)) -> (((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> (((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))) -> ((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x)))))
197	181, 196	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> (((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))) -> ((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x)))))
198	197	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))) -> ((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x)))))
199	198	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))) -> ((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x)))))
200	199	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) -> (((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))) -> ((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x))))
201	200	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) /\ x e. (r i^i s)) -> (((F1` x) e. (F1"(r i^i s)) /\ (F2` x) e. (F2"(r i^i s))) -> ((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x))))
202	126, 201	mpd 29	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) /\ x e. (r i^i s)) -> ((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x)))
203	85, 202	jca 310	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) /\ x e. (r i^i s)) -> (((F1` x) e. RR /\ (L2 - ((abs` (L2 - L1)) / 2)) e. RR /\ (F2` x) e. RR) /\ ((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x))))
204	203	ex 402	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) -> (x e. (r i^i s) -> (((F1` x) e. RR /\ (L2 - ((abs` (L2 - L1)) / 2)) e. RR /\ (F2` x) e. RR) /\ ((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x)))))
205		axlttrn 6673	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F1` x) e. RR /\ (L2 - ((abs` (L2 - L1)) / 2)) e. RR /\ (F2` x) e. RR) -> (((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x)) -> (F1` x) < (F2` x)))
206	205	imp 377	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((F1` x) e. RR /\ (L2 - ((abs` (L2 - L1)) / 2)) e. RR /\ (F2` x) e. RR) /\ ((F1` x) < (L2 - ((abs` (L2 - L1)) / 2)) /\ (L2 - ((abs` (L2 - L1)) / 2)) < (F2` x))) -> (F1` x) < (F2` x))
207	204, 206	syl6 25	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) -> (x e. (r i^i s) -> (F1` x) < (F2` x)))
208	207	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . . 21 |- (((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) /\ ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2))) -> A.x e. (r i^i s)(F1` x) < (F2` x))
209	208	ex 402	. . . . . . . . . . . . . . . . . . . 20 |- ((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> A.x e. (r i^i s)(F1` x) < (F2` x)))
210		raleq 2266	. . . . . . . . . . . . . . . . . . . . . 22 |- (a = (r i^i s) -> (A.x e. a (F1` x) < (F2` x) <-> A.x e. (r i^i s)(F1` x) < (F2` x)))
211	210	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . 21 |- (((r i^i s) e. F /\ A.x e. (r i^i s)(F1` x) < (F2` x)) -> E.a e. F A.x e. a (F1` x) < (F2` x))
212	211	expcom 403	. . . . . . . . . . . . . . . . . . . 20 |- (A.x e. (r i^i s)(F1` x) < (F2` x) -> ((r i^i s) e. F -> E.a e. F A.x e. a (F1` x) < (F2` x)))
213	209, 212	syl6 25	. . . . . . . . . . . . . . . . . . 19 |- ((((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) /\ (r i^i s) e. F) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> ((r i^i s) e. F -> E.a e. F A.x e. a (F1` x) < (F2` x))))
214	213	ex 402	. . . . . . . . . . . . . . . . . 18 |- (((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> ((r i^i s) e. F -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> ((r i^i s) e. F -> E.a e. F A.x e. a (F1` x) < (F2` x)))))
215	214	com14 42	. . . . . . . . . . . . . . . . 17 |- ((r i^i s) e. F -> ((r i^i s) e. F -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> E.a e. F A.x e. a (F1` x) < (F2` x)))))
216	215	pm2.43i 78	. . . . . . . . . . . . . . . 16 |- ((r i^i s) e. F -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> E.a e. F A.x e. a (F1` x) < (F2` x))))
217		inss1 2812	. . . . . . . . . . . . . . . . . 18 |- (r i^i s) C_ r
218		inss2 2813	. . . . . . . . . . . . . . . . . 18 |- (r i^i s) C_ s
219		imass2 4299	. . . . . . . . . . . . . . . . . . 19 |- ((r i^i s) C_ r -> (F1"(r i^i s)) C_ (F1"r))
220		imass2 4299	. . . . . . . . . . . . . . . . . . 19 |- ((r i^i s) C_ s -> (F2"(r i^i s)) C_ (F2"s))
221	219, 220	anim12i 360	. . . . . . . . . . . . . . . . . 18 |- (((r i^i s) C_ r /\ (r i^i s) C_ s) -> ((F1"(r i^i s)) C_ (F1"r) /\ (F2"(r i^i s)) C_ (F2"s)))
222	217, 218, 221	mp2an 761	. . . . . . . . . . . . . . . . 17 |- ((F1"(r i^i s)) C_ (F1"r) /\ (F2"(r i^i s)) C_ (F2"s))
223		sstr2 2623	. . . . . . . . . . . . . . . . . 18 |- ((F1"(r i^i s)) C_ (F1"r) -> ((F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) -> (F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2)))))
224		sstr2 2623	. . . . . . . . . . . . . . . . . 18 |- ((F2"(r i^i s)) C_ (F2"s) -> ((F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))) -> (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))))
225	223, 224	im2anan9 622	. . . . . . . . . . . . . . . . 17 |- (((F1"(r i^i s)) C_ (F1"r) /\ (F2"(r i^i s)) C_ (F2"s)) -> (((F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> ((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))))))
226	222, 225	ax-mp 7	. . . . . . . . . . . . . . . 16 |- (((F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> ((F1"(r i^i s)) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"(r i^i s)) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))))
227	216, 226	syl7 26	. . . . . . . . . . . . . . 15 |- ((r i^i s) e. F -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (((F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> E.a e. F A.x e. a (F1` x) < (F2` x))))
228	68, 227	syl 12	. . . . . . . . . . . . . 14 |- ((F e. Fil /\ r e. F /\ s e. F) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (((F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> E.a e. F A.x e. a (F1` x) < (F2` x))))
229	228	3expib 1070	. . . . . . . . . . . . 13 |- (F e. Fil -> ((r e. F /\ s e. F) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> (((F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> E.a e. F A.x e. a (F1` x) < (F2` x)))))
230	229	com23 36	. . . . . . . . . . . 12 |- (F e. Fil -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> ((r e. F /\ s e. F) -> (((F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> E.a e. F A.x e. a (F1` x) < (F2` x)))))
231	230	3ad2ant1 897	. . . . . . . . . . 11 |- ((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> ((r e. F /\ s e. F) -> (((F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> E.a e. F A.x e. a (F1` x) < (F2` x)))))
232	231	anabsi5 553	. . . . . . . . . 10 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> ((r e. F /\ s e. F) -> (((F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> E.a e. F A.x e. a (F1` x) < (F2` x))))
233	232	com3l 38	. . . . . . . . 9 |- ((r e. F /\ s e. F) -> (((F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> E.a e. F A.x e. a (F1` x) < (F2` x))))
234	233	imp 377	. . . . . . . 8 |- (((r e. F /\ s e. F) /\ ((F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))))) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> E.a e. F A.x e. a (F1` x) < (F2` x)))
235	234	an4s 566	. . . . . . 7 |- (((r e. F /\ (F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2)))) /\ (s e. F /\ (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))))) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> E.a e. F A.x e. a (F1` x) < (F2` x)))
236	235	expcom 403	. . . . . 6 |- ((s e. F /\ (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> ((r e. F /\ (F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2)))) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> E.a e. F A.x e. a (F1` x) < (F2` x))))
237	236	r19.23aiva 2212	. . . . 5 |- (E.s e. F (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))) -> ((r e. F /\ (F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2)))) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> E.a e. F A.x e. a (F1` x) < (F2` x))))
238	237	com12 14	. . . 4 |- ((r e. F /\ (F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2)))) -> (E.s e. F (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> E.a e. F A.x e. a (F1` x) < (F2` x))))
239	238	r19.23aiva 2212	. . 3 |- (E.r e. F (F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) -> (E.s e. F (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2))) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> E.a e. F A.x e. a (F1` x) < (F2` x))))
240	239	imp 377	. 2 |- ((E.r e. F (F1"r) C_ ((L1 - ((abs` (L2 - L1)) / 2))(,)(L1 + ((abs` (L2 - L1)) / 2))) /\ E.s e. F (F2"s) C_ ((L2 - ((abs` (L2 - L1)) / 2))(,)(L2 + ((abs` (L2 - L1)) / 2)))) -> (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> E.a e. F A.x e. a (F1` x) < (F2` x)))
241	67, 240	mpcom 60	1 |- (((F e. Fil /\ F1:Y-->RR /\ F2:Y-->RR) /\ (((J fLimf F)` F1) =/= (/) /\ ((J fLimf F)` F2) =/= (/) /\ L1 < L2)) -> E.a e. F A.x e. a (F1` x) < (F2` x))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106   i^i cin 2592   C_ wss 2593  (/)c0 2875  U.cuni 3177   class class class wbr 3338  dom cdm 3986  ran crn 3987  "cima 3989  Fun wfun 3992  -->wf 3994  ` cfv 3998  (class class class)co 4884  CCcc 6384  RRcr 6385  0cc0 6386   + caddc 6389   - cmin 6445   / cdiv 6447   <_ cle 6448  RR+crp 6453   < clt 6653  2c2 7145  (,)cioo 7524  abscabs 8000  topGenctg 8860  Filcfil 10264   fLimf cflimf 10305

This theorem is referenced by:  lvsovso2 15039

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-map 5383  df-en 5427  df-dom 5428  df-sdom 5429  df-fin 5430  df-undef 5556  df-riota 5560  df-sup 5664  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-n 7108  df-2 7154  df-rp 7232  df-n0 7309  df-z 7345  df-q 7436  df-ioo 7528  df-seq1 7721  df-exp 7812  df-sqr 7920  df-re 8001  df-im 8002  df-cj 8003  df-abs 8004  df-top 8861  df-bases 8863  df-topgen 8864  df-nei 8989  df-haus 9059  df-met 9070  df-bl 9072  df-opn 9073  df-fi 10211  df-fbas 10259  df-fg 10260  df-fil 10265  df-flim1 10295  df-filmap 10306  df-flimf 10316

Copyright terms: Public domain