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 )