dvivthlem2

Step	Hyp	Ref	Expression
1		dvivth.1	$⊢ φ \to M \in (A, B)$
2		dvivth.2	$⊢ φ \to N \in (A, B)$
3		dvivth.3	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℝ$
4		dvivth.4	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
5		dvivth.5	$⊢ φ \to M < N$
6		dvivth.6	$⊢ φ \to C \in [F_{ℝ}^{'} (N), F_{ℝ}^{'} (M)]$
7		dvivth.7	$⊢ G = (y \in (A, B) ⟼ F (y) - C y)$
8	1 2 3 4 5 6 7	dvivthlem1	$⊢ φ \to \exists x \in [M, N] F_{ℝ}^{'} (x) = C$
9		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
10	4	feq2d	$⊢ φ \to (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \leftrightarrow F_{ℝ}^{'} : (A, B) ⟶ ℂ)$
11	9 10	mpbii	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
12	11	ffnd	$⊢ φ \to F_{ℝ}^{'} Fn (A, B)$
13		iccssioo2	$⊢ (M \in (A, B) \land N \in (A, B)) \to [M, N] \subseteq (A, B)$
14	1 2 13	syl2anc	$⊢ φ \to [M, N] \subseteq (A, B)$
15	14	sselda	$⊢ (φ \land x \in [M, N]) \to x \in (A, B)$
16		fnfvelrn	$⊢ (F_{ℝ}^{'} Fn (A, B) \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ran F_{ℝ}^{'}$
17	12 15 16	syl2an2r	$⊢ (φ \land x \in [M, N]) \to F_{ℝ}^{'} (x) \in ran F_{ℝ}^{'}$
18		eleq1	$⊢ F_{ℝ}^{'} (x) = C \to (F_{ℝ}^{'} (x) \in ran F_{ℝ}^{'} \leftrightarrow C \in ran F_{ℝ}^{'})$
19	17 18	syl5ibcom	$⊢ (φ \land x \in [M, N]) \to (F_{ℝ}^{'} (x) = C \to C \in ran F_{ℝ}^{'})$
20	19	rexlimdva	$⊢ φ \to (\exists x \in [M, N] F_{ℝ}^{'} (x) = C \to C \in ran F_{ℝ}^{'})$
21	8 20	mpd	$⊢ φ \to C \in ran F_{ℝ}^{'}$

Metamath Proof Explorer