Metamath Proof Explorer

Theorem ivthle2

Description: The intermediate value theorem with weak inequality, decreasing case. (Contributed by Mario Carneiro, 12-May-2014)

Ref Expression
Hypotheses 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 )
ivthle2.9 
|- ( ph -> ( ( F ` B ) <_ U /\ U <_ ( F ` A ) ) )
Assertion ivthle2 
|- ( ph -> E. c e. ( A [,] B ) ( F ` c ) = U )

Proof

Step Hyp Ref Expression
1 ivth.1 
 |-  ( ph -> A e. RR )
2 ivth.2 
 |-  ( ph -> B e. RR )
3 ivth.3 
 |-  ( ph -> U e. RR )
4 ivth.4 
 |-  ( ph -> A < B )
5 ivth.5 
 |-  ( ph -> ( A [,] B ) C_ D )
6 ivth.7 
 |-  ( ph -> F e. ( D -cn-> CC ) )
7 ivth.8 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )
8 ivthle2.9 
 |-  ( ph -> ( ( F ` B ) <_ U /\ U <_ ( F ` A ) ) )
9 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
10 1 adantr 
 |-  ( ( ph /\ ( ( F ` B ) < U /\ U < ( F ` A ) ) ) -> A e. RR )
11 2 adantr 
 |-  ( ( ph /\ ( ( F ` B ) < U /\ U < ( F ` A ) ) ) -> B e. RR )
12 3 adantr 
 |-  ( ( ph /\ ( ( F ` B ) < U /\ U < ( F ` A ) ) ) -> U e. RR )
13 4 adantr 
 |-  ( ( ph /\ ( ( F ` B ) < U /\ U < ( F ` A ) ) ) -> A < B )
14 5 adantr 
 |-  ( ( ph /\ ( ( F ` B ) < U /\ U < ( F ` A ) ) ) -> ( A [,] B ) C_ D )
15 6 adantr 
 |-  ( ( ph /\ ( ( F ` B ) < U /\ U < ( F ` A ) ) ) -> F e. ( D -cn-> CC ) )
16 7 adantlr 
 |-  ( ( ( ph /\ ( ( F ` B ) < U /\ U < ( F ` A ) ) ) /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )
17 simpr 
 |-  ( ( ph /\ ( ( F ` B ) < U /\ U < ( F ` A ) ) ) -> ( ( F ` B ) < U /\ U < ( F ` A ) ) )
18 10 11 12 13 14 15 16 17 ivth2 
 |-  ( ( ph /\ ( ( F ` B ) < U /\ U < ( F ` A ) ) ) -> E. c e. ( A (,) B ) ( F ` c ) = U )
19 ssrexv 
 |-  ( ( A (,) B ) C_ ( A [,] B ) -> ( E. c e. ( A (,) B ) ( F ` c ) = U -> E. c e. ( A [,] B ) ( F ` c ) = U ) )
20 9 18 19 mpsyl 
 |-  ( ( ph /\ ( ( F ` B ) < U /\ U < ( F ` A ) ) ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
21 20 anassrs 
 |-  ( ( ( ph /\ ( F ` B ) < U ) /\ U < ( F ` A ) ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
22 1 rexrd 
 |-  ( ph -> A e. RR* )
23 2 rexrd 
 |-  ( ph -> B e. RR* )
24 1 2 4 ltled 
 |-  ( ph -> A <_ B )
25 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
26 22 23 24 25 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
27 eqcom 
 |-  ( ( F ` c ) = U <-> U = ( F ` c ) )
28 fveq2 
 |-  ( c = A -> ( F ` c ) = ( F ` A ) )
29 28 eqeq2d 
 |-  ( c = A -> ( U = ( F ` c ) <-> U = ( F ` A ) ) )
30 27 29 bitrid 
 |-  ( c = A -> ( ( F ` c ) = U <-> U = ( F ` A ) ) )
31 30 rspcev 
 |-  ( ( A e. ( A [,] B ) /\ U = ( F ` A ) ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
32 26 31 sylan 
 |-  ( ( ph /\ U = ( F ` A ) ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
33 32 adantlr 
 |-  ( ( ( ph /\ ( F ` B ) < U ) /\ U = ( F ` A ) ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
34 8 simprd 
 |-  ( ph -> U <_ ( F ` A ) )
35 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
36 35 eleq1d 
 |-  ( x = A -> ( ( F ` x ) e. RR <-> ( F ` A ) e. RR ) )
37 7 ralrimiva 
 |-  ( ph -> A. x e. ( A [,] B ) ( F ` x ) e. RR )
38 36 37 26 rspcdva 
 |-  ( ph -> ( F ` A ) e. RR )
39 3 38 leloed 
 |-  ( ph -> ( U <_ ( F ` A ) <-> ( U < ( F ` A ) \/ U = ( F ` A ) ) ) )
40 34 39 mpbid 
 |-  ( ph -> ( U < ( F ` A ) \/ U = ( F ` A ) ) )
41 40 adantr 
 |-  ( ( ph /\ ( F ` B ) < U ) -> ( U < ( F ` A ) \/ U = ( F ` A ) ) )
42 21 33 41 mpjaodan 
 |-  ( ( ph /\ ( F ` B ) < U ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
43 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
44 22 23 24 43 syl3anc 
 |-  ( ph -> B e. ( A [,] B ) )
45 fveqeq2 
 |-  ( c = B -> ( ( F ` c ) = U <-> ( F ` B ) = U ) )
46 45 rspcev 
 |-  ( ( B e. ( A [,] B ) /\ ( F ` B ) = U ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
47 44 46 sylan 
 |-  ( ( ph /\ ( F ` B ) = U ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
48 8 simpld 
 |-  ( ph -> ( F ` B ) <_ U )
49 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
50 49 eleq1d 
 |-  ( x = B -> ( ( F ` x ) e. RR <-> ( F ` B ) e. RR ) )
51 50 37 44 rspcdva 
 |-  ( ph -> ( F ` B ) e. RR )
52 51 3 leloed 
 |-  ( ph -> ( ( F ` B ) <_ U <-> ( ( F ` B ) < U \/ ( F ` B ) = U ) ) )
53 48 52 mpbid 
 |-  ( ph -> ( ( F ` B ) < U \/ ( F ` B ) = U ) )
54 42 47 53 mpjaodan 
 |-  ( ph -> E. c e. ( A [,] B ) ( F ` c ) = U )