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 ( 𝜑𝐴 ∈ ℝ )
ivthicc.2 ( 𝜑𝐵 ∈ ℝ )
ivthicc.3 ( 𝜑𝑀 ∈ ( 𝐴 [,] 𝐵 ) )
ivthicc.4 ( 𝜑𝑁 ∈ ( 𝐴 [,] 𝐵 ) )
ivthicc.5 ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 )
ivthicc.7 ( 𝜑𝐹 ∈ ( 𝐷cn→ ℂ ) )
ivthicc.8 ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹𝑥 ) ∈ ℝ )
Assertion ivthicc ( 𝜑 → ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ⊆ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 ivthicc.1 ( 𝜑𝐴 ∈ ℝ )
2 ivthicc.2 ( 𝜑𝐵 ∈ ℝ )
3 ivthicc.3 ( 𝜑𝑀 ∈ ( 𝐴 [,] 𝐵 ) )
4 ivthicc.4 ( 𝜑𝑁 ∈ ( 𝐴 [,] 𝐵 ) )
5 ivthicc.5 ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 )
6 ivthicc.7 ( 𝜑𝐹 ∈ ( 𝐷cn→ ℂ ) )
7 ivthicc.8 ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹𝑥 ) ∈ ℝ )
8 simpll ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝜑 )
9 elicc2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑀 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑀 ∈ ℝ ∧ 𝐴𝑀𝑀𝐵 ) ) )
10 1 2 9 syl2anc ( 𝜑 → ( 𝑀 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑀 ∈ ℝ ∧ 𝐴𝑀𝑀𝐵 ) ) )
11 3 10 mpbid ( 𝜑 → ( 𝑀 ∈ ℝ ∧ 𝐴𝑀𝑀𝐵 ) )
12 11 simp1d ( 𝜑𝑀 ∈ ℝ )
13 12 ad2antrr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝑀 ∈ ℝ )
14 elicc2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑁 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑁 ∈ ℝ ∧ 𝐴𝑁𝑁𝐵 ) ) )
15 1 2 14 syl2anc ( 𝜑 → ( 𝑁 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑁 ∈ ℝ ∧ 𝐴𝑁𝑁𝐵 ) ) )
16 4 15 mpbid ( 𝜑 → ( 𝑁 ∈ ℝ ∧ 𝐴𝑁𝑁𝐵 ) )
17 16 simp1d ( 𝜑𝑁 ∈ ℝ )
18 17 ad2antrr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝑁 ∈ ℝ )
19 fveq2 ( 𝑥 = 𝑀 → ( 𝐹𝑥 ) = ( 𝐹𝑀 ) )
20 19 eleq1d ( 𝑥 = 𝑀 → ( ( 𝐹𝑥 ) ∈ ℝ ↔ ( 𝐹𝑀 ) ∈ ℝ ) )
21 7 ralrimiva ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹𝑥 ) ∈ ℝ )
22 20 21 3 rspcdva ( 𝜑 → ( 𝐹𝑀 ) ∈ ℝ )
23 fveq2 ( 𝑥 = 𝑁 → ( 𝐹𝑥 ) = ( 𝐹𝑁 ) )
24 23 eleq1d ( 𝑥 = 𝑁 → ( ( 𝐹𝑥 ) ∈ ℝ ↔ ( 𝐹𝑁 ) ∈ ℝ ) )
25 24 21 4 rspcdva ( 𝜑 → ( 𝐹𝑁 ) ∈ ℝ )
26 iccssre ( ( ( 𝐹𝑀 ) ∈ ℝ ∧ ( 𝐹𝑁 ) ∈ ℝ ) → ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ⊆ ℝ )
27 22 25 26 syl2anc ( 𝜑 → ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ⊆ ℝ )
28 27 sselda ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) → 𝑦 ∈ ℝ )
29 28 adantr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝑦 ∈ ℝ )
30 simpr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝑀 < 𝑁 )
31 11 simp2d ( 𝜑𝐴𝑀 )
32 16 simp3d ( 𝜑𝑁𝐵 )
33 iccss ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴𝑀𝑁𝐵 ) ) → ( 𝑀 [,] 𝑁 ) ⊆ ( 𝐴 [,] 𝐵 ) )
34 1 2 31 32 33 syl22anc ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ( 𝐴 [,] 𝐵 ) )
35 34 5 sstrd ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ 𝐷 )
36 35 ad2antrr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → ( 𝑀 [,] 𝑁 ) ⊆ 𝐷 )
37 6 ad2antrr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝐹 ∈ ( 𝐷cn→ ℂ ) )
38 34 sselda ( ( 𝜑𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
39 38 7 syldan ( ( 𝜑𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝐹𝑥 ) ∈ ℝ )
40 8 39 sylan ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝐹𝑥 ) ∈ ℝ )
41 elicc2 ( ( ( 𝐹𝑀 ) ∈ ℝ ∧ ( 𝐹𝑁 ) ∈ ℝ ) → ( 𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( 𝐹𝑀 ) ≤ 𝑦𝑦 ≤ ( 𝐹𝑁 ) ) ) )
42 22 25 41 syl2anc ( 𝜑 → ( 𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( 𝐹𝑀 ) ≤ 𝑦𝑦 ≤ ( 𝐹𝑁 ) ) ) )
43 42 biimpa ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) → ( 𝑦 ∈ ℝ ∧ ( 𝐹𝑀 ) ≤ 𝑦𝑦 ≤ ( 𝐹𝑁 ) ) )
44 3simpc ( ( 𝑦 ∈ ℝ ∧ ( 𝐹𝑀 ) ≤ 𝑦𝑦 ≤ ( 𝐹𝑁 ) ) → ( ( 𝐹𝑀 ) ≤ 𝑦𝑦 ≤ ( 𝐹𝑁 ) ) )
45 43 44 syl ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) → ( ( 𝐹𝑀 ) ≤ 𝑦𝑦 ≤ ( 𝐹𝑁 ) ) )
46 45 adantr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → ( ( 𝐹𝑀 ) ≤ 𝑦𝑦 ≤ ( 𝐹𝑁 ) ) )
47 13 18 29 30 36 37 40 46 ivthle ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → ∃ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( 𝐹𝑧 ) = 𝑦 )
48 35 sselda ( ( 𝜑𝑧 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑧𝐷 )
49 cncff ( 𝐹 ∈ ( 𝐷cn→ ℂ ) → 𝐹 : 𝐷 ⟶ ℂ )
50 ffn ( 𝐹 : 𝐷 ⟶ ℂ → 𝐹 Fn 𝐷 )
51 6 49 50 3syl ( 𝜑𝐹 Fn 𝐷 )
52 fnfvelrn ( ( 𝐹 Fn 𝐷𝑧𝐷 ) → ( 𝐹𝑧 ) ∈ ran 𝐹 )
53 51 52 sylan ( ( 𝜑𝑧𝐷 ) → ( 𝐹𝑧 ) ∈ ran 𝐹 )
54 eleq1 ( ( 𝐹𝑧 ) = 𝑦 → ( ( 𝐹𝑧 ) ∈ ran 𝐹𝑦 ∈ ran 𝐹 ) )
55 53 54 syl5ibcom ( ( 𝜑𝑧𝐷 ) → ( ( 𝐹𝑧 ) = 𝑦𝑦 ∈ ran 𝐹 ) )
56 48 55 syldan ( ( 𝜑𝑧 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ( 𝐹𝑧 ) = 𝑦𝑦 ∈ ran 𝐹 ) )
57 56 rexlimdva ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( 𝐹𝑧 ) = 𝑦𝑦 ∈ ran 𝐹 ) )
58 8 47 57 sylc ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝑦 ∈ ran 𝐹 )
59 simplr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → 𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) )
60 simpr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → 𝑀 = 𝑁 )
61 60 fveq2d ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → ( 𝐹𝑀 ) = ( 𝐹𝑁 ) )
62 61 oveq2d ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → ( ( 𝐹𝑀 ) [,] ( 𝐹𝑀 ) ) = ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) )
63 22 rexrd ( 𝜑 → ( 𝐹𝑀 ) ∈ ℝ* )
64 63 ad2antrr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → ( 𝐹𝑀 ) ∈ ℝ* )
65 iccid ( ( 𝐹𝑀 ) ∈ ℝ* → ( ( 𝐹𝑀 ) [,] ( 𝐹𝑀 ) ) = { ( 𝐹𝑀 ) } )
66 64 65 syl ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → ( ( 𝐹𝑀 ) [,] ( 𝐹𝑀 ) ) = { ( 𝐹𝑀 ) } )
67 62 66 eqtr3d ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) = { ( 𝐹𝑀 ) } )
68 59 67 eleqtrd ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → 𝑦 ∈ { ( 𝐹𝑀 ) } )
69 elsni ( 𝑦 ∈ { ( 𝐹𝑀 ) } → 𝑦 = ( 𝐹𝑀 ) )
70 68 69 syl ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → 𝑦 = ( 𝐹𝑀 ) )
71 5 3 sseldd ( 𝜑𝑀𝐷 )
72 fnfvelrn ( ( 𝐹 Fn 𝐷𝑀𝐷 ) → ( 𝐹𝑀 ) ∈ ran 𝐹 )
73 51 71 72 syl2anc ( 𝜑 → ( 𝐹𝑀 ) ∈ ran 𝐹 )
74 73 ad2antrr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → ( 𝐹𝑀 ) ∈ ran 𝐹 )
75 70 74 eqeltrd ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → 𝑦 ∈ ran 𝐹 )
76 simpll ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝜑 )
77 17 ad2antrr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝑁 ∈ ℝ )
78 12 ad2antrr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝑀 ∈ ℝ )
79 28 adantr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝑦 ∈ ℝ )
80 simpr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝑁 < 𝑀 )
81 16 simp2d ( 𝜑𝐴𝑁 )
82 11 simp3d ( 𝜑𝑀𝐵 )
83 iccss ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴𝑁𝑀𝐵 ) ) → ( 𝑁 [,] 𝑀 ) ⊆ ( 𝐴 [,] 𝐵 ) )
84 1 2 81 82 83 syl22anc ( 𝜑 → ( 𝑁 [,] 𝑀 ) ⊆ ( 𝐴 [,] 𝐵 ) )
85 84 5 sstrd ( 𝜑 → ( 𝑁 [,] 𝑀 ) ⊆ 𝐷 )
86 85 ad2antrr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → ( 𝑁 [,] 𝑀 ) ⊆ 𝐷 )
87 6 ad2antrr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝐹 ∈ ( 𝐷cn→ ℂ ) )
88 84 sselda ( ( 𝜑𝑥 ∈ ( 𝑁 [,] 𝑀 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
89 88 7 syldan ( ( 𝜑𝑥 ∈ ( 𝑁 [,] 𝑀 ) ) → ( 𝐹𝑥 ) ∈ ℝ )
90 76 89 sylan ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) ∧ 𝑥 ∈ ( 𝑁 [,] 𝑀 ) ) → ( 𝐹𝑥 ) ∈ ℝ )
91 45 adantr ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → ( ( 𝐹𝑀 ) ≤ 𝑦𝑦 ≤ ( 𝐹𝑁 ) ) )
92 77 78 79 80 86 87 90 91 ivthle2 ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → ∃ 𝑧 ∈ ( 𝑁 [,] 𝑀 ) ( 𝐹𝑧 ) = 𝑦 )
93 85 sselda ( ( 𝜑𝑧 ∈ ( 𝑁 [,] 𝑀 ) ) → 𝑧𝐷 )
94 93 55 syldan ( ( 𝜑𝑧 ∈ ( 𝑁 [,] 𝑀 ) ) → ( ( 𝐹𝑧 ) = 𝑦𝑦 ∈ ran 𝐹 ) )
95 94 rexlimdva ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝑁 [,] 𝑀 ) ( 𝐹𝑧 ) = 𝑦𝑦 ∈ ran 𝐹 ) )
96 76 92 95 sylc ( ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝑦 ∈ ran 𝐹 )
97 12 17 lttri4d ( 𝜑 → ( 𝑀 < 𝑁𝑀 = 𝑁𝑁 < 𝑀 ) )
98 97 adantr ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) → ( 𝑀 < 𝑁𝑀 = 𝑁𝑁 < 𝑀 ) )
99 58 75 96 98 mpjao3dan ( ( 𝜑𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ) → 𝑦 ∈ ran 𝐹 )
100 99 ex ( 𝜑 → ( 𝑦 ∈ ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) → 𝑦 ∈ ran 𝐹 ) )
101 100 ssrdv ( 𝜑 → ( ( 𝐹𝑀 ) [,] ( 𝐹𝑁 ) ) ⊆ ran 𝐹 )