Theorem ivthlem8 7231

Description: Lemma for isupivth 7233.

Hypotheses

Ref	Expression
ivthlem4.1	|- A e. RR
ivthlem4.2	|- B e. RR
ivthlem4.3	|- U e. RR
ivthlem4.4	|- A < B
ivthlem4.5	|- ((F` A) < U /\ U < (F` B))
ivthlem4.6	|- C = sup(S, RR, < )
ivthlem4.7	|- S = {c e. (A[,]B) | (F` c) <_ U}
ivthlem4.8	|- F e. ((A[,]B)-cn->RR)

Assertion

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

Distinct variable groups:   A,c   B,c   F,c   U,c

Proof of Theorem ivthlem8

Step	Hyp	Ref	Expression
1		ivthlem4.1	. . . . . 6 |- A e. RR
2		ivthlem4.2	. . . . . 6 |- B e. RR
3		ivthlem4.3	. . . . . 6 |- U e. RR
4		ivthlem4.4	. . . . . 6 |- A < B
5		ivthlem4.5	. . . . . 6 |- ((F` A) < U /\ U < (F` B))
6		ivthlem4.6	. . . . . 6 |- C = sup(S, RR, < )
7		ivthlem4.7	. . . . . 6 |- S = {c e. (A[,]B) | (F` c) <_ U}
8		ivthlem4.8	. . . . . 6 |- F e. ((A[,]B)-cn->RR)
9	1, 2, 3, 4, 5, 6, 7, 8	ivthlem5 7228	. . . . 5 |- C e. (A[,]B)
10		elicc2t 6332	. . . . . 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 5562	. . . . . . . . 9 |- A <_ B
16		lbicc2t 6345	. . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ A <_ B) -> A e. (A[,]B))
17	1, 2, 15, 16	mp3an 914	. . . . . . . 8 |- A e. (A[,]B)
18		iccssret 6337	. . . . . . . . . . . . . 14 |- ((A e. RR /\ B e. RR) -> (A[,]B) (_ RR)
19	1, 2, 18	mp2an 696	. . . . . . . . . . . . 13 |- (A[,]B) (_ RR
20		axresscn 5248	. . . . . . . . . . . . 13 |- RR (_ CC
21	19, 20	sstri 2069	. . . . . . . . . . . 12 |- (A[,]B) (_ CC
22		elcncf 7208	. . . . . . . . . . . 12 |- (((A[,]B) (_ CC /\ RR (_ CC) -> (F e. ((A[,]B)-cn->RR) <-> (F:(A[,]B)-->RR /\ 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))))
23	21, 20, 22	mp2an 696	. . . . . . . . . . 11 |- (F e. ((A[,]B)-cn->RR) <-> (F:(A[,]B)-->RR /\ 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)))
24	8, 23	mpbi 189	. . . . . . . . . 10 |- (F:(A[,]B)-->RR /\ 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))
25	24	pm3.26i 320	. . . . . . . . 9 |- F:(A[,]B)-->RR
26	25	ffvelrni 3806	. . . . . . . 8 |- (A e. (A[,]B) -> (F` A) e. RR)
27	17, 26	ax-mp 7	. . . . . . 7 |- (F` A) e. RR
28	27, 3	ltne 5564	. . . . . 6 |- ((F` A) < U -> U =/= (F` A))
29	14, 28	ax-mp 7	. . . . 5 |- U =/= (F` A)
30		fveq2 3715	. . . . . . 7 |- (C = A -> (F` C) = (F` A))
31	25	ffvelrni 3806	. . . . . . . . . 10 |- (C e. (A[,]B) -> (F` C) e. RR)
32	9, 31	ax-mp 7	. . . . . . . . 9 |- (F` C) e. RR
33	32, 3	lttri3 5554	. . . . . . . 8 |- ((F` C) = U <-> (-. (F` C) < U /\ -. U < (F` C)))
34		pm4.2 170	. . . . . . . . . . 11 |- (z e. RR+ <-> z e. RR+)
35		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)))
36		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))
37		eqid 1473	. . . . . . . . . . 11 |- if(B <_ (C + z), B, (C + z)) = if(B <_ (C + z), B, (C + z))
38	1, 2, 3, 4, 5, 6, 7, 8, 34, 35, 36, 37	ivthlem7 7230	. . . . . . . . . 10 |- -. (z e. RR+ /\ A.w e. (A[,]B)((abs` (C - w)) < z -> (F` w) < U))
39	38	nex 1099	. . . . . . . . 9 |- -. E.z(z e. RR+ /\ A.w e. (A[,]B)((abs` (C - w)) < z -> (F` w) < U))
40		opreq1 3959	. . . . . . . . . . . . . . . . . 18 |- (x = C -> (x - w) = (C - w))
41	40	fveq2d 3719	. . . . . . . . . . . . . . . . 17 |- (x = C -> (abs` (x - w)) = (abs` (C - w)))
42	41	breq1d 2624	. . . . . . . . . . . . . . . 16 |- (x = C -> ((abs` (x - w)) < z <-> (abs` (C - w)) < z))
43		fveq2 3715	. . . . . . . . . . . . . . . . . . 19 |- (x = C -> (F` x) = (F` C))
44	43	opreq1d 3966	. . . . . . . . . . . . . . . . . 18 |- (x = C -> ((F` x) - (F` w)) = ((F` C) - (F` w)))
45	44	fveq2d 3719	. . . . . . . . . . . . . . . . 17 |- (x = C -> (abs` ((F` x) - (F` w))) = (abs` ((F` C) - (F` w))))
46	45	breq1d 2624	. . . . . . . . . . . . . . . 16 |- (x = C -> ((abs` ((F` x) - (F` w))) < y <-> (abs` ((F` C) - (F` w))) < y))
47	42, 46	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)))
48	47	rexralbidv 1679	. . . . . . . . . . . . . 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)))
49	48	ralbidv 1660	. . . . . . . . . . . . 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)))
50	24	pm3.27i 324	. . . . . . . . . . . . 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)
51	49, 50	vtoclri 1855	. . . . . . . . . . . 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))
52	9, 51	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)
53	32, 3, 52	ivthlem2 7225	. . . . . . . . . 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))))
54	25	ffvelrni 3806	. . . . . . . . . . 11 |- (w e. (A[,]B) -> (F` w) e. RR)
55	3, 32	ivthlem1 7224	. . . . . . . . . . . 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)))
56	55	pm3.27i 324	. . . . . . . . . . 11 |- ((F` w) e. RR -> ((abs` ((F` C) - (F` w))) < (U - (F` C)) -> (F` w) < U))
57	54, 56	syl 10	. . . . . . . . . 10 |- (w e. (A[,]B) -> ((abs` ((F` C) - (F` w))) < (U - (F` C)) -> (F` w) < U))
58	53, 57	ivthlem3 7226	. . . . . . . . 9 |- ((F` C) < U -> E.z(z e. RR+ /\ A.w e. (A[,]B)((abs` (C - w)) < z -> (F` w) < U)))
59	39, 58	mto 106	. . . . . . . 8 |- -. (F` C) < U
60	1, 2, 3, 4, 5, 6, 7, 8, 34, 35, 36, 37	ivthlem6 7229	. . . . . . . . . 10 |- -. (z e. RR+ /\ A.w e. (A[,]B)((abs` (C - w)) < z -> U < (F` w)))
61	60	nex 1099	. . . . . . . . 9 |- -. E.z(z e. RR+ /\ A.w e. (A[,]B)((abs