ivthlem3

Description: Lemma for ivth , the intermediate value theorem. Show that ( FC ) cannot be greater than U , and so establish the existence of a root of the function. (Contributed by Mario Carneiro, 30-Apr-2014) (Revised by Mario Carneiro, 17-Jun-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 ℝ$
	ivth.9	$⊢ φ \to (F (A) < U \land U < F (B))$
	ivth.10	$⊢ S = \{x \in [A, B] \| F (x) \leq U\}$
	ivth.11	$⊢ C = sup (S ℝ <)$
Assertion	ivthlem3	$⊢ φ \to (C \in (A, B) \land 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		ivth.9	$⊢ φ \to (F (A) < U \land U < F (B))$
9		ivth.10	$⊢ S = \{x \in [A, B] \| F (x) \leq U\}$
10		ivth.11	$⊢ C = sup (S ℝ <)$
11	9	ssrab3	$⊢ S \subseteq [A, B]$
12		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
13	1 2 12	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
14	11 13	sstrid	$⊢ φ \to S \subseteq ℝ$
15	1 2 3 4 5 6 7 8 9	ivthlem1	$⊢ φ \to (A \in S \land \forall z \in S z \leq B)$
16	15	simpld	$⊢ φ \to A \in S$
17	16	ne0d	$⊢ φ \to S \neq \emptyset$
18	15	simprd	$⊢ φ \to \forall z \in S z \leq B$
19		brralrspcev	$⊢ (B \in ℝ \land \forall z \in S z \leq B) \to \exists x \in ℝ \forall z \in S z \leq x$
20	2 18 19	syl2anc	$⊢ φ \to \exists x \in ℝ \forall z \in S z \leq x$
21	14 17 20	suprcld	$⊢ φ \to sup (S ℝ <) \in ℝ$
22	10 21	eqeltrid	$⊢ φ \to C \in ℝ$
23	8	simpld	$⊢ φ \to F (A) < U$
24	1 2 3 4 5 6 7 8 9 10	ivthlem2	$⊢ φ \to \neg F (C) < U$
25	6	adantr	$⊢ (φ \land U < F (C)) \to F : D \underset{cn}{⟶} ℂ$
26	14 17 20 16	suprubd	$⊢ φ \to A \leq sup (S ℝ <)$
27	26 10	breqtrrdi	$⊢ φ \to A \leq C$
28	14 17 20	3jca	$⊢ φ \to (S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall z \in S z \leq x)$
29		suprleub	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall z \in S z \leq x) \land B \in ℝ) \to (sup (S ℝ <) \leq B \leftrightarrow \forall z \in S z \leq B)$
30	28 2 29	syl2anc	$⊢ φ \to (sup (S ℝ <) \leq B \leftrightarrow \forall z \in S z \leq B)$
31	18 30	mpbird	$⊢ φ \to sup (S ℝ <) \leq B$
32	10 31	eqbrtrid	$⊢ φ \to C \leq B$
33		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (C \in [A, B] \leftrightarrow (C \in ℝ \land A \leq C \land C \leq B))$
34	1 2 33	syl2anc	$⊢ φ \to (C \in [A, B] \leftrightarrow (C \in ℝ \land A \leq C \land C \leq B))$
35	22 27 32 34	mpbir3and	$⊢ φ \to C \in [A, B]$
36	5 35	sseldd	$⊢ φ \to C \in D$
37	36	adantr	$⊢ (φ \land U < F (C)) \to C \in D$
38		fveq2	$⊢ x = C \to F (x) = F (C)$
39	38	eleq1d	$⊢ x = C \to (F (x) \in ℝ \leftrightarrow F (C) \in ℝ)$
40	7	ralrimiva	$⊢ φ \to \forall x \in [A, B] F (x) \in ℝ$
41	39 40 35	rspcdva	$⊢ φ \to F (C) \in ℝ$
42		difrp	$⊢ (U \in ℝ \land F (C) \in ℝ) \to (U < F (C) \leftrightarrow F (C) - U \in ℝ^{+})$
43	3 41 42	syl2anc	$⊢ φ \to (U < F (C) \leftrightarrow F (C) - U \in ℝ^{+})$
44	43	biimpa	$⊢ (φ \land U < F (C)) \to F (C) - U \in ℝ^{+}$
45		cncfi	$⊢ (F : D \underset{cn}{⟶} ℂ \land C \in D \land F (C) - U \in ℝ^{+}) \to \exists z \in ℝ^{+} \forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U)$
46	25 37 44 45	syl3anc	$⊢ (φ \land U < F (C)) \to \exists z \in ℝ^{+} \forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U)$
47		ssralv	$⊢ [A, B] \subseteq D \to (\forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U) \to \forall y \in [A, B] (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U))$
48	5 47	syl	$⊢ φ \to (\forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U) \to \forall y \in [A, B] (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U))$
49	48	ad2antrr	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to (\forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U) \to \forall y \in [A, B] (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U))$
50	22	ad2antrr	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to C \in ℝ$
51		ltsubrp	$⊢ (C \in ℝ \land z \in ℝ^{+}) \to C - z < C$
52	50 51	sylancom	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to C - z < C$
53	52 10	breqtrdi	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to C - z < sup (S ℝ <)$
54	28	ad2antrr	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to (S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall z \in S z \leq x)$
55		rpre	$⊢ z \in ℝ^{+} \to z \in ℝ$
56	55	adantl	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to z \in ℝ$
57	50 56	resubcld	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to C - z \in ℝ$
58		suprlub	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall z \in S z \leq x) \land C - z \in ℝ) \to (C - z < sup (S ℝ <) \leftrightarrow \exists y \in S C - z < y)$
59	54 57 58	syl2anc	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to (C - z < sup (S ℝ <) \leftrightarrow \exists y \in S C - z < y)$
60	53 59	mpbid	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to \exists y \in S C - z < y$
61	11	sseli	$⊢ y \in S \to y \in [A, B]$
62	61	ad2antrl	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to y \in [A, B]$
63		simplll	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to φ$
64	63 13	syl	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to [A, B] \subseteq ℝ$
65	64 62	sseldd	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to y \in ℝ$
66	63 22	syl	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to C \in ℝ$
67	63 28	syl	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to (S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall z \in S z \leq x)$
68		simprl	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to y \in S$
69		suprub	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall z \in S z \leq x) \land y \in S) \to y \leq sup (S ℝ <)$
70	67 68 69	syl2anc	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to y \leq sup (S ℝ <)$
71	70 10	breqtrrdi	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to y \leq C$
72	65 66 71	abssuble0d	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to \|y - C\| = C - y$
73	56	adantr	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to z \in ℝ$
74		simprr	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to C - z < y$
75	66 73 65 74	ltsub23d	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to C - y < z$
76	72 75	eqbrtrd	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to \|y - C\| < z$
77	62 76 68	jca32	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land (y \in S \land C - z < y)) \to (y \in [A, B] \land (\|y - C\| < z \land y \in S))$
78	77	ex	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to ((y \in S \land C - z < y) \to (y \in [A, B] \land (\|y - C\| < z \land y \in S)))$
79	78	reximdv2	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to (\exists y \in S C - z < y \to \exists y \in [A, B] (\|y - C\| < z \land y \in S))$
80	60 79	mpd	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to \exists y \in [A, B] (\|y - C\| < z \land y \in S)$
81		r19.29	$⊢ (\forall y \in [A, B] (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U) \land \exists y \in [A, B] (\|y - C\| < z \land y \in S)) \to \exists y \in [A, B] ((\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U) \land (\|y - C\| < z \land y \in S))$
82		pm3.45	$⊢ (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U) \to ((\|y - C\| < z \land y \in S) \to (\|F (y) - F (C)\| < F (C) - U \land y \in S))$
83	82	imp	$⊢ ((\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U) \land (\|y - C\| < z \land y \in S)) \to (\|F (y) - F (C)\| < F (C) - U \land y \in S)$
84		fveq2	$⊢ x = y \to F (x) = F (y)$
85	84	eleq1d	$⊢ x = y \to (F (x) \in ℝ \leftrightarrow F (y) \in ℝ)$
86	40	ad2antrr	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to \forall x \in [A, B] F (x) \in ℝ$
87	61	ad2antll	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to y \in [A, B]$
88	85 86 87	rspcdva	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to F (y) \in ℝ$
89	41	ad2antrr	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to F (C) \in ℝ$
90	3	ad2antrr	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to U \in ℝ$
91	89 90	resubcld	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to F (C) - U \in ℝ$
92	88 89 91	absdifltd	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to (\|F (y) - F (C)\| < F (C) - U \leftrightarrow (F (C) - (F (C) - U) < F (y) \land F (y) < F (C) + F (C) - U))$
93	89	recnd	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to F (C) \in ℂ$
94	90	recnd	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to U \in ℂ$
95	93 94	nncand	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to F (C) - (F (C) - U) = U$
96	95	breq1d	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to (F (C) - (F (C) - U) < F (y) \leftrightarrow U < F (y))$
97	84	breq1d	$⊢ x = y \to (F (x) \leq U \leftrightarrow F (y) \leq U)$
98	97 9	elrab2	$⊢ y \in S \leftrightarrow (y \in [A, B] \land F (y) \leq U)$
99	98	simprbi	$⊢ y \in S \to F (y) \leq U$
100	99	ad2antll	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to F (y) \leq U$
101	88 90 100	lensymd	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to \neg U < F (y)$
102	101	pm2.21d	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to (U < F (y) \to \neg U < F (C))$
103	96 102	sylbid	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to (F (C) - (F (C) - U) < F (y) \to \neg U < F (C))$
104	103	adantrd	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to ((F (C) - (F (C) - U) < F (y) \land F (y) < F (C) + F (C) - U) \to \neg U < F (C))$
105	92 104	sylbid	$⊢ ((φ \land U < F (C)) \land (z \in ℝ^{+} \land y \in S)) \to (\|F (y) - F (C)\| < F (C) - U \to \neg U < F (C))$
106	105	expr	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to (y \in S \to (\|F (y) - F (C)\| < F (C) - U \to \neg U < F (C)))$
107	106	impcomd	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to ((\|F (y) - F (C)\| < F (C) - U \land y \in S) \to \neg U < F (C))$
108	107	adantr	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land y \in [A, B]) \to ((\|F (y) - F (C)\| < F (C) - U \land y \in S) \to \neg U < F (C))$
109	83 108	syl5	$⊢ (((φ \land U < F (C)) \land z \in ℝ^{+}) \land y \in [A, B]) \to (((\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U) \land (\|y - C\| < z \land y \in S)) \to \neg U < F (C))$
110	109	rexlimdva	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to (\exists y \in [A, B] ((\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U) \land (\|y - C\| < z \land y \in S)) \to \neg U < F (C))$
111	81 110	syl5	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to ((\forall y \in [A, B] (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U) \land \exists y \in [A, B] (\|y - C\| < z \land y \in S)) \to \neg U < F (C))$
112	80 111	mpan2d	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to (\forall y \in [A, B] (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U) \to \neg U < F (C))$
113	49 112	syld	$⊢ ((φ \land U < F (C)) \land z \in ℝ^{+}) \to (\forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U) \to \neg U < F (C))$
114	113	rexlimdva	$⊢ (φ \land U < F (C)) \to (\exists z \in ℝ^{+} \forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < F (C) - U) \to \neg U < F (C))$
115	46 114	mpd	$⊢ (φ \land U < F (C)) \to \neg U < F (C)$
116	115	pm2.01da	$⊢ φ \to \neg U < F (C)$
117	41 3	lttri3d	$⊢ φ \to (F (C) = U \leftrightarrow (\neg F (C) < U \land \neg U < F (C)))$
118	24 116 117	mpbir2and	$⊢ φ \to F (C) = U$
119	23 118	breqtrrd	$⊢ φ \to F (A) < F (C)$
120	41	ltnrd	$⊢ φ \to \neg F (C) < F (C)$
121		fveq2	$⊢ C = A \to F (C) = F (A)$
122	121	breq1d	$⊢ C = A \to (F (C) < F (C) \leftrightarrow F (A) < F (C))$
123	122	notbid	$⊢ C = A \to (\neg F (C) < F (C) \leftrightarrow \neg F (A) < F (C))$
124	120 123	syl5ibcom	$⊢ φ \to (C = A \to \neg F (A) < F (C))$
125	124	necon2ad	$⊢ φ \to (F (A) < F (C) \to C \neq A)$
126	125 27	jctild	$⊢ φ \to (F (A) < F (C) \to (A \leq C \land C \neq A))$
127	1 22	ltlend	$⊢ φ \to (A < C \leftrightarrow (A \leq C \land C \neq A))$
128	126 127	sylibrd	$⊢ φ \to (F (A) < F (C) \to A < C)$
129	119 128	mpd	$⊢ φ \to A < C$
130	8	simprd	$⊢ φ \to U < F (B)$
131	118 130	eqbrtrd	$⊢ φ \to F (C) < F (B)$
132		fveq2	$⊢ B = C \to F (B) = F (C)$
133	132	breq2d	$⊢ B = C \to (F (C) < F (B) \leftrightarrow F (C) < F (C))$
134	133	notbid	$⊢ B = C \to (\neg F (C) < F (B) \leftrightarrow \neg F (C) < F (C))$
135	120 134	syl5ibrcom	$⊢ φ \to (B = C \to \neg F (C) < F (B))$
136	135	necon2ad	$⊢ φ \to (F (C) < F (B) \to B \neq C)$
137	136 32	jctild	$⊢ φ \to (F (C) < F (B) \to (C \leq B \land B \neq C))$
138	22 2	ltlend	$⊢ φ \to (C < B \leftrightarrow (C \leq B \land B \neq C))$
139	137 138	sylibrd	$⊢ φ \to (F (C) < F (B) \to C < B)$
140	131 139	mpd	$⊢ φ \to C < B$
141	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
142	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
143		elioo2	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (C \in (A, B) \leftrightarrow (C \in ℝ \land A < C \land C < B))$
144	141 142 143	syl2anc	$⊢ φ \to (C \in (A, B) \leftrightarrow (C \in ℝ \land A < C \land C < B))$
145	22 129 140 144	mpbir3and	$⊢ φ \to C \in (A, B)$
146	145 118	jca	$⊢ φ \to (C \in (A, B) \land F (C) = U)$

Metamath Proof Explorer

Theorem ivthlem3

Proof