Theorem ivthlem8OLD 7249

Description: Lemma for ivthOLD 7250.

Hypotheses

Ref	Expression
ivthOLD.1	|- A e. RR
ivthOLD.2	|- B e. RR
ivthOLD.3	|- U e. RR
ivthOLD.4	|- A < B
ivthOLD.5	|- ((F` A) < U /\ U < (F` B))
ivthlem4OLD.6	|- C = sup(S, RR, < )
ivthlem4OLD.7	|- S = {c e. (A[,]B) | (F` c) <_ U}
ivthlem4OLD.8	|- F:(A[,]B)-->RR
ivthlem8OLD.9	|- A.x e. (A[,]B)A.y e. RR+ E.z e. RR+ A.w e. (A[,]B)((abs` (x - w)) < z -> (abs` ((F` x) - (F` w))) < y)

Assertion

Ref	Expression
ivthlem8OLD	|- (C e. (A(,)B) /\ (F` C) = U)

Distinct variable groups:   w,c,x,y,z,A   B,c,w,x,y,z   w,C,x,y,z   F,c,w,x,y,z   w,S,x,y   U,c,w,x,y,z

Proof of Theorem ivthlem8OLD

Step	Hyp	Ref	Expression
1		ivthOLD.1	. . . . . 6 |- A e. RR
2		ivthOLD.2	. . . . . 6 |- B e. RR
3		ivthOLD.3	. . . . . 6 |- U e. RR
4		ivthOLD.4	. . . . . 6 |- A < B
5		ivthOLD.5	. . . . . 6 |- ((F` A) < U /\ U < (F` B))
6		ivthlem4OLD.6	. . . . . 6 |- C = sup(S, RR, < )
7		ivthlem4OLD.7	. . . . . 6 |- S = {c e. (A[,]B) | (F` c) <_ U}
8		ivthlem4OLD.8	. . . . . 6 |- F:(A[,]B)-->RR
9	1, 2, 3, 4, 5, 6, 7, 8	ivthlem5OLD 7246	. . . . 5 |- C e. (A[,]B)
10		elicc2t 6337	. . . . . 6 |- ((A e. RR /\ B e. RR) -> (C e. (A[,]B) <-> (C e. RR /\ A <_ C /\ C <_ B)))
11	1, 2, 10	mp2an 696	. . . . 5 |- (C e. (A[,]B) <-> (C e. RR /\ A <_ C /\ C <_ B))
12	9, 11	mpbi 189	. . . 4 |- (C e. RR /\ A <_ C /\ C <_ B)
13	12	3simp1i 790	. . 3 |- C e. RR
14	5	pm3.26i 320	. . . . . 6 |- (F` A) < U
15	1, 2, 4	ltlei 5564	. . . . . . . . 9 |- A <_ B
16		lbicc2t 6350	. . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ A <_ B) -> A e. (A[,]B))
17	1, 2, 15, 16	mp3an 915	. . . . . . . 8 |- A e. (A[,]B)
18	8	ffvelrni 3810	. . . . . . . 8 |- (A e. (A[,]B) -> (F` A) e. RR)
19	17, 18	ax-mp 7	. . . . . . 7 |- (F` A) e. RR
20	19, 3	ltne 5566	. . . . . 6 |- ((F` A) < U -> U =/= (F` A))
21	14, 20	ax-mp 7	. . . . 5 |- U =/= (F` A)
22		fveq2 3719	. . . . . . 7 |- (C = A -> (F` C) = (F` A))
23	8	ffvelrni 3810	. . . . . . . . . 10 |- (C e. (A[,]B) -> (F` C) e. RR)
24	9, 23	ax-mp 7	. . . . . . . . 9 |- (F` C) e. RR
25	24, 3	lttri3 5556	. . . . . . . 8 |- ((F` C) = U <-> (-. (F` C) < U /\ -. U < (F` C)))
26		pm4.2 170	. . . . . . . . . . 11 |- (z e. RR+ <-> z e. RR+)
27		pm4.2 170	. . . . . . . . . . 11 |- (A.w e. (A[,]B)((abs` (C - w)) < z -> U < (F` w)) <-> A.w e. (A[,]B)((abs` (C - w)) < z -> U < (F` w)))
28		pm4.2 170	. . . . . . . . . . 11 |- (A.w e. (A[,]B)((abs` (C - w)) < z -> (F` w) < U) <-> A.w e. (A[,]B)((abs` (C - w)) < z -> (F` w) < U))
29		eqid 1474	. . . . . . . . . . 11 |- if(B <_ (C + z), B, (C + z)) = if(B <_ (C + z), B, (C + z))
30	1, 2, 3, 4, 5, 6, 7, 8, 26, 27, 28, 29	ivthlem7OLD 7248	. . . . . . . . . 10 |- -. (z e. RR+ /\ A.w e. (A[,]B)((abs` (C - w)) < z -> (F` w) < U))
31	30	nex 1100	. . . . . . . . 9 |- -. E.z(z e. RR+ /\ A.w e. (A[,]B)((abs` (C - w)) < z -> (F` w) < U))
32		opreq1 3963	. . . . . . . . . . . . . . . . . 18 |- (x = C -> (x - w) = (C - w))
33	32	fveq2d 3723	. . . . . . . . . . . . . . . . 17 |- (x = C -> (abs` (x - w)) = (abs` (C - w)))
34	33	breq1d 2625	. . . . . . . . . . . . . . . 16 |- (x = C -> ((abs` (x - w)) < z <-> (abs` (C - w)) < z))
35		fveq2 3719	. . . . . . . . . . . . . . . . . . 19 |- (x = C -> (F` x) = (F` C))
36	35	opreq1d 3970	. . . . . . . . . . . . . . . . . 18 |- (x = C -> ((F` x) - (F` w)) = ((F` C) - (F` w)))
37	36	fveq2d 3723	. . . . . . . . . . . . . . . . 17 |- (x = C -> (abs` ((F` x) - (F` w))) = (abs` ((F` C) - (F` w))))
38	37	breq1d 2625	. . . . . . . . . . . . . . . 16 |- (x = C -> ((abs` ((F` x) - (F` w))) < y <-> (abs` ((F` C) - (F` w))) < y))
39	34, 38	imbi12d 625	. . . . . . . . . . . . . . 15 |- (x = C -> (((abs` (x - w)) < z -> (abs` ((F` x) - (F` w))) < y) <-> ((abs` (C - w)) < z -> (abs` ((F` C) - (F` w))) < y)))
40	39	rexralbidv 1680	. . . . . . . . . . . . . 14 |- (x = C -> (E.z e. RR+ A.w e. (A[,]B)((abs` (x - w)) < z -> (abs` ((F` x) - (F` w))) < y) <-> E.z e. RR+ A.w e. (A[,]B)((abs` (C - w)) < z -> (abs` ((F` C) - (F` w))) < y)))
41	40	ralbidv 1661	. . . . . . . . . . . . 13 |- (x = C -> (A.y e. RR+ E.z e. RR+ A.w e. (A[,]B)((abs` (x - w)) < z -> (abs` ((F` x) - (F` w))) < y) <-> A.y e. RR+ E.z e. RR+ A.w e. (A[,]B)((abs` (C - w)) < z -> (abs` ((F` C) - (F` w))) < y)))
42		ivthlem8OLD.9	. . . . . . . . . . . . 13 |- A.x e. (A[,]B)A.y e. RR+ E.z e. RR+ A.w e. (A[,]B)((abs` (x - w)) < z -> (abs` ((F` x) - (F` w))) < y)
43	41, 42	vtoclri 1856	. . . . . . . . . . . 12 |- (C e. (A[,]B) -> A.y e. RR+ E.z e. RR+ A.w e. (A[,]B)((abs` (C - w)) < z -> (abs` ((F` C) - (F` w))) < y))
44	9, 43	ax-mp 7	. . . . . . . . . . 11 |- A.y e. RR+ E.z e. RR+ A.w e. (A[,]B)((abs` (C - w)) < z -> (abs` ((F` C) - (F` w))) < y)
45	24, 3, 44	ivthlem2 7234	. . . . . . . . . 10 |- ((F` C) < U -> E.z e. RR+ A.w e. (A[,]B)((abs` (C - w)) < z -> (abs` ((F` C) - (F` w))) < (U - (F` C))))
46	8	ffvelrni 3810	. . . . . . . . . . 11 |- (w e. (A[,]B) -> (F` w) e. RR)
47	3, 24	ivthlem1 7233	. . . . . . . . . . . 12 |- (((F` w) e. RR -> ((abs` ((F` C) - (F` w))) < ((F` C) - U) -> U < (F` w))) /\ ((F` w) e. RR -> ((abs` ((F` C) - (F` w))) < (U - (F` C)) -> (F` w) < U)))
48	47	pm3.27i 324	. . . . . . . . . . 11 |- ((F` w) e. RR -> ((abs` ((F` C) - (F` w))) < (U - (F` C)) -> (F` w) < U))
49	46, 48	syl 10	. . . . . . . . . 10 |- (w e. (A[,]B) -> ((abs` ((F` C) - (F` w))) < (U - (F` C)) -> (F` w) < U))
50	45, 49	ivthlem3 7235	. . . . . . . . 9 |- ((F` C) < U -> E.z(z e. RR+ /\ A.w e. (A[,]B)((abs` (C - w)) < z -> (F` w) < U)))
51	31, 50	mto 106	. . . . . . . 8 |- -. (F` C) < U
52	1, 2, 3, 4, 5, 6, 7, 8, 26, 27, 28	ivthlem6OLD 7247	. . . . . . . . . 10 |- -. (z e. RR+ /\ A.w e. (A[,]B)((abs` (C - w)) < z -> U < (F` w)))
53	52	nex 1100	. . . . . . . . 9 |- -. E.z(z e. RR+ /\ A.w e. (A[,]B)((abs` (C - w)) < z -> U < (F` w)))
54	3, 24, 44	ivthlem2 7234	. . . . . . . . . 10 |- (U < (F` C) -> E.z e. RR+ A.w e. (A[,]B)((abs` (C - w)) < z -> (abs` ((F` C) - (F` w))) < ((F` C) - U)))
55	47	pm3.26i 320	. . . . . . . . . . 11 |- ((F` w) e. RR -> ((abs` ((F` C) - (F` w))) < ((F` C) - U) -> U < (F` w)))
56	46, 55	syl 10	. . . . . . . . . 10 |- (w e. (A[,]B) -> ((abs` ((F` C) - (F` w))) < ((F` C) - U) -> U < (F` w)))
57	54, 56	ivthlem3 7235	. . . . . . . . 9 |- (U < (F` C) -> E.z(z e. RR+ /\ A.w e. (A[,]B)((abs` (C - w)) < z -> U < (F` w))))
58	53, 57	mto 106	. . . . . . . 8 |- -. U < (