Theorem dvivthlem2

Description: Lemma for dvivth . (Contributed by Mario Carneiro, 20-Feb-2015)

	Ref	Expression
Hypotheses	dvivth.1	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐴 (,) 𝐵 ) )
	dvivth.2	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐴 (,) 𝐵 ) )
	dvivth.3	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
	dvivth.4	⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
	dvivth.5	⊢ ( 𝜑 → 𝑀 < 𝑁 )
	dvivth.6	⊢ ( 𝜑 → 𝐶 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) )
	dvivth.7	⊢ 𝐺 = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐶 · 𝑦 ) ) )
Assertion	dvivthlem2	⊢ ( 𝜑 → 𝐶 ∈ ran ( ℝ D 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		dvivth.1	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐴 (,) 𝐵 ) )
2		dvivth.2	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐴 (,) 𝐵 ) )
3		dvivth.3	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
4		dvivth.4	⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
5		dvivth.5	⊢ ( 𝜑 → 𝑀 < 𝑁 )
6		dvivth.6	⊢ ( 𝜑 → 𝐶 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) )
7		dvivth.7	⊢ 𝐺 = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐶 · 𝑦 ) ) )
8	1 2 3 4 5 6 7	dvivthlem1	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 )
9		dvf	⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ
10	4	feq2d	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ ↔ ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
11	9 10	mpbii	⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
12	11	ffnd	⊢ ( 𝜑 → ( ℝ D 𝐹 ) Fn ( 𝐴 (,) 𝐵 ) )
13		iccssioo2	⊢ ( ( 𝑀 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑁 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑀 [,] 𝑁 ) ⊆ ( 𝐴 (,) 𝐵 ) )
14	1 2 13	syl2anc	⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ( 𝐴 (,) 𝐵 ) )
15	14	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
16		fnfvelrn	⊢ ( ( ( ℝ D 𝐹 ) Fn ( 𝐴 (,) 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ran ( ℝ D 𝐹 ) )
17	12 15 16	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ran ( ℝ D 𝐹 ) )
18		eleq1	⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ran ( ℝ D 𝐹 ) ↔ 𝐶 ∈ ran ( ℝ D 𝐹 ) ) )
19	17 18	syl5ibcom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 → 𝐶 ∈ ran ( ℝ D 𝐹 ) ) )
20	19	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 → 𝐶 ∈ ran ( ℝ D 𝐹 ) ) )
21	8 20	mpd	⊢ ( 𝜑 → 𝐶 ∈ ran ( ℝ D 𝐹 ) )