Metamath Proof Explorer


Theorem ivthle

Description: The intermediate value theorem with weak inequality, increasing case. (Contributed by Mario Carneiro, 12-Aug-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 )
ivthle.9
|- ( ph -> ( ( F ` A ) <_ U /\ U <_ ( F ` B ) ) )
Assertion ivthle
|- ( 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 ivthle.9
 |-  ( ph -> ( ( F ` A ) <_ U /\ U <_ ( F ` B ) ) )
9 ioossicc
 |-  ( A (,) B ) C_ ( A [,] B )
10 1 adantr
 |-  ( ( ph /\ ( ( F ` A ) < U /\ U < ( F ` B ) ) ) -> A e. RR )
11 2 adantr
 |-  ( ( ph /\ ( ( F ` A ) < U /\ U < ( F ` B ) ) ) -> B e. RR )
12 3 adantr
 |-  ( ( ph /\ ( ( F ` A ) < U /\ U < ( F ` B ) ) ) -> U e. RR )
13 4 adantr
 |-  ( ( ph /\ ( ( F ` A ) < U /\ U < ( F ` B ) ) ) -> A < B )
14 5 adantr
 |-  ( ( ph /\ ( ( F ` A ) < U /\ U < ( F ` B ) ) ) -> ( A [,] B ) C_ D )
15 6 adantr
 |-  ( ( ph /\ ( ( F ` A ) < U /\ U < ( F ` B ) ) ) -> F e. ( D -cn-> CC ) )
16 7 adantlr
 |-  ( ( ( ph /\ ( ( F ` A ) < U /\ U < ( F ` B ) ) ) /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )
17 simpr
 |-  ( ( ph /\ ( ( F ` A ) < U /\ U < ( F ` B ) ) ) -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )
18 10 11 12 13 14 15 16 17 ivth
 |-  ( ( ph /\ ( ( F ` A ) < U /\ U < ( F ` B ) ) ) -> 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 ` A ) < U /\ U < ( F ` B ) ) ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
21 20 anassrs
 |-  ( ( ( ph /\ ( F ` A ) < U ) /\ U < ( F ` B ) ) -> 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 ubicc2
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
26 22 23 24 25 syl3anc
 |-  ( ph -> B e. ( A [,] B ) )
27 eqcom
 |-  ( ( F ` c ) = U <-> U = ( F ` c ) )
28 fveq2
 |-  ( c = B -> ( F ` c ) = ( F ` B ) )
29 28 eqeq2d
 |-  ( c = B -> ( U = ( F ` c ) <-> U = ( F ` B ) ) )
30 27 29 syl5bb
 |-  ( c = B -> ( ( F ` c ) = U <-> U = ( F ` B ) ) )
31 30 rspcev
 |-  ( ( B e. ( A [,] B ) /\ U = ( F ` B ) ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
32 26 31 sylan
 |-  ( ( ph /\ U = ( F ` B ) ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
33 32 adantlr
 |-  ( ( ( ph /\ ( F ` A ) < U ) /\ U = ( F ` B ) ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
34 8 simprd
 |-  ( ph -> U <_ ( F ` B ) )
35 fveq2
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
36 35 eleq1d
 |-  ( x = B -> ( ( F ` x ) e. RR <-> ( F ` B ) e. RR ) )
37 7 ralrimiva
 |-  ( ph -> A. x e. ( A [,] B ) ( F ` x ) e. RR )
38 36 37 26 rspcdva
 |-  ( ph -> ( F ` B ) e. RR )
39 3 38 leloed
 |-  ( ph -> ( U <_ ( F ` B ) <-> ( U < ( F ` B ) \/ U = ( F ` B ) ) ) )
40 34 39 mpbid
 |-  ( ph -> ( U < ( F ` B ) \/ U = ( F ` B ) ) )
41 40 adantr
 |-  ( ( ph /\ ( F ` A ) < U ) -> ( U < ( F ` B ) \/ U = ( F ` B ) ) )
42 21 33 41 mpjaodan
 |-  ( ( ph /\ ( F ` A ) < U ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
43 lbicc2
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
44 22 23 24 43 syl3anc
 |-  ( ph -> A e. ( A [,] B ) )
45 fveqeq2
 |-  ( c = A -> ( ( F ` c ) = U <-> ( F ` A ) = U ) )
46 45 rspcev
 |-  ( ( A e. ( A [,] B ) /\ ( F ` A ) = U ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
47 44 46 sylan
 |-  ( ( ph /\ ( F ` A ) = U ) -> E. c e. ( A [,] B ) ( F ` c ) = U )
48 8 simpld
 |-  ( ph -> ( F ` A ) <_ U )
49 fveq2
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
50 49 eleq1d
 |-  ( x = A -> ( ( F ` x ) e. RR <-> ( F ` A ) e. RR ) )
51 50 37 44 rspcdva
 |-  ( ph -> ( F ` A ) e. RR )
52 51 3 leloed
 |-  ( ph -> ( ( F ` A ) <_ U <-> ( ( F ` A ) < U \/ ( F ` A ) = U ) ) )
53 48 52 mpbid
 |-  ( ph -> ( ( F ` A ) < U \/ ( F ` A ) = U ) )
54 42 47 53 mpjaodan
 |-  ( ph -> E. c e. ( A [,] B ) ( F ` c ) = U )