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 )