This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rollelem

Description: Lemma for rolle . (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses rolle.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
rolle.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
rolle.lt ⊢ ( 𝜑 → 𝐴 < 𝐵 )
rolle.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
rolle.d ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
rolle.r ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
rolle.u ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐴 [,] 𝐵 ) )
rolle.n ⊢ ( 𝜑 → ¬ 𝑈 ∈ { 𝐴 , 𝐵 } )
Assertion rollelem ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 )

Proof

Step Hyp Ref Expression
1 rolle.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 rolle.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 rolle.lt ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 rolle.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
5 rolle.d ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
6 rolle.r ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
7 rolle.u ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐴 [,] 𝐵 ) )
8 rolle.n ⊢ ( 𝜑 → ¬ 𝑈 ∈ { 𝐴 , 𝐵 } )
9 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
10 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
11 1 2 3 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
12 prunioo ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
13 9 10 11 12 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
14 7 13 eleqtrrd ⊢ ( 𝜑 → 𝑈 ∈ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) )
15 elun ⊢ ( 𝑈 ∈ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) ↔ ( 𝑈 ∈ ( 𝐴 (,) 𝐵 ) ∨ 𝑈 ∈ { 𝐴 , 𝐵 } ) )
16 14 15 sylib ⊢ ( 𝜑 → ( 𝑈 ∈ ( 𝐴 (,) 𝐵 ) ∨ 𝑈 ∈ { 𝐴 , 𝐵 } ) )
17 16 ord ⊢ ( 𝜑 → ( ¬ 𝑈 ∈ ( 𝐴 (,) 𝐵 ) → 𝑈 ∈ { 𝐴 , 𝐵 } ) )
18 8 17 mt3d ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐴 (,) 𝐵 ) )
19 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
20 4 19 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
21 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
22 1 2 21 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
23 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
24 23 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
25 18 5 eleqtrrd ⊢ ( 𝜑 → 𝑈 ∈ dom ( ℝ D 𝐹 ) )
26 ssralv ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) ) )
27 24 6 26 sylc ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
28 20 22 18 24 25 27 dvferm ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) = 0 )
29 fveqeq2 ⊢ ( 𝑥 = 𝑈 → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ↔ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) = 0 ) )
30 29 rspcev ⊢ ( ( 𝑈 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) = 0 ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 )
31 18 28 30 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 )