ivth2

Description: The intermediate value theorem, decreasing case. (Contributed by Paul Chapman, 22-Jan-2008) (Revised by Mario Carneiro, 30-Apr-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 ℝ$
	ivth2.9	$⊢ φ \to (F (B) < U \land U < F (A))$
Assertion	ivth2	$⊢ φ \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		ivth2.9	$⊢ φ \to (F (B) < U \land U < F (A))$
9	3	renegcld	$⊢ φ \to - U \in ℝ$
10		eqid	$⊢ (y \in D ⟼ - F (y)) = (y \in D ⟼ - F (y))$
11	10	negfcncf	$⊢ F : D \underset{cn}{⟶} ℂ \to (y \in D ⟼ - F (y)) : D \underset{cn}{⟶} ℂ$
12	6 11	syl	$⊢ φ \to (y \in D ⟼ - F (y)) : D \underset{cn}{⟶} ℂ$
13	5	sselda	$⊢ (φ \land x \in [A, B]) \to x \in D$
14		fveq2	$⊢ y = x \to F (y) = F (x)$
15	14	negeqd	$⊢ y = x \to - F (y) = - F (x)$
16		negex	$⊢ - F (x) \in V$
17	15 10 16	fvmpt	$⊢ x \in D \to (y \in D ⟼ - F (y)) (x) = - F (x)$
18	13 17	syl	$⊢ (φ \land x \in [A, B]) \to (y \in D ⟼ - F (y)) (x) = - F (x)$
19	7	renegcld	$⊢ (φ \land x \in [A, B]) \to - F (x) \in ℝ$
20	18 19	eqeltrd	$⊢ (φ \land x \in [A, B]) \to (y \in D ⟼ - F (y)) (x) \in ℝ$
21	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
22	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
23	1 2 4	ltled	$⊢ φ \to A \leq B$
24		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
25	21 22 23 24	syl3anc	$⊢ φ \to A \in [A, B]$
26	5 25	sseldd	$⊢ φ \to A \in D$
27		fveq2	$⊢ y = A \to F (y) = F (A)$
28	27	negeqd	$⊢ y = A \to - F (y) = - F (A)$
29		negex	$⊢ - F (A) \in V$
30	28 10 29	fvmpt	$⊢ A \in D \to (y \in D ⟼ - F (y)) (A) = - F (A)$
31	26 30	syl	$⊢ φ \to (y \in D ⟼ - F (y)) (A) = - F (A)$
32	8	simprd	$⊢ φ \to U < F (A)$
33		fveq2	$⊢ x = A \to F (x) = F (A)$
34	33	eleq1d	$⊢ x = A \to (F (x) \in ℝ \leftrightarrow F (A) \in ℝ)$
35	7	ralrimiva	$⊢ φ \to \forall x \in [A, B] F (x) \in ℝ$
36	34 35 25	rspcdva	$⊢ φ \to F (A) \in ℝ$
37	3 36	ltnegd	$⊢ φ \to (U < F (A) \leftrightarrow - F (A) < - U)$
38	32 37	mpbid	$⊢ φ \to - F (A) < - U$
39	31 38	eqbrtrd	$⊢ φ \to (y \in D ⟼ - F (y)) (A) < - U$
40	8	simpld	$⊢ φ \to F (B) < U$
41		fveq2	$⊢ x = B \to F (x) = F (B)$
42	41	eleq1d	$⊢ x = B \to (F (x) \in ℝ \leftrightarrow F (B) \in ℝ)$
43		ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$
44	21 22 23 43	syl3anc	$⊢ φ \to B \in [A, B]$
45	42 35 44	rspcdva	$⊢ φ \to F (B) \in ℝ$
46	45 3	ltnegd	$⊢ φ \to (F (B) < U \leftrightarrow - U < - F (B))$
47	40 46	mpbid	$⊢ φ \to - U < - F (B)$
48	5 44	sseldd	$⊢ φ \to B \in D$
49		fveq2	$⊢ y = B \to F (y) = F (B)$
50	49	negeqd	$⊢ y = B \to - F (y) = - F (B)$
51		negex	$⊢ - F (B) \in V$
52	50 10 51	fvmpt	$⊢ B \in D \to (y \in D ⟼ - F (y)) (B) = - F (B)$
53	48 52	syl	$⊢ φ \to (y \in D ⟼ - F (y)) (B) = - F (B)$
54	47 53	breqtrrd	$⊢ φ \to - U < (y \in D ⟼ - F (y)) (B)$
55	39 54	jca	$⊢ φ \to ((y \in D ⟼ - F (y)) (A) < - U \land - U < (y \in D ⟼ - F (y)) (B))$
56	1 2 9 4 5 12 20 55	ivth	$⊢ φ \to \exists c \in (A, B) (y \in D ⟼ - F (y)) (c) = - U$
57		ioossicc	$⊢ (A, B) \subseteq [A, B]$
58	57 5	sstrid	$⊢ φ \to (A, B) \subseteq D$
59	58	sselda	$⊢ (φ \land c \in (A, B)) \to c \in D$
60		fveq2	$⊢ y = c \to F (y) = F (c)$
61	60	negeqd	$⊢ y = c \to - F (y) = - F (c)$
62		negex	$⊢ - F (c) \in V$
63	61 10 62	fvmpt	$⊢ c \in D \to (y \in D ⟼ - F (y)) (c) = - F (c)$
64	59 63	syl	$⊢ (φ \land c \in (A, B)) \to (y \in D ⟼ - F (y)) (c) = - F (c)$
65	64	eqeq1d	$⊢ (φ \land c \in (A, B)) \to ((y \in D ⟼ - F (y)) (c) = - U \leftrightarrow - F (c) = - U)$
66		cncff	$⊢ F : D \underset{cn}{⟶} ℂ \to F : D ⟶ ℂ$
67	6 66	syl	$⊢ φ \to F : D ⟶ ℂ$
68	67	ffvelrnda	$⊢ (φ \land c \in D) \to F (c) \in ℂ$
69	59 68	syldan	$⊢ (φ \land c \in (A, B)) \to F (c) \in ℂ$
70	3	recnd	$⊢ φ \to U \in ℂ$
71	70	adantr	$⊢ (φ \land c \in (A, B)) \to U \in ℂ$
72	69 71	neg11ad	$⊢ (φ \land c \in (A, B)) \to (- F (c) = - U \leftrightarrow F (c) = U)$
73	65 72	bitrd	$⊢ (φ \land c \in (A, B)) \to ((y \in D ⟼ - F (y)) (c) = - U \leftrightarrow F (c) = U)$
74	73	rexbidva	$⊢ φ \to (\exists c \in (A, B) (y \in D ⟼ - F (y)) (c) = - U \leftrightarrow \exists c \in (A, B) F (c) = U)$
75	56 74	mpbid	$⊢ φ \to \exists c \in (A, B) F (c) = U$

Metamath Proof Explorer

Theorem ivth2

Proof