ivthlem2

Description: Lemma for ivth . Show that the supremum of S cannot be less than U . If it was, continuity of F implies that there are points just above the supremum that are also less than U , a contradiction. (Contributed 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	ivthlem2	$⊢ φ \to \neg 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	6	adantr	$⊢ (φ \land F (C) < U) \to F : D \underset{cn}{⟶} ℂ$
12	9	ssrab3	$⊢ S \subseteq [A, B]$
13		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
14	1 2 13	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
15	12 14	sstrid	$⊢ φ \to S \subseteq ℝ$
16	1 2 3 4 5 6 7 8 9	ivthlem1	$⊢ φ \to (A \in S \land \forall z \in S z \leq B)$
17	16	simpld	$⊢ φ \to A \in S$
18	17	ne0d	$⊢ φ \to S \neq \emptyset$
19	16	simprd	$⊢ φ \to \forall z \in S z \leq B$
20		brralrspcev	$⊢ (B \in ℝ \land \forall z \in S z \leq B) \to \exists x \in ℝ \forall z \in S z \leq x$
21	2 19 20	syl2anc	$⊢ φ \to \exists x \in ℝ \forall z \in S z \leq x$
22	15 18 21	suprcld	$⊢ φ \to sup (S ℝ <) \in ℝ$
23	10 22	eqeltrid	$⊢ φ \to C \in ℝ$
24	15 18 21 17	suprubd	$⊢ φ \to A \leq sup (S ℝ <)$
25	24 10	breqtrrdi	$⊢ φ \to A \leq C$
26	15 18 21	3jca	$⊢ φ \to (S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall z \in S z \leq x)$
27		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)$
28	26 2 27	syl2anc	$⊢ φ \to (sup (S ℝ <) \leq B \leftrightarrow \forall z \in S z \leq B)$
29	19 28	mpbird	$⊢ φ \to sup (S ℝ <) \leq B$
30	10 29	eqbrtrid	$⊢ φ \to C \leq B$
31		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (C \in [A, B] \leftrightarrow (C \in ℝ \land A \leq C \land C \leq B))$
32	1 2 31	syl2anc	$⊢ φ \to (C \in [A, B] \leftrightarrow (C \in ℝ \land A \leq C \land C \leq B))$
33	23 25 30 32	mpbir3and	$⊢ φ \to C \in [A, B]$
34	5 33	sseldd	$⊢ φ \to C \in D$
35	34	adantr	$⊢ (φ \land F (C) < U) \to C \in D$
36		fveq2	$⊢ x = C \to F (x) = F (C)$
37	36	eleq1d	$⊢ x = C \to (F (x) \in ℝ \leftrightarrow F (C) \in ℝ)$
38	7	ralrimiva	$⊢ φ \to \forall x \in [A, B] F (x) \in ℝ$
39	37 38 33	rspcdva	$⊢ φ \to F (C) \in ℝ$
40		difrp	$⊢ (F (C) \in ℝ \land U \in ℝ) \to (F (C) < U \leftrightarrow U - F (C) \in ℝ^{+})$
41	39 3 40	syl2anc	$⊢ φ \to (F (C) < U \leftrightarrow U - F (C) \in ℝ^{+})$
42	41	biimpa	$⊢ (φ \land F (C) < U) \to U - F (C) \in ℝ^{+}$
43		cncfi	$⊢ (F : D \underset{cn}{⟶} ℂ \land C \in D \land U - F (C) \in ℝ^{+}) \to \exists z \in ℝ^{+} \forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C))$
44	11 35 42 43	syl3anc	$⊢ (φ \land F (C) < U) \to \exists z \in ℝ^{+} \forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C))$
45		ssralv	$⊢ [A, B] \subseteq D \to (\forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)) \to \forall y \in [A, B] (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)))$
46	5 45	syl	$⊢ φ \to (\forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)) \to \forall y \in [A, B] (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)))$
47	46	ad2antrr	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to (\forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)) \to \forall y \in [A, B] (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)))$
48	2	ad2antrr	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to B \in ℝ$
49	23	ad2antrr	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to C \in ℝ$
50		rphalfcl	$⊢ z \in ℝ^{+} \to \frac{z}{2} \in ℝ^{+}$
51	50	adantl	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to \frac{z}{2} \in ℝ^{+}$
52	51	rpred	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to \frac{z}{2} \in ℝ$
53	49 52	readdcld	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to C + (\frac{z}{2}) \in ℝ$
54	48 53	ifcld	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \in ℝ$
55	1	ad2antrr	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to A \in ℝ$
56	25	ad2antrr	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to A \leq C$
57	8	simprd	$⊢ φ \to U < F (B)$
58		fveq2	$⊢ x = B \to F (x) = F (B)$
59	58	eleq1d	$⊢ x = B \to (F (x) \in ℝ \leftrightarrow F (B) \in ℝ)$
60	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
61	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
62	1 2 4	ltled	$⊢ φ \to A \leq B$
63		ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$
64	60 61 62 63	syl3anc	$⊢ φ \to B \in [A, B]$
65	59 38 64	rspcdva	$⊢ φ \to F (B) \in ℝ$
66		lttr	$⊢ (F (C) \in ℝ \land U \in ℝ \land F (B) \in ℝ) \to ((F (C) < U \land U < F (B)) \to F (C) < F (B))$
67	39 3 65 66	syl3anc	$⊢ φ \to ((F (C) < U \land U < F (B)) \to F (C) < F (B))$
68	57 67	mpan2d	$⊢ φ \to (F (C) < U \to F (C) < F (B))$
69	68	imp	$⊢ (φ \land F (C) < U) \to F (C) < F (B)$
70	69	adantr	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to F (C) < F (B)$
71	39	ltnrd	$⊢ φ \to \neg F (C) < F (C)$
72		fveq2	$⊢ B = C \to F (B) = F (C)$
73	72	breq2d	$⊢ B = C \to (F (C) < F (B) \leftrightarrow F (C) < F (C))$
74	73	notbid	$⊢ B = C \to (\neg F (C) < F (B) \leftrightarrow \neg F (C) < F (C))$
75	71 74	syl5ibrcom	$⊢ φ \to (B = C \to \neg F (C) < F (B))$
76	75	necon2ad	$⊢ φ \to (F (C) < F (B) \to B \neq C)$
77	76 30	jctild	$⊢ φ \to (F (C) < F (B) \to (C \leq B \land B \neq C))$
78	23 2	ltlend	$⊢ φ \to (C < B \leftrightarrow (C \leq B \land B \neq C))$
79	77 78	sylibrd	$⊢ φ \to (F (C) < F (B) \to C < B)$
80	79	ad2antrr	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to (F (C) < F (B) \to C < B)$
81	70 80	mpd	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to C < B$
82	49 51	ltaddrpd	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to C < C + (\frac{z}{2})$
83		breq2	$⊢ B = if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \to (C < B \leftrightarrow C < if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})))$
84		breq2	$⊢ C + (\frac{z}{2}) = if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \to (C < C + (\frac{z}{2}) \leftrightarrow C < if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})))$
85	83 84	ifboth	$⊢ (C < B \land C < C + (\frac{z}{2})) \to C < if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2}))$
86	81 82 85	syl2anc	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to C < if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2}))$
87	49 54 86	ltled	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to C \leq if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2}))$
88	55 49 54 56 87	letrd	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to A \leq if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2}))$
89		min1	$⊢ (B \in ℝ \land C + (\frac{z}{2}) \in ℝ) \to if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \leq B$
90	48 53 89	syl2anc	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \leq B$
91		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \in [A, B] \leftrightarrow (if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \in ℝ \land A \leq if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \land if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \leq B))$
92	1 2 91	syl2anc	$⊢ φ \to (if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \in [A, B] \leftrightarrow (if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \in ℝ \land A \leq if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \land if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \leq B))$
93	92	ad2antrr	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to (if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \in [A, B] \leftrightarrow (if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \in ℝ \land A \leq if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \land if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \leq B))$
94	54 88 90 93	mpbir3and	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \in [A, B]$
95	49 54 87	abssubge0d	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to \|if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) - C\| = if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) - C$
96		rpre	$⊢ z \in ℝ^{+} \to z \in ℝ$
97	96	adantl	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to z \in ℝ$
98	49 97	readdcld	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to C + z \in ℝ$
99		min2	$⊢ (B \in ℝ \land C + (\frac{z}{2}) \in ℝ) \to if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \leq C + (\frac{z}{2})$
100	48 53 99	syl2anc	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \leq C + (\frac{z}{2})$
101		rphalflt	$⊢ z \in ℝ^{+} \to \frac{z}{2} < z$
102	101	adantl	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to \frac{z}{2} < z$
103	52 97 49 102	ltadd2dd	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to C + (\frac{z}{2}) < C + z$
104	54 53 98 100 103	lelttrd	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) < C + z$
105	54 49 97	ltsubadd2d	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to (if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) - C < z \leftrightarrow if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) < C + z)$
106	104 105	mpbird	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) - C < z$
107	95 106	eqbrtrd	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to \|if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) - C\| < z$
108		fvoveq1	$⊢ y = if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \to \|y - C\| = \|if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) - C\|$
109	108	breq1d	$⊢ y = if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \to (\|y - C\| < z \leftrightarrow \|if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) - C\| < z)$
110		breq2	$⊢ y = if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \to (C < y \leftrightarrow C < if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})))$
111	109 110	anbi12d	$⊢ y = if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \to ((\|y - C\| < z \land C < y) \leftrightarrow (\|if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) - C\| < z \land C < if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2}))))$
112	111	rspcev	$⊢ (if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) \in [A, B] \land (\|if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})) - C\| < z \land C < if (B \leq C + (\frac{z}{2}), B, C + (\frac{z}{2})))) \to \exists y \in [A, B] (\|y - C\| < z \land C < y)$
113	94 107 86 112	syl12anc	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to \exists y \in [A, B] (\|y - C\| < z \land C < y)$
114		r19.29	$⊢ (\forall y \in [A, B] (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)) \land \exists y \in [A, B] (\|y - C\| < z \land C < y)) \to \exists y \in [A, B] ((\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)) \land (\|y - C\| < z \land C < y))$
115		pm3.45	$⊢ (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)) \to ((\|y - C\| < z \land C < y) \to (\|F (y) - F (C)\| < U - F (C) \land C < y))$
116	115	imp	$⊢ ((\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)) \land (\|y - C\| < z \land C < y)) \to (\|F (y) - F (C)\| < U - F (C) \land C < y)$
117		simprr	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to C < y$
118		fveq2	$⊢ x = y \to F (x) = F (y)$
119	118	eleq1d	$⊢ x = y \to (F (x) \in ℝ \leftrightarrow F (y) \in ℝ)$
120		simplll	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to φ$
121	120 38	syl	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to \forall x \in [A, B] F (x) \in ℝ$
122		simprl	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to y \in [A, B]$
123	119 121 122	rspcdva	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to F (y) \in ℝ$
124	120 39	syl	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to F (C) \in ℝ$
125	120 3	syl	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to U \in ℝ$
126	125 124	resubcld	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to U - F (C) \in ℝ$
127	123 124 126	absdifltd	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to (\|F (y) - F (C)\| < U - F (C) \leftrightarrow (F (C) - (U - F (C)) < F (y) \land F (y) < F (C) + U - F (C)))$
128		ltle	$⊢ (F (y) \in ℝ \land U \in ℝ) \to (F (y) < U \to F (y) \leq U)$
129	123 125 128	syl2anc	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to (F (y) < U \to F (y) \leq U)$
130	124	recnd	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to F (C) \in ℂ$
131	125	recnd	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to U \in ℂ$
132	130 131	pncan3d	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to F (C) + U - F (C) = U$
133	132	breq2d	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to (F (y) < F (C) + U - F (C) \leftrightarrow F (y) < U)$
134	118	breq1d	$⊢ x = y \to (F (x) \leq U \leftrightarrow F (y) \leq U)$
135	134 9	elrab2	$⊢ y \in S \leftrightarrow (y \in [A, B] \land F (y) \leq U)$
136	135	baib	$⊢ y \in [A, B] \to (y \in S \leftrightarrow F (y) \leq U)$
137	136	ad2antrl	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to (y \in S \leftrightarrow F (y) \leq U)$
138	129 133 137	3imtr4d	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to (F (y) < F (C) + U - F (C) \to y \in S)$
139		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 ℝ <)$
140	139 10	breqtrrdi	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall z \in S z \leq x) \land y \in S) \to y \leq C$
141	140	ex	$⊢ (S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall z \in S z \leq x) \to (y \in S \to y \leq C)$
142	120 26 141	3syl	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to (y \in S \to y \leq C)$
143	120 14	syl	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to [A, B] \subseteq ℝ$
144	143 122	sseldd	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to y \in ℝ$
145	120 23	syl	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to C \in ℝ$
146	144 145	lenltd	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to (y \leq C \leftrightarrow \neg C < y)$
147	142 146	sylibd	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to (y \in S \to \neg C < y)$
148	138 147	syld	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to (F (y) < F (C) + U - F (C) \to \neg C < y)$
149	148	adantld	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to ((F (C) - (U - F (C)) < F (y) \land F (y) < F (C) + U - F (C)) \to \neg C < y)$
150	127 149	sylbid	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to (\|F (y) - F (C)\| < U - F (C) \to \neg C < y)$
151	117 150	mt2d	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to \neg \|F (y) - F (C)\| < U - F (C)$
152	151	pm2.21d	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land (y \in [A, B] \land C < y)) \to (\|F (y) - F (C)\| < U - F (C) \to \neg F (C) < U)$
153	152	expr	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land y \in [A, B]) \to (C < y \to (\|F (y) - F (C)\| < U - F (C) \to \neg F (C) < U))$
154	153	impcomd	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land y \in [A, B]) \to ((\|F (y) - F (C)\| < U - F (C) \land C < y) \to \neg F (C) < U)$
155	116 154	syl5	$⊢ (((φ \land F (C) < U) \land z \in ℝ^{+}) \land y \in [A, B]) \to (((\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)) \land (\|y - C\| < z \land C < y)) \to \neg F (C) < U)$
156	155	rexlimdva	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to (\exists y \in [A, B] ((\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)) \land (\|y - C\| < z \land C < y)) \to \neg F (C) < U)$
157	114 156	syl5	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to ((\forall y \in [A, B] (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)) \land \exists y \in [A, B] (\|y - C\| < z \land C < y)) \to \neg F (C) < U)$
158	113 157	mpan2d	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to (\forall y \in [A, B] (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)) \to \neg F (C) < U)$
159	47 158	syld	$⊢ ((φ \land F (C) < U) \land z \in ℝ^{+}) \to (\forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)) \to \neg F (C) < U)$
160	159	rexlimdva	$⊢ (φ \land F (C) < U) \to (\exists z \in ℝ^{+} \forall y \in D (\|y - C\| < z \to \|F (y) - F (C)\| < U - F (C)) \to \neg F (C) < U)$
161	44 160	mpd	$⊢ (φ \land F (C) < U) \to \neg F (C) < U$
162	161	pm2.01da	$⊢ φ \to \neg F (C) < U$

Metamath Proof Explorer

Theorem ivthlem2

Proof