Metamath Proof Explorer

Theorem ivth

Description: The intermediate value theorem, increasing case. This is Metamath 100 proof #79. (Contributed by Paul Chapman, 22-Jan-2008) (Proof shortened by Mario Carneiro, 30-Apr-2014)

		Ref	Expression
	Hypotheses	ivth.1	$⊢ φ \to A \in ℝ$
		ivth.2	$⊢ φ \to B \in ℝ$
		ivth.3	$⊢ φ \to U \in ℝ$
		ivth.4	$⊢ φ \to A < B$
		ivth.5	$⊢ φ \to [A, B] \subseteq D$
		ivth.7	$⊢ φ \to F : D \underset{cn}{⟶} ℂ$
		ivth.8	$⊢ (φ \land x \in [A, B]) \to F (x) \in ℝ$
		ivth.9	$⊢ φ \to (F (A) < U \land U < F (B))$
	Assertion	ivth	$⊢ φ \to \exists c \in (A, B) F (c) = U$

Proof

Step	Hyp	Ref	Expression
1		ivth.1	$⊢ φ \to A \in ℝ$
2		ivth.2	$⊢ φ \to B \in ℝ$
3		ivth.3	$⊢ φ \to U \in ℝ$
4		ivth.4	$⊢ φ \to A < B$
5		ivth.5	$⊢ φ \to [A, B] \subseteq D$
6		ivth.7	$⊢ φ \to F : D \underset{cn}{⟶} ℂ$
7		ivth.8	$⊢ (φ \land x \in [A, B]) \to F (x) \in ℝ$
8		ivth.9	$⊢ φ \to (F (A) < U \land U < F (B))$
9		fveq2	$⊢ y = x \to F (y) = F (x)$
10	9	breq1d	$⊢ y = x \to (F (y) \leq U \leftrightarrow F (x) \leq U)$
11	10	cbvrabv	$⊢ \{y \in [A, B] \| F (y) \leq U\} = \{x \in [A, B] \| F (x) \leq U\}$
12		eqid	$⊢ sup (\{y \in [A, B] \| F (y) \leq U\} ℝ <) = sup (\{y \in [A, B] \| F (y) \leq U\} ℝ <)$
13	1 2 3 4 5 6 7 8 11 12	ivthlem3	$⊢ φ \to (sup (\{y \in [A, B] \| F (y) \leq U\} ℝ <) \in (A, B) \land F (sup (\{y \in [A, B] \| F (y) \leq U\} ℝ <)) = U)$
14		fveqeq2	$⊢ c = sup (\{y \in [A, B] \| F (y) \leq U\} ℝ <) \to (F (c) = U \leftrightarrow F (sup (\{y \in [A, B] \| F (y) \leq U\} ℝ <)) = U)$
15	14	rspcev	$⊢ (sup (\{y \in [A, B] \| F (y) \leq U\} ℝ <) \in (A, B) \land F (sup (\{y \in [A, B] \| F (y) \leq U\} ℝ <)) = U) \to \exists c \in (A, B) F (c) = U$
16	13 15	syl	$⊢ φ \to \exists c \in (A, B) F (c) = U$