Metamath Proof Explorer


Theorem ivthicc

Description: The interval between any two points of a continuous real function is contained in the range of the function. Equivalently, the range of a continuous real function is convex. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Hypotheses ivthicc.1
|- ( ph -> A e. RR )
ivthicc.2
|- ( ph -> B e. RR )
ivthicc.3
|- ( ph -> M e. ( A [,] B ) )
ivthicc.4
|- ( ph -> N e. ( A [,] B ) )
ivthicc.5
|- ( ph -> ( A [,] B ) C_ D )
ivthicc.7
|- ( ph -> F e. ( D -cn-> CC ) )
ivthicc.8
|- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )
Assertion ivthicc
|- ( ph -> ( ( F ` M ) [,] ( F ` N ) ) C_ ran F )

Proof

Step Hyp Ref Expression
1 ivthicc.1
 |-  ( ph -> A e. RR )
2 ivthicc.2
 |-  ( ph -> B e. RR )
3 ivthicc.3
 |-  ( ph -> M e. ( A [,] B ) )
4 ivthicc.4
 |-  ( ph -> N e. ( A [,] B ) )
5 ivthicc.5
 |-  ( ph -> ( A [,] B ) C_ D )
6 ivthicc.7
 |-  ( ph -> F e. ( D -cn-> CC ) )
7 ivthicc.8
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )
8 simpll
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> ph )
9 elicc2
 |-  ( ( A e. RR /\ B e. RR ) -> ( M e. ( A [,] B ) <-> ( M e. RR /\ A <_ M /\ M <_ B ) ) )
10 1 2 9 syl2anc
 |-  ( ph -> ( M e. ( A [,] B ) <-> ( M e. RR /\ A <_ M /\ M <_ B ) ) )
11 3 10 mpbid
 |-  ( ph -> ( M e. RR /\ A <_ M /\ M <_ B ) )
12 11 simp1d
 |-  ( ph -> M e. RR )
13 12 ad2antrr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> M e. RR )
14 elicc2
 |-  ( ( A e. RR /\ B e. RR ) -> ( N e. ( A [,] B ) <-> ( N e. RR /\ A <_ N /\ N <_ B ) ) )
15 1 2 14 syl2anc
 |-  ( ph -> ( N e. ( A [,] B ) <-> ( N e. RR /\ A <_ N /\ N <_ B ) ) )
16 4 15 mpbid
 |-  ( ph -> ( N e. RR /\ A <_ N /\ N <_ B ) )
17 16 simp1d
 |-  ( ph -> N e. RR )
18 17 ad2antrr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> N e. RR )
19 fveq2
 |-  ( x = M -> ( F ` x ) = ( F ` M ) )
20 19 eleq1d
 |-  ( x = M -> ( ( F ` x ) e. RR <-> ( F ` M ) e. RR ) )
21 7 ralrimiva
 |-  ( ph -> A. x e. ( A [,] B ) ( F ` x ) e. RR )
22 20 21 3 rspcdva
 |-  ( ph -> ( F ` M ) e. RR )
23 fveq2
 |-  ( x = N -> ( F ` x ) = ( F ` N ) )
24 23 eleq1d
 |-  ( x = N -> ( ( F ` x ) e. RR <-> ( F ` N ) e. RR ) )
25 24 21 4 rspcdva
 |-  ( ph -> ( F ` N ) e. RR )
26 iccssre
 |-  ( ( ( F ` M ) e. RR /\ ( F ` N ) e. RR ) -> ( ( F ` M ) [,] ( F ` N ) ) C_ RR )
27 22 25 26 syl2anc
 |-  ( ph -> ( ( F ` M ) [,] ( F ` N ) ) C_ RR )
28 27 sselda
 |-  ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) -> y e. RR )
29 28 adantr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> y e. RR )
30 simpr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> M < N )
31 11 simp2d
 |-  ( ph -> A <_ M )
32 16 simp3d
 |-  ( ph -> N <_ B )
33 iccss
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ M /\ N <_ B ) ) -> ( M [,] N ) C_ ( A [,] B ) )
34 1 2 31 32 33 syl22anc
 |-  ( ph -> ( M [,] N ) C_ ( A [,] B ) )
35 34 5 sstrd
 |-  ( ph -> ( M [,] N ) C_ D )
36 35 ad2antrr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> ( M [,] N ) C_ D )
37 6 ad2antrr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> F e. ( D -cn-> CC ) )
38 34 sselda
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> x e. ( A [,] B ) )
39 38 7 syldan
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( F ` x ) e. RR )
40 8 39 sylan
 |-  ( ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) /\ x e. ( M [,] N ) ) -> ( F ` x ) e. RR )
41 elicc2
 |-  ( ( ( F ` M ) e. RR /\ ( F ` N ) e. RR ) -> ( y e. ( ( F ` M ) [,] ( F ` N ) ) <-> ( y e. RR /\ ( F ` M ) <_ y /\ y <_ ( F ` N ) ) ) )
42 22 25 41 syl2anc
 |-  ( ph -> ( y e. ( ( F ` M ) [,] ( F ` N ) ) <-> ( y e. RR /\ ( F ` M ) <_ y /\ y <_ ( F ` N ) ) ) )
43 42 biimpa
 |-  ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) -> ( y e. RR /\ ( F ` M ) <_ y /\ y <_ ( F ` N ) ) )
44 3simpc
 |-  ( ( y e. RR /\ ( F ` M ) <_ y /\ y <_ ( F ` N ) ) -> ( ( F ` M ) <_ y /\ y <_ ( F ` N ) ) )
45 43 44 syl
 |-  ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) -> ( ( F ` M ) <_ y /\ y <_ ( F ` N ) ) )
46 45 adantr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> ( ( F ` M ) <_ y /\ y <_ ( F ` N ) ) )
47 13 18 29 30 36 37 40 46 ivthle
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> E. z e. ( M [,] N ) ( F ` z ) = y )
48 35 sselda
 |-  ( ( ph /\ z e. ( M [,] N ) ) -> z e. D )
