ivthle2

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

	Ref	Expression
Hypotheses	ivth.1	$⊢ φ \to A \in ℝ$
	ivth.2	$⊢ φ \to B \in ℝ$
	ivth.3	$⊢ φ \to U \in ℝ$
	ivth.4	$⊢ φ \to A < B$
	ivth.5	$⊢ φ \to [A, B] \subseteq D$
	ivth.7	$⊢ φ \to F : D \underset{cn}{⟶} ℂ$
	ivth.8	$⊢ (φ \land x \in [A, B]) \to F (x) \in ℝ$
	ivthle2.9	$⊢ φ \to (F (B) \leq U \land U \leq F (A))$
Assertion	ivthle2	$⊢ φ \to \exists c \in [A, B] F (c) = U$

Proof

Step	Hyp	Ref	Expression
1		ivth.1	$⊢ φ \to A \in ℝ$
2		ivth.2	$⊢ φ \to B \in ℝ$
3		ivth.3	$⊢ φ \to U \in ℝ$
4		ivth.4	$⊢ φ \to A < B$
5		ivth.5	$⊢ φ \to [A, B] \subseteq D$
6		ivth.7	$⊢ φ \to F : D \underset{cn}{⟶} ℂ$
7		ivth.8	$⊢ (φ \land x \in [A, B]) \to F (x) \in ℝ$
8		ivthle2.9	$⊢ φ \to (F (B) \leq U \land U \leq F (A))$
9		ioossicc	$⊢ (A, B) \subseteq [A, B]$
10	1	adantr	$⊢ (φ \land (F (B) < U \land U < F (A))) \to A \in ℝ$
11	2	adantr	$⊢ (φ \land (F (B) < U \land U < F (A))) \to B \in ℝ$
12	3	adantr	$⊢ (φ \land (F (B) < U \land U < F (A))) \to U \in ℝ$
13	4	adantr	$⊢ (φ \land (F (B) < U \land U < F (A))) \to A < B$
14	5	adantr	$⊢ (φ \land (F (B) < U \land U < F (A))) \to [A, B] \subseteq D$
15	6	adantr	$⊢ (φ \land (F (B) < U \land U < F (A))) \to F : D \underset{cn}{⟶} ℂ$
16	7	adantlr	$⊢ ((φ \land (F (B) < U \land U < F (A))) \land x \in [A, B]) \to F (x) \in ℝ$
17		simpr	$⊢ (φ \land (F (B) < U \land U < F (A))) \to (F (B) < U \land U < F (A))$
18	10 11 12 13 14 15 16 17	ivth2	$⊢ (φ \land (F (B) < U \land U < F (A))) \to \exists c \in (A, B) F (c) = U$
19		ssrexv	$⊢ (A, B) \subseteq [A, B] \to (\exists c \in (A, B) F (c) = U \to \exists c \in [A, B] F (c) = U)$
20	9 18 19	mpsyl	$⊢ (φ \land (F (B) < U \land U < F (A))) \to \exists c \in [A, B] F (c) = U$
21	20	anassrs	$⊢ ((φ \land F (B) < U) \land U < F (A)) \to \exists c \in [A, B] F (c) = U$
22	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
23	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
24	1 2 4	ltled	$⊢ φ \to A \leq B$
25		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
26	22 23 24 25	syl3anc	$⊢ φ \to A \in [A, B]$
27		eqcom	$⊢ F (c) = U \leftrightarrow U = F (c)$
28		fveq2	$⊢ c = A \to F (c) = F (A)$
29	28	eqeq2d	$⊢ c = A \to (U = F (c) \leftrightarrow U = F (A))$
30	27 29	bitrid	$⊢ c = A \to (F (c) = U \leftrightarrow U = F (A))$
31	30	rspcev	$⊢ (A \in [A, B] \land U = F (A)) \to \exists c \in [A, B] F (c) = U$
32	26 31	sylan	$⊢ (φ \land U = F (A)) \to \exists c \in [A, B] F (c) = U$
33	32	adantlr	$⊢ ((φ \land F (B) < U) \land U = F (A)) \to \exists c \in [A, B] F (c) = U$
34	8	simprd	$⊢ φ \to U \leq F (A)$
35		fveq2	$⊢ x = A \to F (x) = F (A)$
36	35	eleq1d	$⊢ x = A \to (F (x) \in ℝ \leftrightarrow F (A) \in ℝ)$
37	7	ralrimiva	$⊢ φ \to \forall x \in [A, B] F (x) \in ℝ$
38	36 37 26	rspcdva	$⊢ φ \to F (A) \in ℝ$
39	3 38	leloed	$⊢ φ \to (U \leq F (A) \leftrightarrow (U < F (A) \lor U = F (A)))$
40	34 39	mpbid	$⊢ φ \to (U < F (A) \lor U = F (A))$
41	40	adantr	$⊢ (φ \land F (B) < U) \to (U < F (A) \lor U = F (A))$
42	21 33 41	mpjaodan	$⊢ (φ \land F (B) < U) \to \exists c \in [A, B] F (c) = U$
43		ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$
44	22 23 24 43	syl3anc	$⊢ φ \to B \in [A, B]$
45		fveqeq2	$⊢ c = B \to (F (c) = U \leftrightarrow F (B) = U)$
46	45	rspcev	$⊢ (B \in [A, B] \land F (B) = U) \to \exists c \in [A, B] F (c) = U$
47	44 46	sylan	$⊢ (φ \land F (B) = U) \to \exists c \in [A, B] F (c) = U$
48	8	simpld	$⊢ φ \to F (B) \leq U$
49		fveq2	$⊢ x = B \to F (x) = F (B)$
50	49	eleq1d	$⊢ x = B \to (F (x) \in ℝ \leftrightarrow F (B) \in ℝ)$
51	50 37 44	rspcdva	$⊢ φ \to F (B) \in ℝ$
52	51 3	leloed	$⊢ φ \to (F (B) \leq U \leftrightarrow (F (B) < U \lor F (B) = U))$
53	48 52	mpbid	$⊢ φ \to (F (B) < U \lor F (B) = U)$
54	42 47 53	mpjaodan	$⊢ φ \to \exists c \in [A, B] F (c) = U$

Metamath Proof Explorer

Theorem ivthle2

Proof