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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )