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

Metamath Proof Explorer

Theorem ivthle

Description: The intermediate value theorem with weak inequality, increasing case. (Contributed by Mario Carneiro, 12-Aug-2014)

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

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 ivthle.9 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ≤ 𝑈 ∧ 𝑈 ≤ ( 𝐹 ‘ 𝐵 ) ) )
9 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
10 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) ) → 𝐴 ∈ ℝ )
11 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) ) → 𝐵 ∈ ℝ )
12 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) ) → 𝑈 ∈ ℝ )
13 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) ) → 𝐴 < 𝐵 )
14 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 )
15 6 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) ) → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
16 7 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
17 simpr ⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) ) → ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) )
18 10 11 12 13 14 15 16 17 ivth ⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) ) → ∃ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )
19 ssrexv ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) → ( ∃ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 → ∃ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 ) )
20 9 18 19 mpsyl ⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) ) → ∃ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )
21 20 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) < 𝑈 ) ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) → ∃ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )
22 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
23 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
24 1 2 4 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
25 ubicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
26 22 23 24 25 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
27 eqcom ⊢ ( ( 𝐹 ‘ 𝑐 ) = 𝑈 ↔ 𝑈 = ( 𝐹 ‘ 𝑐 ) )
28 fveq2 ⊢ ( 𝑐 = 𝐵 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝐵 ) )
29 28 eqeq2d ⊢ ( 𝑐 = 𝐵 → ( 𝑈 = ( 𝐹 ‘ 𝑐 ) ↔ 𝑈 = ( 𝐹 ‘ 𝐵 ) ) )
30 27 29 bitrid ⊢ ( 𝑐 = 𝐵 → ( ( 𝐹 ‘ 𝑐 ) = 𝑈 ↔ 𝑈 = ( 𝐹 ‘ 𝐵 ) ) )
31 30 rspcev ⊢ ( ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑈 = ( 𝐹 ‘ 𝐵 ) ) → ∃ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )
32 26 31 sylan ⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝐹 ‘ 𝐵 ) ) → ∃ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )
33 32 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) < 𝑈 ) ∧ 𝑈 = ( 𝐹 ‘ 𝐵 ) ) → ∃ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )
34 8 simprd ⊢ ( 𝜑 → 𝑈 ≤ ( 𝐹 ‘ 𝐵 ) )
35 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
36 35 eleq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝐵 ) ∈ ℝ ) )
37 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
38 36 37 26 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
39 3 38 leloed ⊢ ( 𝜑 → ( 𝑈 ≤ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝑈 < ( 𝐹 ‘ 𝐵 ) ∨ 𝑈 = ( 𝐹 ‘ 𝐵 ) ) ) )
40 34 39 mpbid ⊢ ( 𝜑 → ( 𝑈 < ( 𝐹 ‘ 𝐵 ) ∨ 𝑈 = ( 𝐹 ‘ 𝐵 ) ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) < 𝑈 ) → ( 𝑈 < ( 𝐹 ‘ 𝐵 ) ∨ 𝑈 = ( 𝐹 ‘ 𝐵 ) ) )
42 21 33 41 mpjaodan ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) < 𝑈 ) → ∃ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )
43 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
44 22 23 24 43 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
45 fveqeq2 ⊢ ( 𝑐 = 𝐴 → ( ( 𝐹 ‘ 𝑐 ) = 𝑈 ↔ ( 𝐹 ‘ 𝐴 ) = 𝑈 ) )
46 45 rspcev ⊢ ( ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐹 ‘ 𝐴 ) = 𝑈 ) → ∃ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )
47 44 46 sylan ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) = 𝑈 ) → ∃ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )
48 8 simpld ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ≤ 𝑈 )
49 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
50 49 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) )
51 50 37 44 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
52 51 3 leloed ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ≤ 𝑈 ↔ ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∨ ( 𝐹 ‘ 𝐴 ) = 𝑈 ) ) )
53 48 52 mpbid ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∨ ( 𝐹 ‘ 𝐴 ) = 𝑈 ) )
54 42 47 53 mpjaodan ⊢ ( 𝜑 → ∃ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )