ivthlem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ivthlem2		Structured version Visualization version GIF version

Theorem ivthlem2 24045

Description: Lemma for ivth 24047. Show that the supremum of 𝑆 cannot be less than 𝑈. If it was, continuity of 𝐹 implies that there are points just above the supremum that are also less than 𝑈, a contradiction. (Contributed by Mario Carneiro, 17-Jun-2014.)

**Hypotheses**
Ref	Expression
ivth.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ivth.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
ivth.3	⊢ (𝜑 → 𝑈 ∈ ℝ)
ivth.4	⊢ (𝜑 → 𝐴 < 𝐵)
ivth.5	⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
ivth.7	⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))
ivth.8	⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)
ivth.9	⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))
ivth.10	⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈}
ivth.11	⊢ 𝐶 = sup(𝑆, ℝ, < )

**Assertion**
Ref	Expression
ivthlem2	⊢ (𝜑 → ¬ (𝐹‘𝐶) < 𝑈)

Distinct variable groups: 𝑥,𝐵 𝑥,𝐷 𝑥,𝐹 𝜑,𝑥 𝑥,𝐴 𝑥,𝐶 𝑥,𝑆 𝑥,𝑈

Proof of Theorem ivthlem2 Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ivth.7	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))
2	1	adantr 483	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → 𝐹 ∈ (𝐷–cn→ℂ))
3		ivth.5	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
4		ivth.11	. . . . . . . 8 ⊢ 𝐶 = sup(𝑆, ℝ, < )
5		ivth.10	. . . . . . . . . . 11 ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈}
6	5	ssrab3 4055	. . . . . . . . . 10 ⊢ 𝑆 ⊆ (𝐴[,]𝐵)
7		ivth.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
8		ivth.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9		iccssre 12810	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
10	7, 8, 9	syl2anc 586	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
11	6, 10	sstrid 3976	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ⊆ ℝ)
12		ivth.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ ℝ)
13		ivth.4	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
14		ivth.8	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)
15		ivth.9	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))
16	7, 8, 12, 13, 3, 1, 14, 15, 5	ivthlem1 24044	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
17	16	simpld 497	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
18	17	ne0d 4299	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ≠ ∅)
19	16	simprd 498	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵)
20		brralrspcev 5117	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
21	8, 19, 20	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
22	11, 18, 21	suprcld 11596	. . . . . . . 8 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ ℝ)
23	4, 22	eqeltrid 2915	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℝ)
24	11, 18, 21, 17	suprubd 11595	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < ))
25	24, 4	breqtrrdi 5099	. . . . . . 7 ⊢ (𝜑 → 𝐴 ≤ 𝐶)
26	11, 18, 21	3jca 1123	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
27		suprleub 11599	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
28	26, 8, 27	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
29	19, 28	mpbird 259	. . . . . . . 8 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ≤ 𝐵)
30	4, 29	eqbrtrid 5092	. . . . . . 7 ⊢ (𝜑 → 𝐶 ≤ 𝐵)
31		elicc2 12793	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
32	7, 8, 31	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
33	23, 25, 30, 32	mpbir3and 1337	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))
34	3, 33	sseldd 3966	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝐷)
35	34	adantr 483	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → 𝐶 ∈ 𝐷)
36		fveq2 6663	. . . . . . . 8 ⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶))
37	36	eleq1d 2895	. . . . . . 7 ⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐶) ∈ ℝ))
38	14	ralrimiva 3180	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
39	37, 38, 33	rspcdva 3623	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℝ)
40		difrp 12419	. . . . . 6 ⊢ (((𝐹‘𝐶) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹‘𝐶) < 𝑈 ↔ (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺))
41	39, 12, 40	syl2anc 586	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝐶) < 𝑈 ↔ (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺))
42	41	biimpa 479	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺)
43		cncfi 23494	. . . 4 ⊢ ((𝐹 ∈ (𝐷–cn→ℂ) ∧ 𝐶 ∈ 𝐷 ∧ (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))))
44	2, 35, 42, 43	syl3anc 1366	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))))
45		ssralv 4031	. . . . . . 7 ⊢ ((𝐴[,]𝐵) ⊆ 𝐷 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))))
46	3, 45	syl 17	. . . . . 6 ⊢ (𝜑 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))))
47	46	ad2antrr 724	. . . . 5 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))))
48	8	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐵 ∈ ℝ)
49	23	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 ∈ ℝ)
50		rphalfcl 12408	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ⁺ → (𝑧 / 2) ∈ ℝ⁺)
51	50	adantl 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝑧 / 2) ∈ ℝ⁺)
52	51	rpred 12423	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝑧 / 2) ∈ ℝ)
53	49, 52	readdcld 10662	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 + (𝑧 / 2)) ∈ ℝ)
54	48, 53	ifcld 4510	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ)
55	7	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
56	25	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐴 ≤ 𝐶)
57	15	simprd 498	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 < (𝐹‘𝐵))
58		fveq2 6663	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
59	58	eleq1d 2895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐵) ∈ ℝ))
60	7	rexrd 10683	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
61	8	rexrd 10683	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
62	7, 8, 13	ltled 10780	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
63		ubicc2 12845	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
64	60, 61, 62, 63	syl3anc 1366	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
65	59, 38, 64	rspcdva 3623	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ)
66		lttr 10709	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝐶) ∈ ℝ ∧ 𝑈 ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ) → (((𝐹‘𝐶) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)) → (𝐹‘𝐶) < (𝐹‘𝐵)))
67	39, 12, 65, 66	syl3anc 1366	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐹‘𝐶) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)) → (𝐹‘𝐶) < (𝐹‘𝐵)))
68	57, 67	mpan2d 692	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝐶) < 𝑈 → (𝐹‘𝐶) < (𝐹‘𝐵)))
69	68	imp 409	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (𝐹‘𝐶) < (𝐹‘𝐵))
70	69	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐹‘𝐶) < (𝐹‘𝐵))
71	39	ltnrd 10766	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < (𝐹‘𝐶))
72		fveq2 6663	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 𝐶 → (𝐹‘𝐵) = (𝐹‘𝐶))
73	72	breq2d 5069	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 = 𝐶 → ((𝐹‘𝐶) < (𝐹‘𝐵) ↔ (𝐹‘𝐶) < (𝐹‘𝐶)))
74	73	notbid 320	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = 𝐶 → (¬ (𝐹‘𝐶) < (𝐹‘𝐵) ↔ ¬ (𝐹‘𝐶) < (𝐹‘𝐶)))
75	71, 74	syl5ibrcom 249	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 = 𝐶 → ¬ (𝐹‘𝐶) < (𝐹‘𝐵)))
76	75	necon2ad 3029	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐵 ≠ 𝐶))
77	76, 30	jctild 528	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
78	23, 8	ltlend 10777	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 < 𝐵 ↔ (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
79	77, 78	sylibrd 261	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵))
80	79	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵))
81	70, 80	mpd 15	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 < 𝐵)
82	49, 51	ltaddrpd 12456	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 < (𝐶 + (𝑧 / 2)))
83		breq2 5061	. . . . . . . . . . . 12 ⊢ (𝐵 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < 𝐵 ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))
84		breq2 5061	. . . . . . . . . . . 12 ⊢ ((𝐶 + (𝑧 / 2)) = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < (𝐶 + (𝑧 / 2)) ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))
85	83, 84	ifboth 4503	. . . . . . . . . . 11 ⊢ ((𝐶 < 𝐵 ∧ 𝐶 < (𝐶 + (𝑧 / 2))) → 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
86	81, 82, 85	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
87	49, 54, 86	ltled 10780	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
88	55, 49, 54, 56, 87	letrd 10789	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
89		min1 12574	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ ∧ (𝐶 + (𝑧 / 2)) ∈ ℝ) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)
90	48, 53, 89	syl2anc 586	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)
91		elicc2 12793	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)))
92	7, 8, 91	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)))
93	92	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)))
94	54, 88, 90, 93	mpbir3and 1337	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵))
95	49, 54, 87	abssubge0d 14783	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) = (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶))
96		rpre 12389	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ⁺ → 𝑧 ∈ ℝ)
97	96	adantl 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝑧 ∈ ℝ)
98	49, 97	readdcld 10662	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 + 𝑧) ∈ ℝ)
99		min2 12575	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ (𝐶 + (𝑧 / 2)) ∈ ℝ) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ (𝐶 + (𝑧 / 2)))
100	48, 53, 99	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ (𝐶 + (𝑧 / 2)))
101		rphalflt 12410	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ⁺ → (𝑧 / 2) < 𝑧)
102	101	adantl 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝑧 / 2) < 𝑧)
103	52, 97, 49, 102	ltadd2dd 10791	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 + (𝑧 / 2)) < (𝐶 + 𝑧))
104	54, 53, 98, 100, 103	lelttrd 10790	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) < (𝐶 + 𝑧))
105	54, 49, 97	ltsubadd2d 11230	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ((if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶) < 𝑧 ↔ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) < (𝐶 + 𝑧)))
106	104, 105	mpbird 259	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶) < 𝑧)
107	95, 106	eqbrtrd 5079	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧)
108		fvoveq1 7171	. . . . . . . . . 10 ⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (abs‘(𝑦 − 𝐶)) = (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)))
109	108	breq1d 5067	. . . . . . . . 9 ⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → ((abs‘(𝑦 − 𝐶)) < 𝑧 ↔ (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧))
110		breq2 5061	. . . . . . . . 9 ⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < 𝑦 ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))
111	109, 110	anbi12d 632	. . . . . . . 8 ⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦) ↔ ((abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧 ∧ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))))
112	111	rspcev 3621	. . . . . . 7 ⊢ ((if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ∧ ((abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧 ∧ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦))
113	94, 107, 86, 112	syl12anc 834	. . . . . 6 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦))
114		r19.29 3252	. . . . . . 7 ⊢ ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)))
115		pm3.45 623	. . . . . . . . . 10 ⊢ (((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → (((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ∧ 𝐶 < 𝑦)))
116	115	imp 409	. . . . . . . . 9 ⊢ ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ∧ 𝐶 < 𝑦))
117		simprr 771	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝐶 < 𝑦)
118		fveq2 6663	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
119	118	eleq1d 2895	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑦) ∈ ℝ))
120		simplll 773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝜑)
121	120, 38	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
122		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑦 ∈ (𝐴[,]𝐵))
123	119, 121, 122	rspcdva 3623	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝑦) ∈ ℝ)
124	120, 39	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝐶) ∈ ℝ)
125	120, 12	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑈 ∈ ℝ)
126	125, 124	resubcld 11060	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑈 − (𝐹‘𝐶)) ∈ ℝ)
127	123, 124, 126	absdifltd 14785	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ↔ (((𝐹‘𝐶) − (𝑈 − (𝐹‘𝐶))) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))))))
128		ltle 10721	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹‘𝑦) < 𝑈 → (𝐹‘𝑦) ≤ 𝑈))
129	123, 125, 128	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < 𝑈 → (𝐹‘𝑦) ≤ 𝑈))
130	124	recnd 10661	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝐶) ∈ ℂ)
131	125	recnd 10661	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑈 ∈ ℂ)
132	130, 131	pncan3d 10992	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) = 𝑈)
133	132	breq2d 5069	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) ↔ (𝐹‘𝑦) < 𝑈))
134	118	breq1d 5067	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑈 ↔ (𝐹‘𝑦) ≤ 𝑈))
135	134, 5	elrab2 3681	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ (𝐴[,]𝐵) ∧ (𝐹‘𝑦) ≤ 𝑈))
136	135	baib 538	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (𝐴[,]𝐵) → (𝑦 ∈ 𝑆 ↔ (𝐹‘𝑦) ≤ 𝑈))
137	136	ad2antrl 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 ↔ (𝐹‘𝑦) ≤ 𝑈))
138	129, 133, 137	3imtr4d 296	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) → 𝑦 ∈ 𝑆))
139		suprub 11594	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ sup(𝑆, ℝ, < ))
140	139, 4	breqtrrdi 5099	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ 𝐶)
141	140	ex 415	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) → (𝑦 ∈ 𝑆 → 𝑦 ≤ 𝐶))
142	120, 26, 141	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 → 𝑦 ≤ 𝐶))
143	120, 10	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐴[,]𝐵) ⊆ ℝ)
144	143, 122	sseldd 3966	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑦 ∈ ℝ)
145	120, 23	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝐶 ∈ ℝ)
146	144, 145	lenltd 10778	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ≤ 𝐶 ↔ ¬ 𝐶 < 𝑦))
147	142, 146	sylibd 241	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 → ¬ 𝐶 < 𝑦))
148	138, 147	syld 47	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) → ¬ 𝐶 < 𝑦))
149	148	adantld 493	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((((𝐹‘𝐶) − (𝑈 − (𝐹‘𝐶))) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶)))) → ¬ 𝐶 < 𝑦))
150	127, 149	sylbid 242	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) → ¬ 𝐶 < 𝑦))
151	117, 150	mt2d 138	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ¬ (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))
152	151	pm2.21d 121	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) → ¬ (𝐹‘𝐶) < 𝑈))
153	152	expr 459	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐶 < 𝑦 → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) → ¬ (𝐹‘𝐶) < 𝑈)))
154	153	impcomd 414	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ∧ 𝐶 < 𝑦) → ¬ (𝐹‘𝐶) < 𝑈))
155	116, 154	syl5 34	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ¬ (𝐹‘𝐶) < 𝑈))
156	155	rexlimdva 3282	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ¬ (𝐹‘𝐶) < 𝑈))
157	114, 156	syl5 34	. . . . . 6 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ¬ (𝐹‘𝐶) < 𝑈))
158	113, 157	mpan2d 692	. . . . 5 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ¬ (𝐹‘𝐶) < 𝑈))
159	47, 158	syld 47	. . . 4 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ¬ (𝐹‘𝐶) < 𝑈))
160	159	rexlimdva 3282	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ¬ (𝐹‘𝐶) < 𝑈))
161	44, 160	mpd 15	. 2 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → ¬ (𝐹‘𝐶) < 𝑈)
162	161	pm2.01da 797	1 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < 𝑈)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1082 = wceq 1531 ∈ wcel 2108 ≠ wne 3014 ∀wral 3136 ∃wrex 3137 {crab 3140 ⊆ wss 3934 ∅c0 4289 ifcif 4465 class class class wbr 5057 ‘cfv 6348 (class class class)co 7148 supcsup 8896 ℂcc 10527 ℝcr 10528 + caddc 10532 ℝ^*cxr 10666 < clt 10667 ≤ cle 10668 − cmin 10862 / cdiv 11289 2c2 11684 ℝ⁺crp 12381 [,]cicc 12733 abscabs 14585 –cn→ccncf 23476

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7453 ax-cnex 10585 ax-resscn 10586 ax-1cn 10587 ax-icn 10588 ax-addcl 10589 ax-addrcl 10590 ax-mulcl 10591 ax-mulrcl 10592 ax-mulcom 10593 ax-addass 10594 ax-mulass 10595 ax-distr 10596 ax-i2m1 10597 ax-1ne0 10598 ax-1rid 10599 ax-rnegex 10600 ax-rrecex 10601 ax-cnre 10602 ax-pre-lttri 10603 ax-pre-lttrn 10604 ax-pre-ltadd 10605 ax-pre-mulgt0 10606 ax-pre-sup 10607

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1083 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-mo 2616 df-eu 2648 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ne 3015 df-nel 3122 df-ral 3141 df-rex 3142 df-reu 3143 df-rmo 3144 df-rab 3145 df-v 3495 df-sbc 3771 df-csb 3882 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-pss 3952 df-nul 4290 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-tp 4564 df-op 4566 df-uni 4831 df-iun 4912 df-br 5058 df-opab 5120 df-mpt 5138 df-tr 5164 df-id 5453 df-eprel 5458 df-po 5467 df-so 5468 df-fr 5507 df-we 5509 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-pred 6141 df-ord 6187 df-on 6188 df-lim 6189 df-suc 6190 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 df-fv 6356 df-riota 7106 df-ov 7151 df-oprab 7152 df-mpo 7153 df-om 7573 df-2nd 7682 df-wrecs 7939 df-recs 8000 df-rdg 8038 df-er 8281 df-map 8400 df-en 8502 df-dom 8503 df-sdom 8504 df-sup 8898 df-pnf 10669 df-mnf 10670 df-xr 10671 df-ltxr 10672 df-le 10673 df-sub 10864 df-neg 10865 df-div 11290 df-nn 11631 df-2 11692 df-3 11693 df-n0 11890 df-z 11974 df-uz 12236 df-rp 12382 df-icc 12737 df-seq 13362 df-exp 13422 df-cj 14450 df-re 14451 df-im 14452 df-sqrt 14586 df-abs 14587 df-cncf 23478

This theorem is referenced by: ivthlem3 24046

W3C validator