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	$⊢ φ \to A \in ℝ$
	ivthicc.2	$⊢ φ \to B \in ℝ$
	ivthicc.3	$⊢ φ \to M \in [A, B]$
	ivthicc.4	$⊢ φ \to N \in [A, B]$
	ivthicc.5	$⊢ φ \to [A, B] \subseteq D$
	ivthicc.7	$⊢ φ \to F : D \underset{cn}{⟶} ℂ$
	ivthicc.8	$⊢ (φ \land x \in [A, B]) \to F (x) \in ℝ$
Assertion	ivthicc	$⊢ φ \to [F (M), F (N)] \subseteq ran F$

Proof

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

Metamath Proof Explorer

Theorem ivthicc

Proof