Theorem ivth

Description: The intermediate value theorem, increasing case. This is Metamath 100 proof #79. (Contributed by Paul Chapman, 22-Jan-2008) (Proof shortened by Mario Carneiro, 30-Apr-2014)

	Ref	Expression
Hypotheses	ivth.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ivth.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ivth.3	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
	ivth.4	⊢ ( 𝜑 → 𝐴 < 𝐵 )
	ivth.5	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 )
	ivth.7	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
	ivth.8	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
	ivth.9	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) )
Assertion	ivth	⊢ ( 𝜑 → ∃ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		ivth.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		ivth.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		ivth.3	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
4		ivth.4	⊢ ( 𝜑 → 𝐴 < 𝐵 )
5		ivth.5	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 )
6		ivth.7	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
7		ivth.8	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
8		ivth.9	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) )
9		fveq2	⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
10	9	breq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑈 ) )
11	10	cbvrabv	⊢ { 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 } = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑈 }
12		eqid	⊢ sup ( { 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 } , ℝ , < ) = sup ( { 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 } , ℝ , < )
13	1 2 3 4 5 6 7 8 11 12	ivthlem3	⊢ ( 𝜑 → ( sup ( { 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 } , ℝ , < ) ∈ ( 𝐴 (,) 𝐵 ) ∧ ( 𝐹 ‘ sup ( { 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 } , ℝ , < ) ) = 𝑈 ) )
14		fveqeq2	⊢ ( 𝑐 = sup ( { 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 } , ℝ , < ) → ( ( 𝐹 ‘ 𝑐 ) = 𝑈 ↔ ( 𝐹 ‘ sup ( { 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 } , ℝ , < ) ) = 𝑈 ) )
15	14	rspcev	⊢ ( ( sup ( { 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 } , ℝ , < ) ∈ ( 𝐴 (,) 𝐵 ) ∧ ( 𝐹 ‘ sup ( { 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 } , ℝ , < ) ) = 𝑈 ) → ∃ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )
16	13 15	syl	⊢ ( 𝜑 → ∃ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )