Metamath Proof Explorer

Theorem ivth2

Description: The intermediate value theorem, decreasing case. (Contributed by Paul Chapman, 22-Jan-2008) (Revised by Mario Carneiro, 30-Apr-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 )
ivth2.9 
|- ( ph -> ( ( F ` B ) < U /\ U < ( F ` A ) ) )
Assertion ivth2 
|- ( 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 ivth2.9 
 |-  ( ph -> ( ( F ` B ) < U /\ U < ( F ` A ) ) )
9 3 renegcld 
 |-  ( ph -> -u U e. RR )
10 eqid 
 |-  ( y e. D |-> -u ( F ` y ) ) = ( y e. D |-> -u ( F ` y ) )
11 10 negfcncf 
 |-  ( F e. ( D -cn-> CC ) -> ( y e. D |-> -u ( F ` y ) ) e. ( D -cn-> CC ) )
12 6 11 syl 
 |-  ( ph -> ( y e. D |-> -u ( F ` y ) ) e. ( D -cn-> CC ) )
13 5 sselda 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. D )
14 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
15 14 negeqd 
 |-  ( y = x -> -u ( F ` y ) = -u ( F ` x ) )
16 negex 
 |-  -u ( F ` x ) e. _V
17 15 10 16 fvmpt 
 |-  ( x e. D -> ( ( y e. D |-> -u ( F ` y ) ) ` x ) = -u ( F ` x ) )
18 13 17 syl 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( y e. D |-> -u ( F ` y ) ) ` x ) = -u ( F ` x ) )
19 7 renegcld 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> -u ( F ` x ) e. RR )
20 18 19 eqeltrd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( y e. D |-> -u ( F ` y ) ) ` x ) e. RR )
21 1 rexrd 
 |-  ( ph -> A e. RR* )
22 2 rexrd 
 |-  ( ph -> B e. RR* )
23 1 2 4 ltled 
 |-  ( ph -> A <_ B )
24 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
25 21 22 23 24 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
26 5 25 sseldd 
 |-  ( ph -> A e. D )
27 fveq2 
 |-  ( y = A -> ( F ` y ) = ( F ` A ) )
28 27 negeqd 
 |-  ( y = A -> -u ( F ` y ) = -u ( F ` A ) )
29 negex 
 |-  -u ( F ` A ) e. _V
30 28 10 29 fvmpt 
 |-  ( A e. D -> ( ( y e. D |-> -u ( F ` y ) ) ` A ) = -u ( F ` A ) )
31 26 30 syl 
 |-  ( ph -> ( ( y e. D |-> -u ( F ` y ) ) ` A ) = -u ( F ` A ) )
32 8 simprd 
 |-  ( ph -> U < ( F ` A ) )
33 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
34 33 eleq1d 
 |-  ( x = A -> ( ( F ` x ) e. RR <-> ( F ` A ) e. RR ) )
35 7 ralrimiva 
 |-  ( ph -> A. x e. ( A [,] B ) ( F ` x ) e. RR )
36 34 35 25 rspcdva 
 |-  ( ph -> ( F ` A ) e. RR )
37 3 36 ltnegd 
 |-  ( ph -> ( U < ( F ` A ) <-> -u ( F ` A ) < -u U ) )
38 32 37 mpbid 
 |-  ( ph -> -u ( F ` A ) < -u U )
39 31 38 eqbrtrd 
 |-  ( ph -> ( ( y e. D |-> -u ( F ` y ) ) ` A ) < -u U )
40 8 simpld 
 |-  ( ph -> ( F ` B ) < U )
41 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
42 41 eleq1d 
 |-  ( x = B -> ( ( F ` x ) e. RR <-> ( F ` B ) e. RR ) )
43 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
44 21 22 23 43 syl3anc 
 |-  ( ph -> B e. ( A [,] B ) )
45 42 35 44 rspcdva 
 |-  ( ph -> ( F ` B ) e. RR )
46 45 3 ltnegd 
 |-  ( ph -> ( ( F ` B ) < U <-> -u U < -u ( F ` B ) ) )
47 40 46 mpbid 
 |-  ( ph -> -u U < -u ( F ` B ) )
48 5 44 sseldd 
 |-  ( ph -> B e. D )
49 fveq2 
 |-  ( y = B -> ( F ` y ) = ( F ` B ) )
50 49 negeqd 
 |-  ( y = B -> -u ( F ` y ) = -u ( F ` B ) )
51 negex 
 |-  -u ( F ` B ) e. _V
52 50 10 51 fvmpt 
 |-  ( B e. D -> ( ( y e. D |-> -u ( F ` y ) ) ` B ) = -u ( F ` B ) )
53 48 52 syl 
 |-  ( ph -> ( ( y e. D |-> -u ( F ` y ) ) ` B ) = -u ( F ` B ) )
54 47 53 breqtrrd 
 |-  ( ph -> -u U < ( ( y e. D |-> -u ( F ` y ) ) ` B ) )
55 39 54 jca 
 |-  ( ph -> ( ( ( y e. D |-> -u ( F ` y ) ) ` A ) < -u U /\ -u U < ( ( y e. D |-> -u ( F ` y ) ) ` B ) ) )
56 1 2 9 4 5 12 20 55 ivth 
 |-  ( ph -> E. c e. ( A (,) B ) ( ( y e. D |-> -u ( F ` y ) ) ` c ) = -u U )
57 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
58 57 5 sstrid 
 |-  ( ph -> ( A (,) B ) C_ D )
59 58 sselda 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> c e. D )
60 fveq2 
 |-  ( y = c -> ( F ` y ) = ( F ` c ) )
61 60 negeqd 
 |-  ( y = c -> -u ( F ` y ) = -u ( F ` c ) )
62 negex 
 |-  -u ( F ` c ) e. _V
63 61 10 62 fvmpt 
 |-  ( c e. D -> ( ( y e. D |-> -u ( F ` y ) ) ` c ) = -u ( F ` c ) )
64 59 63 syl 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( ( y e. D |-> -u ( F ` y ) ) ` c ) = -u ( F ` c ) )
65 64 eqeq1d 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( ( ( y e. D |-> -u ( F ` y ) ) ` c ) = -u U <-> -u ( F ` c ) = -u U ) )
66 cncff 
 |-  ( F e. ( D -cn-> CC ) -> F : D --> CC )
67 6 66 syl 
 |-  ( ph -> F : D --> CC )
68 67 ffvelrnda 
 |-  ( ( ph /\ c e. D ) -> ( F ` c ) e. CC )
69 59 68 syldan 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( F ` c ) e. CC )
70 3 recnd 
 |-  ( ph -> U e. CC )
71 70 adantr 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> U e. CC )
72 69 71 neg11ad 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( -u ( F ` c ) = -u U <-> ( F ` c ) = U ) )
73 65 72 bitrd 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( ( ( y e. D |-> -u ( F ` y ) ) ` c ) = -u U <-> ( F ` c ) = U ) )
74 73 rexbidva 
 |-  ( ph -> ( E. c e. ( A (,) B ) ( ( y e. D |-> -u ( F ` y ) ) ` c ) = -u U <-> E. c e. ( A (,) B ) ( F ` c ) = U ) )
75 56 74 mpbid 
 |-  ( ph -> E. c e. ( A (,) B ) ( F ` c ) = U )