Theorem ivthlem2 18812

Description: Lemma for ivth 18814. Show that the supremum of S cannot be less than U. If it was, continuity of F implies that there are points just above the supremum that are also less than U, a contradiction. (Contributed by Mario Carneiro, 17-Jun-2014.)

Hypotheses

Ref	Expression
ivth.1	|- ( ph -> A e. RR )
ivth.2	|- ( ph -> B e. RR )
ivth.3	|- ( ph -> U e. RR )
ivth.4	|- ( ph -> A < B )
ivth.5	|- ( ph -> ( A [,] B ) C_ D )
ivth.7	|- ( ph -> F e. ( D -cn-> CC ) )
ivth.8	|- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )
ivth.9	|- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )
ivth.10	|- S = { x e. ( A [,] B ) | ( F ` x ) <_ U }
ivth.11	|- C = sup ( S , RR , < )

Assertion

Ref	Expression
ivthlem2	|- ( ph -> -. ( F ` C ) < U )

Distinct variable groups:   x, B   x, D   x, F   ph, x   x, A   x, C   x, S   x, U

Proof of Theorem ivthlem2

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ivth.7	. . . . . 6 |- ( ph -> F e. ( D -cn-> CC ) )
2	1	adantr 451	. . . . 5 |- ( ( ph /\ ( F ` C ) < U ) -> F e. ( D -cn-> CC ) )
3		ivth.5	. . . . . . 7 |- ( ph -> ( A [,] B ) C_ D )
4		ivth.11	. . . . . . . . 9 |- C = sup ( S , RR , < )
5		ivth.10	. . . . . . . . . . . . 13 |- S = { x e. ( A [,] B ) | ( F ` x ) <_ U }
6		ssrab2 3258	. . . . . . . . . . . . 13 |- { x e. ( A [,] B ) | ( F ` x ) <_ U } C_ ( A [,] B )
7	5, 6	eqsstri 3208	. . . . . . . . . . . 12 |- S C_ ( A [,] B )
8		ivth.1	. . . . . . . . . . . . 13 |- ( ph -> A e. RR )
9		ivth.2	. . . . . . . . . . . . 13 |- ( ph -> B e. RR )
10		iccssre 10731	. . . . . . . . . . . . 13 |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
11	8, 9, 10	syl2anc 642	. . . . . . . . . . . 12 |- ( ph -> ( A [,] B ) C_ RR )
12	7, 11	syl5ss 3190	. . . . . . . . . . 11 |- ( ph -> S C_ RR )
13		ivth.3	. . . . . . . . . . . . . 14 |- ( ph -> U e. RR )
14		ivth.4	. . . . . . . . . . . . . 14 |- ( ph -> A < B )
15		ivth.8	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )
16		ivth.9	. . . . . . . . . . . . . 14 |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )
17	8, 9, 13, 14, 3, 1, 15, 16, 5	ivthlem1 18811	. . . . . . . . . . . . 13 |- ( ph -> ( A e. S /\ A. z e. S z <_ B ) )
18	17	simpld 445	. . . . . . . . . . . 12 |- ( ph -> A e. S )
19		ne0i 3461	. . . . . . . . . . . 12 |- ( A e. S -> S =/= (/) )
20	18, 19	syl 15	. . . . . . . . . . 11 |- ( ph -> S =/= (/) )
21	17	simprd 449	. . . . . . . . . . . 12 |- ( ph -> A. z e. S z <_ B )
22		breq2 4027	. . . . . . . . . . . . . 14 |- ( x = B -> ( z <_ x <-> z <_ B ) )
23	22	ralbidv 2563	. . . . . . . . . . . . 13 |- ( x = B -> ( A. z e. S z <_ x <-> A. z e. S z <_ B ) )
24	23	rspcev 2884	. . . . . . . . . . . 12 |- ( ( B e. RR /\ A. z e. S z <_ B ) -> E. x e. RR A. z e. S z <_ x )
25	9, 21, 24	syl2anc 642	. . . . . . . . . . 11 |- ( ph -> E. x e. RR A. z e. S z <_ x )
26	12, 20, 25	3jca 1132	. . . . . . . . . 10 |- ( ph -> ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) )
27		suprcl 9714	. . . . . . . . . 10 |- ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) -> sup ( S , RR , < ) e. RR )
28	26, 27	syl 15	. . . . . . . . 9 |- ( ph -> sup ( S , RR , < ) e. RR )
29	4, 28	syl5eqel 2367	. . . . . . . 8 |- ( ph -> C e. RR )
30		suprub 9715	. . . . . . . . . 10 |- ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) /\ A e. S ) -> A <_ sup ( S , RR , < ) )
31	26, 18, 30	syl2anc 642	. . . . . . . . 9 |- ( ph -> A <_ sup ( S , RR , < ) )
32	31, 4	syl6breqr 4063	. . . . . . . 8 |- ( ph -> A <_ C )
33		suprleub 9718	. . . . . . . . . . 11 |- ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) /\ B e. RR ) -> ( sup ( S , RR , < ) <_ B <-> A. z e. S z <_ B ) )
34	26, 9, 33	syl2anc 642	. . . . . . . . . 10 |- ( ph -> ( sup ( S , RR , < ) <_ B <-> A. z e. S z <_ B ) )
35	21, 34	mpbird 223	. . . . . . . . 9 |- ( ph -> sup ( S , RR , < ) <_ B )
36	4, 35	syl5eqbr 4056	. . . . . . . 8 |- ( ph -> C <_ B )
37		elicc2 10715	. . . . . . . . 9 |- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
38	8, 9, 37	syl2anc 642	. . . . . . . 8 |- ( ph -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
39	29, 32, 36, 38	mpbir3and 1135	. . . . . . 7 |- ( ph -> C e. ( A [,] B ) )
40	3, 39	sseldd 3181	. . . . . 6 |- ( ph -> C e. D )
41	40	adantr 451	. . . . 5 |- ( ( ph /\ ( F ` C ) < U ) -> C e. D )
42	15	ralrimiva 2626	. . . . . . . 8 |- ( ph -> A. x e. ( A [,] B ) ( F ` x ) e. RR )
43		fveq2 5525	. . . . . . . . . 10 |- ( x = C -> ( F ` x ) = ( F ` C ) )
44	43	eleq1d 2349	. . . . . . . . 9 |- ( x = C -> ( ( F ` x ) e. RR <-> ( F ` C ) e. RR ) )
45	44	rspcv 2880	. . . . . . . 8 |- ( C e. ( A [,] B ) -> ( A. x e. ( A [,] B ) ( F ` x ) e. RR -> ( F ` C ) e. RR ) )
46	39, 42, 45	sylc 56	. . . . . . 7 |- ( ph -> ( F ` C ) e. RR )
47		difrp 10387	. . . . . . 7 |- ( ( ( F ` C ) e. RR /\ U e. RR ) -> ( ( F ` C ) < U <-> ( U - ( F ` C ) ) e. RR+ ) )
48	46, 13, 47	syl2anc 642	. . . . . 6 |- ( ph -> ( ( F ` C ) < U <-> ( U - ( F ` C ) ) e. RR+ ) )
49	48	biimpa 470	. . . . 5 |- ( ( ph /\ ( F ` C ) < U ) -> ( U - ( F ` C ) ) e. RR+ )
50		cncfi 18398	. . . . 5 |- ( ( F e. ( D -cn-> CC ) /\ C e. D /\ ( U - ( F ` C ) ) e. RR+ ) -> E. z e. RR+ A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) )
51	2, 41, 49, 50	syl3anc 1182	. . . 4 |- ( ( ph /\ ( F ` C ) < U ) -> E. z e. RR+ A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) )
52		ssralv 3237	. . . . . . . 8 |- ( ( A [,] B ) C_ D -> ( A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) ) )
53	3, 52	syl 15	. . . . . . 7 |- ( ph -> ( A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) ) )
54	53	ad2antrr 706	. . . . . 6 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) ) )
55	9	ad2antrr 706	. . . . . . . . . 10 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> B e. RR )
56	29	ad2antrr 706	. . . . . . . . . . 11 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> C e. RR )
57		rphalfcl 10378	. . . . . . . . . . . . 13 |- ( z e. RR+ -> ( z / 2 ) e. RR+ )
58	57	adantl 452	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( z / 2 ) e. RR+ )
59	58	rpred 10390	. . . . . . . . . . 11 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( z / 2 ) e. RR )
60	56, 59	readdcld 8862	. . . . . . . . . 10 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( C + ( z / 2 ) ) e. RR )
61		ifcl 3601	. . . . . . . . . 10 |- ( ( B e. RR /\ ( C + ( z / 2 ) ) e. RR ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. RR )
62	55, 60, 61	syl2anc 642	. . . . . . . . 9 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. RR )
63	8	ad2antrr 706	. . . . . . . . . 10 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> A e. RR )
64	32	ad2antrr 706	. . . . . . . . . 10 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> A <_ C )
65	16	simprd 449	. . . . . . . . . . . . . . . 16 |- ( ph -> U < ( F ` B ) )
66	8	rexrd 8881	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A e. RR* )
67	9	rexrd 8881	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> B e. RR* )
68	8, 9, 14	ltled 8967	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A <_ B )
69		ubicc2 10753	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
70	66, 67, 68, 69	syl3anc 1182	. . . . . . . . . . . . . . . . . 18 |- ( ph -> B e. ( A [,] B ) )
71		fveq2 5525	. . . . . . . . . . . . . . . . . . . 20 |- ( x = B -> ( F ` x ) = ( F ` B ) )
72	71	eleq1d 2349	. . . . . . . . . . . . . . . . . . 19 |- ( x = B -> ( ( F ` x ) e. RR <-> ( F ` B ) e. RR ) )
73	72	rspcv 2880	. . . . . . . . . . . . . . . . . 18 |- ( B e. ( A [,] B ) -> ( A. x e. ( A [,] B ) ( F ` x ) e. RR -> ( F ` B ) e. RR ) )
74	70, 42, 73	sylc 56	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( F ` B ) e. RR )
75		lttr 8899	. . . . . . . . . . . . . . . . 17 |- ( ( ( F ` C ) e. RR /\ U e. RR /\ ( F ` B ) e. RR ) -> ( ( ( F ` C ) < U /\ U < ( F ` B ) ) -> ( F ` C ) < ( F ` B ) ) )
76	46, 13, 74, 75	syl3anc 1182	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( F ` C ) < U /\ U < ( F ` B ) ) -> ( F ` C ) < ( F ` B ) ) )
77	65, 76	mpan2d 655	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( F ` C ) < U -> ( F ` C ) < ( F ` B ) ) )
78	77	imp 418	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( F ` C ) < U ) -> ( F ` C ) < ( F ` B ) )
79	78	adantr 451	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( F ` C ) < ( F ` B ) )
80	46	ltnrd 8953	. . . . . . . . . . . . . . . . . 18 |- ( ph -> -. ( F ` C ) < ( F ` C ) )
81		fveq2 5525	. . . . . . . . . . . . . . . . . . . 20 |- ( B = C -> ( F ` B ) = ( F ` C ) )
82	81	breq2d 4035	. . . . . . . . . . . . . . . . . . 19 |- ( B = C -> ( ( F ` C ) < ( F ` B ) <-> ( F ` C ) < ( F ` C ) ) )
83	82	notbid 285	. . . . . . . . . . . . . . . . . 18 |- ( B = C -> ( -. ( F ` C ) < ( F ` B ) <-> -. ( F ` C ) < ( F ` C ) ) )
84	80, 83	syl5ibrcom 213	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( B = C -> -. ( F ` C ) < ( F ` B ) ) )
85	84	necon2ad 2494	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( F ` C ) < ( F ` B ) -> B =/= C ) )
86	85, 36	jctild 527	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( F ` C ) < ( F ` B ) -> ( C <_ B /\ B =/= C ) ) )
87	29, 9	ltlend 8964	. . . . . . . . . . . . . . 15 |- ( ph -> ( C < B <-> ( C <_ B /\ B =/= C ) ) )
88	86, 87	sylibrd 225	. . . . . . . . . . . . . 14 |- ( ph -> ( ( F ` C ) < ( F ` B ) -> C < B ) )
89	88	ad2antrr 706	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( ( F ` C ) < ( F ` B ) -> C < B ) )
90	79, 89	mpd 14	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> C < B )
91	56, 58	ltaddrpd 10419	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> C < ( C + ( z / 2 ) ) )
92		breq2 4027	. . . . . . . . . . . . 13 |- ( B = if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) -> ( C < B <-> C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) ) )
93		breq2 4027	. . . . . . . . . . . . 13 |- ( ( C + ( z / 2 ) ) = if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) -> ( C < ( C + ( z / 2 ) ) <-> C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) ) )
94	92, 93	ifboth 3596	. . . . . . . . . . . 12 |- ( ( C < B /\ C < ( C + ( z / 2 ) ) ) -> C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) )
95	90, 91, 94	syl2anc 642	. . . . . . . . . . 11 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) )
96	56, 62, 95	ltled 8967	. . . . . . . . . 10 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> C <_ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) )
97	63, 56, 62, 64, 96	letrd 8973	. . . . . . . . 9 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> A <_ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) )
98		min1 10517	. . . . . . . . . 10 |- ( ( B e. RR /\ ( C + ( z / 2 ) ) e. RR ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ B )
99	55, 60, 98	syl2anc 642	. . . . . . . . 9 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ B )
100		elicc2 10715	. . . . . . . . . . 11 |- ( ( A e. RR /\ B e. RR ) -> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. ( A [,] B ) <-> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. RR /\ A <_ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) /\ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ B ) ) )
101	8, 9, 100	syl2anc 642	. . . . . . . . . 10 |- ( ph -> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. ( A [,] B ) <-> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. RR /\ A <_ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) /\ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ B ) ) )
102	101	ad2antrr 706	. . . . . . . . 9 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. ( A [,] B ) <-> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. RR /\ A <_ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) /\ if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ B ) ) )
103	62, 97, 99, 102	mpbir3and 1135	. . . . . . . 8 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. ( A [,] B ) )
104	56, 62, 96	abssubge0d 11914	. . . . . . . . 9 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( abs ` ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) ) = ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) )
105		rpre 10360	. . . . . . . . . . . . 13 |- ( z e. RR+ -> z e. RR )
106	105	adantl 452	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> z e. RR )
107	56, 106	readdcld 8862	. . . . . . . . . . 11 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( C + z ) e. RR )
108		min2 10518	. . . . . . . . . . . 12 |- ( ( B e. RR /\ ( C + ( z / 2 ) ) e. RR ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ ( C + ( z / 2 ) ) )
109	55, 60, 108	syl2anc 642	. . . . . . . . . . 11 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) <_ ( C + ( z / 2 ) ) )
110		rphalflt 10380	. . . . . . . . . . . . 13 |- ( z e. RR+ -> ( z / 2 ) < z )
111	110	adantl 452	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( z / 2 ) < z )
112	59, 106, 56, 111	ltadd2dd 8975	. . . . . . . . . . 11 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( C + ( z / 2 ) ) < ( C + z ) )
113	62, 60, 107, 109, 112	lelttrd 8974	. . . . . . . . . 10 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) < ( C + z ) )
114	62, 56, 106	ltsubadd2d 9370	. . . . . . . . . 10 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) < z <-> if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) < ( C + z ) ) )
115	113, 114	mpbird 223	. . . . . . . . 9 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) < z )
116	104, 115	eqbrtrd 4043	. . . . . . . 8 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( abs ` ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) ) < z )
117		oveq1 5865	. . . . . . . . . . . 12 |- ( y = if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) -> ( y - C ) = ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) )
118	117	fveq2d 5529	. . . . . . . . . . 11 |- ( y = if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) -> ( abs ` ( y - C ) ) = ( abs ` ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) ) )
119	118	breq1d 4033	. . . . . . . . . 10 |- ( y = if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) -> ( ( abs ` ( y - C ) ) < z <-> ( abs ` ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) ) < z ) )
120		breq2 4027	. . . . . . . . . 10 |- ( y = if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) -> ( C < y <-> C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) ) )
121	119, 120	anbi12d 691	. . . . . . . . 9 |- ( y = if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) -> ( ( ( abs ` ( y - C ) ) < z /\ C < y ) <-> ( ( abs ` ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) ) < z /\ C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) ) ) )
122	121	rspcev 2884	. . . . . . . 8 |- ( ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) e. ( A [,] B ) /\ ( ( abs ` ( if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) - C ) ) < z /\ C < if ( B <_ ( C + ( z / 2 ) ) , B , ( C + ( z / 2 ) ) ) ) ) -> E. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z /\ C < y ) )
123	103, 116, 95, 122	syl12anc 1180	. . . . . . 7 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> E. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z /\ C < y ) )
124		r19.29 2683	. . . . . . . 8 |- ( ( A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) /\ E. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z /\ C < y ) ) -> E. y e. ( A [,] B ) ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) /\ ( ( abs ` ( y - C ) ) < z /\ C < y ) ) )
125		pm3.45 807	. . . . . . . . . . 11 |- ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> ( ( ( abs ` ( y - C ) ) < z /\ C < y ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) /\ C < y ) ) )
126	125	imp 418	. . . . . . . . . 10 |- ( ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) /\ ( ( abs ` ( y - C ) ) < z /\ C < y ) ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) /\ C < y ) )
127		simprr 733	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> C < y )
128		simprl 732	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> y e. ( A [,] B ) )
129		simplll 734	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ph )
130	129, 42	syl 15	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> A. x e. ( A [,] B ) ( F ` x ) e. RR )
131		fveq2 5525	. . . . . . . . . . . . . . . . . . . 20 |- ( x = y -> ( F ` x ) = ( F ` y ) )
132	131	eleq1d 2349	. . . . . . . . . . . . . . . . . . 19 |- ( x = y -> ( ( F ` x ) e. RR <-> ( F ` y ) e. RR ) )
133	132	rspcv 2880	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( A [,] B ) -> ( A. x e. ( A [,] B ) ( F ` x ) e. RR -> ( F ` y ) e. RR ) )
134	128, 130, 133	sylc 56	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( F ` y ) e. RR )
135	129, 46	syl 15	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( F ` C ) e. RR )
136	129, 13	syl 15	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> U e. RR )
137	136, 135	resubcld 9211	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( U - ( F ` C ) ) e. RR )
138	134, 135, 137	absdifltd 11916	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) <-> ( ( ( F ` C ) - ( U - ( F ` C ) ) ) < ( F ` y ) /\ ( F ` y ) < ( ( F ` C ) + ( U - ( F ` C ) ) ) ) ) )
139		ltle 8910	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( F ` y ) e. RR /\ U e. RR ) -> ( ( F ` y ) < U -> ( F ` y ) <_ U ) )
140	134, 136, 139	syl2anc 642	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( F ` y ) < U -> ( F ` y ) <_ U ) )
141	135	recnd 8861	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( F ` C ) e. CC )
142	136	recnd 8861	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> U e. CC )
143	141, 142	pncan3d 9160	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( F ` C ) + ( U - ( F ` C ) ) ) = U )
144	143	breq2d 4035	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( F ` y ) < ( ( F ` C ) + ( U - ( F ` C ) ) ) <-> ( F ` y ) < U ) )
145	131	breq1d 4033	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( ( F ` x ) <_ U <-> ( F ` y ) <_ U ) )
146	145, 5	elrab2 2925	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. S <-> ( y e. ( A [,] B ) /\ ( F ` y ) <_ U ) )
147	146	baib 871	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( A [,] B ) -> ( y e. S <-> ( F ` y ) <_ U ) )
148	147	ad2antrl 708	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( y e. S <-> ( F ` y ) <_ U ) )
149	140, 144, 148	3imtr4d 259	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( F ` y ) < ( ( F ` C ) + ( U - ( F ` C ) ) ) -> y e. S ) )
150		suprub 9715	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) /\ y e. S ) -> y <_ sup ( S , RR , < ) )
151	150, 4	syl6breqr 4063	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) /\ y e. S ) -> y <_ C )
152	151	ex 423	. . . . . . . . . . . . . . . . . . . 20 |- ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. z e. S z <_ x ) -> ( y e. S -> y <_ C ) )
153	129, 26, 152	3syl 18	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( y e. S -> y <_ C ) )
154	129, 11	syl 15	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( A [,] B ) C_ RR )
155	154, 128	sseldd 3181	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> y e. RR )
156	129, 29	syl 15	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> C e. RR )
157	155, 156	lenltd 8965	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( y <_ C <-> -. C < y ) )
158	153, 157	sylibd 205	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( y e. S -> -. C < y ) )
159	149, 158	syld 40	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( F ` y ) < ( ( F ` C ) + ( U - ( F ` C ) ) ) -> -. C < y ) )
160	159	adantld 453	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( ( ( F ` C ) - ( U - ( F ` C ) ) ) < ( F ` y ) /\ ( F ` y ) < ( ( F ` C ) + ( U - ( F ` C ) ) ) ) -> -. C < y ) )
161	138, 160	sylbid 206	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) -> -. C < y ) )
162	127, 161	mt2d 109	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> -. ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) )
163	162	pm2.21d 98	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ ( y e. ( A [,] B ) /\ C < y ) ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) -> -. ( F ` C ) < U ) )
164	163	expr 598	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ y e. ( A [,] B ) ) -> ( C < y -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) -> -. ( F ` C ) < U ) ) )
165	164	com23 72	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ y e. ( A [,] B ) ) -> ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) -> ( C < y -> -. ( F ` C ) < U ) ) )
166	165	imp3a 420	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ y e. ( A [,] B ) ) -> ( ( ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) /\ C < y ) -> -. ( F ` C ) < U ) )
167	126, 166	syl5 28	. . . . . . . . 9 |- ( ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) /\ y e. ( A [,] B ) ) -> ( ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) /\ ( ( abs ` ( y - C ) ) < z /\ C < y ) ) -> -. ( F ` C ) < U ) )
168	167	rexlimdva 2667	. . . . . . . 8 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( E. y e. ( A [,] B ) ( ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) /\ ( ( abs ` ( y - C ) ) < z /\ C < y ) ) -> -. ( F ` C ) < U ) )
169	124, 168	syl5 28	. . . . . . 7 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( ( A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) /\ E. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z /\ C < y ) ) -> -. ( F ` C ) < U ) )
170	123, 169	mpan2d 655	. . . . . 6 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( A. y e. ( A [,] B ) ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> -. ( F ` C ) < U ) )
171	54, 170	syld 40	. . . . 5 |- ( ( ( ph /\ ( F ` C ) < U ) /\ z e. RR+ ) -> ( A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> -. ( F ` C ) < U ) )
172	171	rexlimdva 2667	. . . 4 |- ( ( ph /\ ( F ` C ) < U ) -> ( E. z e. RR+ A. y e. D ( ( abs ` ( y - C ) ) < z -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < ( U - ( F ` C ) ) ) -> -. ( F ` C ) < U ) )
173	51, 172	mpd 14	. . 3 |- ( ( ph /\ ( F ` C ) < U ) -> -. ( F ` C ) < U )
174	173	ex 423	. 2 |- ( ph -> ( ( F ` C ) < U -> -. ( F ` C ) < U ) )
175	174	pm2.01d 161	1 |- ( ph -> -. ( F ` C ) < U )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 176   /\ wa 358   /\ w3a 934   = wceq 1623   e. wcel 1684   =/= wne 2446   A.wral 2543   E.wrex 2544   {crab 2547   C_ wss 3152   (/)c0 3455   ifcif 3565   class class class wbr 4023   ` cfv 5255  (class class class)co 5858   supcsup 7193   CCcc 8735   RRcr 8736   + caddc 8740   RR*cxr 8866   < clt 8867   <_ cle 8868   - cmin 9037   / cdiv 9423   2c2 9795   RR+crp 10354   [,]cicc 10659   abscabs 11719   -cn->ccncf 18380

This theorem is referenced by:  ivthlem3  18813

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814  ax-pre-sup 8815

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-er 6660  df-map 6774  df-en 6864  df-dom 6865  df-sdom 6866  df-sup 7194  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-2 9804  df-3 9805  df-n0 9966  df-z 10025  df-uz 10231  df-rp 10355  df-icc 10663  df-seq 11047  df-exp 11105  df-cj 11584  df-re 11585  df-im 11586  df-sqr 11720  df-abs 11721  df-cncf 18382