Metamath Proof Explorer

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 𝐹 ) )