49 cncff
 |-  ( F e. ( D -cn-> CC ) -> F : D --> CC )
50 ffn
 |-  ( F : D --> CC -> F Fn D )
51 6 49 50 3syl
 |-  ( ph -> F Fn D )
52 fnfvelrn
 |-  ( ( F Fn D /\ z e. D ) -> ( F ` z ) e. ran F )
53 51 52 sylan
 |-  ( ( ph /\ z e. D ) -> ( F ` z ) e. ran F )
54 eleq1
 |-  ( ( F ` z ) = y -> ( ( F ` z ) e. ran F <-> y e. ran F ) )
55 53 54 syl5ibcom
 |-  ( ( ph /\ z e. D ) -> ( ( F ` z ) = y -> y e. ran F ) )
56 48 55 syldan
 |-  ( ( ph /\ z e. ( M [,] N ) ) -> ( ( F ` z ) = y -> y e. ran F ) )
57 56 rexlimdva
 |-  ( ph -> ( E. z e. ( M [,] N ) ( F ` z ) = y -> y e. ran F ) )
58 8 47 57 sylc
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M < N ) -> y e. ran F )
59 simplr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> y e. ( ( F ` M ) [,] ( F ` N ) ) )
60 simpr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> M = N )
61 60 fveq2d
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> ( F ` M ) = ( F ` N ) )
62 61 oveq2d
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> ( ( F ` M ) [,] ( F ` M ) ) = ( ( F ` M ) [,] ( F ` N ) ) )
63 22 rexrd
 |-  ( ph -> ( F ` M ) e. RR* )
64 63 ad2antrr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> ( F ` M ) e. RR* )
65 iccid
 |-  ( ( F ` M ) e. RR* -> ( ( F ` M ) [,] ( F ` M ) ) = { ( F ` M ) } )
66 64 65 syl
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> ( ( F ` M ) [,] ( F ` M ) ) = { ( F ` M ) } )
67 62 66 eqtr3d
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> ( ( F ` M ) [,] ( F ` N ) ) = { ( F ` M ) } )
68 59 67 eleqtrd
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> y e. { ( F ` M ) } )
69 elsni
 |-  ( y e. { ( F ` M ) } -> y = ( F ` M ) )
70 68 69 syl
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> y = ( F ` M ) )
71 5 3 sseldd
 |-  ( ph -> M e. D )
72 fnfvelrn
 |-  ( ( F Fn D /\ M e. D ) -> ( F ` M ) e. ran F )
73 51 71 72 syl2anc
 |-  ( ph -> ( F ` M ) e. ran F )
74 73 ad2antrr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> ( F ` M ) e. ran F )
75 70 74 eqeltrd
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ M = N ) -> y e. ran F )
76 simpll
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> ph )
77 17 ad2antrr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> N e. RR )
78 12 ad2antrr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> M e. RR )
79 28 adantr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> y e. RR )
80 simpr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> N < M )
81 16 simp2d
 |-  ( ph -> A <_ N )
82 11 simp3d
 |-  ( ph -> M <_ B )
83 iccss
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ N /\ M <_ B ) ) -> ( N [,] M ) C_ ( A [,] B ) )
84 1 2 81 82 83 syl22anc
 |-  ( ph -> ( N [,] M ) C_ ( A [,] B ) )
85 84 5 sstrd
 |-  ( ph -> ( N [,] M ) C_ D )
86 85 ad2antrr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> ( N [,] M ) C_ D )
87 6 ad2antrr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> F e. ( D -cn-> CC ) )
88 84 sselda
 |-  ( ( ph /\ x e. ( N [,] M ) ) -> x e. ( A [,] B ) )
89 88 7 syldan
 |-  ( ( ph /\ x e. ( N [,] M ) ) -> ( F ` x ) e. RR )
90 76 89 sylan
 |-  ( ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) /\ x e. ( N [,] M ) ) -> ( F ` x ) e. RR )
91 45 adantr
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> ( ( F ` M ) <_ y /\ y <_ ( F ` N ) ) )
92 77 78 79 80 86 87 90 91 ivthle2
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> E. z e. ( N [,] M ) ( F ` z ) = y )
93 85 sselda
 |-  ( ( ph /\ z e. ( N [,] M ) ) -> z e. D )
94 93 55 syldan
 |-  ( ( ph /\ z e. ( N [,] M ) ) -> ( ( F ` z ) = y -> y e. ran F ) )
95 94 rexlimdva
 |-  ( ph -> ( E. z e. ( N [,] M ) ( F ` z ) = y -> y e. ran F ) )
96 76 92 95 sylc
 |-  ( ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) /\ N < M ) -> y e. ran F )
97 12 17 lttri4d
 |-  ( ph -> ( M < N \/ M = N \/ N < M ) )
98 97 adantr
 |-  ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) -> ( M < N \/ M = N \/ N < M ) )
99 58 75 96 98 mpjao3dan
 |-  ( ( ph /\ y e. ( ( F ` M ) [,] ( F ` N ) ) ) -> y e. ran F )
100 99 ex
 |-  ( ph -> ( y e. ( ( F ` M ) [,] ( F ` N ) ) -> y e. ran F ) )
101 100 ssrdv
 |-  ( ph -> ( ( F ` M ) [,] ( F ` N ) ) C_ ran F )