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 24056

Description: Lemma for ivth 24058. 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 4060	. . . . . . . . . 10 ⊢ 𝑆 ⊆ (𝐴[,]𝐵)
7		ivth.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
8		ivth.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9		iccssre 12821	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
10	7, 8, 9	syl2anc 586	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
11	6, 10	sstrid 3981	. . . . . . . . 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 24055	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
17	16	simpld 497	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
18	17	ne0d 4304	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ≠ ∅)
19	16	simprd 498	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵)
20		brralrspcev 5129	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
21	8, 19, 20	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
22	11, 18, 21	suprcld 11607	. . . . . . . 8 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ ℝ)
23	4, 22	eqeltrid 2920	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℝ)
24	11, 18, 21, 17	suprubd 11606	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < ))
25	24, 4	breqtrrdi 5111	. . . . . . 7 ⊢ (𝜑 → 𝐴 ≤ 𝐶)
26	11, 18, 21	3jca 1124	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
27		suprleub 11610	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
28	26, 8, 27	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
29	19, 28	mpbird 259	. . . . . . . 8 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ≤ 𝐵)
30	4, 29	eqbrtrid 5104	. . . . . . 7 ⊢ (𝜑 → 𝐶 ≤ 𝐵)
31		elicc2 12804	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
32	7, 8, 31	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
33	23, 25, 30, 32	mpbir3and 1338	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))
34	3, 33	sseldd 3971	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝐷)
35	34	adantr 483	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → 𝐶 ∈ 𝐷)
36		fveq2 6673	. . . . . . . 8 ⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶))
37	36	eleq1d 2900	. . . . . . 7 ⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐶) ∈ ℝ))
38	14	ralrimiva 3185	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
39	37, 38, 33	rspcdva 3628	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℝ)
40		difrp 12430	. . . . . 6 ⊢ (((𝐹‘𝐶) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹‘𝐶) < 𝑈 ↔ (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺))
41	39, 12, 40	syl2anc 586	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝐶) < 𝑈 ↔ (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺))
42	41	biimpa 479	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺)
43		cncfi 23505	. . . 4 ⊢ ((𝐹 ∈ (𝐷–cn→ℂ) ∧ 𝐶 ∈ 𝐷 ∧ (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))))
44	2, 35, 42, 43	syl3anc 1367	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))))
45		ssralv 4036	. . . . . . 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 12419	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ⁺ → (𝑧 / 2) ∈ ℝ⁺)
51	50	adantl 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝑧 / 2) ∈ ℝ⁺)
52	51	rpred 12434	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝑧 / 2) ∈ ℝ)
53	49, 52	readdcld 10673	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 + (𝑧 / 2)) ∈ ℝ)
54	48, 53	ifcld 4515	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ)
55	7	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
56	25	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐴 ≤ 𝐶)
57	15	simprd 498	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 < (𝐹‘𝐵))
58		fveq2 6673	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
59	58	eleq1d 2900	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐵) ∈ ℝ))
60	7	rexrd 10694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
61	8	rexrd 10694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
62	7, 8, 13	ltled 10791	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
63		ubicc2 12856	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
64	60, 61, 62, 63	syl3anc 1367	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
65	59, 38, 64	rspcdva 3628	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ)
66		lttr 10720	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝐶) ∈ ℝ ∧ 𝑈 ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ) → (((𝐹‘𝐶) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)) → (𝐹‘𝐶) < (𝐹‘𝐵)))
67	39, 12, 65, 66	syl3anc 1367	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐹‘𝐶) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)) → (𝐹‘𝐶) < (𝐹‘𝐵)))
68	57, 67	mpan2d 692	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝐶) < 𝑈 → (𝐹‘𝐶) < (𝐹‘𝐵)))
69	68	imp 409	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (𝐹‘𝐶) < (𝐹‘𝐵))
70	69	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐹‘𝐶) < (𝐹‘𝐵))
71	39	ltnrd 10777	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < (𝐹‘𝐶))
72		fveq2 6673	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 𝐶 → (𝐹‘𝐵) = (𝐹‘𝐶))
73	72	breq2d 5081	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 = 𝐶 → ((𝐹‘𝐶) < (𝐹‘𝐵) ↔ (𝐹‘𝐶) < (𝐹‘𝐶)))
74	73	notbid 320	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = 𝐶 → (¬ (𝐹‘𝐶) < (𝐹‘𝐵) ↔ ¬ (𝐹‘𝐶) < (𝐹‘𝐶)))
75	71, 74	syl5ibrcom 249	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 = 𝐶 → ¬ (𝐹‘𝐶) < (𝐹‘𝐵)))
76	75	necon2ad 3034	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐵 ≠ 𝐶))
77	76, 30	jctild 528	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
78	23, 8	ltlend 10788	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 < 𝐵 ↔ (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
79	77, 78	sylibrd 261	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵))
80	79	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵))
81	70, 80	mpd 15	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 < 𝐵)
82	49, 51	ltaddrpd 12467	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 < (𝐶 + (𝑧 / 2)))
83		breq2 5073	. . . . . . . . . . . 12 ⊢ (𝐵 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < 𝐵 ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))
84		breq2 5073	. . . . . . . . . . . 12 ⊢ ((𝐶 + (𝑧 / 2)) = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < (𝐶 + (𝑧 / 2)) ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))
85	83, 84	ifboth 4508	. . . . . . . . . . 11 ⊢ ((𝐶 < 𝐵 ∧ 𝐶 < (𝐶 + (𝑧 / 2))) → 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
86	81, 82, 85	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
87	49, 54, 86	ltled 10791	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
88	55, 49, 54, 56, 87	letrd 10800	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
89		min1 12585	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ ∧ (𝐶 + (𝑧 / 2)) ∈ ℝ) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)
90	48, 53, 89	syl2anc 586	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)
91		elicc2 12804	. . . . . . . . . 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 1338	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵))
95	49, 54, 87	abssubge0d 14794	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) = (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶))
96		rpre 12400	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ⁺ → 𝑧 ∈ ℝ)
97	96	adantl 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝑧 ∈ ℝ)
98	49, 97	readdcld 10673	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 + 𝑧) ∈ ℝ)
99		min2 12586	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ (𝐶 + (𝑧 / 2)) ∈ ℝ) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ (𝐶 + (𝑧 / 2)))
100	48, 53, 99	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ (𝐶 + (𝑧 / 2)))
101		rphalflt 12421	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ⁺ → (𝑧 / 2) < 𝑧)
102	101	adantl 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝑧 / 2) < 𝑧)
103	52, 97, 49, 102	ltadd2dd 10802	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 + (𝑧 / 2)) < (𝐶 + 𝑧))
104	54, 53, 98, 100, 103	lelttrd 10801	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) < (𝐶 + 𝑧))
105	54, 49, 97	ltsubadd2d 11241	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ((if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶) < 𝑧 ↔ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) < (𝐶 + 𝑧)))
106	104, 105	mpbird 259	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶) < 𝑧)
107	95, 106	eqbrtrd 5091	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧)
108		fvoveq1 7182	. . . . . . . . . 10 ⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (abs‘(𝑦 − 𝐶)) = (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)))
109	108	breq1d 5079	. . . . . . . . 9 ⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → ((abs‘(𝑦 − 𝐶)) < 𝑧 ↔ (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧))
110		breq2 5073	. . . . . . . . 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 3626	. . . . . . 7 ⊢ ((if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ∧ ((abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧 ∧ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦))
113	94, 107, 86, 112	syl12anc 834	. . . . . 6 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦))
114		r19.29 3257	. . . . . . 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 6673	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
119	118	eleq1d 2900	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑦) ∈ ℝ))
120		simplll 773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝜑)
121	120, 38	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
122		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑦 ∈ (𝐴[,]𝐵))
123	119, 121, 122	rspcdva 3628	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝑦) ∈ ℝ)
124	120, 39	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝐶) ∈ ℝ)
125	120, 12	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑈 ∈ ℝ)
126	125, 124	resubcld 11071	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑈 − (𝐹‘𝐶)) ∈ ℝ)
127	123, 124, 126	absdifltd 14796	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ↔ (((𝐹‘𝐶) − (𝑈 − (𝐹‘𝐶))) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))))))
128		ltle 10732	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹‘𝑦) < 𝑈 → (𝐹‘𝑦) ≤ 𝑈))
129	123, 125, 128	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < 𝑈 → (𝐹‘𝑦) ≤ 𝑈))
130	124	recnd 10672	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝐶) ∈ ℂ)
131	125	recnd 10672	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑈 ∈ ℂ)
132	130, 131	pncan3d 11003	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) = 𝑈)
133	132	breq2d 5081	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) ↔ (𝐹‘𝑦) < 𝑈))
134	118	breq1d 5079	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑈 ↔ (𝐹‘𝑦) ≤ 𝑈))
135	134, 5	elrab2 3686	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ (𝐴[,]𝐵) ∧ (𝐹‘𝑦) ≤ 𝑈))
136	135	baib 538	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (𝐴[,]𝐵) → (𝑦 ∈ 𝑆 ↔ (𝐹‘𝑦) ≤ 𝑈))
137	136	ad2antrl 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 ↔ (𝐹‘𝑦) ≤ 𝑈))
138	129, 133, 137	3imtr4d 296	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) → 𝑦 ∈ 𝑆))
139		suprub 11605	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ sup(𝑆, ℝ, < ))
140	139, 4	breqtrrdi 5111	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ 𝐶)
141	140	ex 415	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) → (𝑦 ∈ 𝑆 → 𝑦 ≤ 𝐶))
142	120, 26, 141	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 → 𝑦 ≤ 𝐶))
143	120, 10	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐴[,]𝐵) ⊆ ℝ)
144	143, 122	sseldd 3971	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑦 ∈ ℝ)
145	120, 23	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝐶 ∈ ℝ)
146	144, 145	lenltd 10789	. . . . . . . . . . . . . . . . 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 3287	. . . . . . 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 3287	. . 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 1083 = wceq 1536 ∈ wcel 2113 ≠ wne 3019 ∀wral 3141 ∃wrex 3142 {crab 3145 ⊆ wss 3939 ∅c0 4294 ifcif 4470 class class class wbr 5069 ‘cfv 6358 (class class class)co 7159 supcsup 8907 ℂcc 10538 ℝcr 10539 + caddc 10543 ℝ^*cxr 10677 < clt 10678 ≤ cle 10679 − cmin 10873 / cdiv 11300 2c2 11695 ℝ⁺crp 12392 [,]cicc 12744 abscabs 14596 –cn→ccncf 23487

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-sep 5206 ax-nul 5213 ax-pow 5269 ax-pr 5333 ax-un 7464 ax-cnex 10596 ax-resscn 10597 ax-1cn 10598 ax-icn 10599 ax-addcl 10600 ax-addrcl 10601 ax-mulcl 10602 ax-mulrcl 10603 ax-mulcom 10604 ax-addass 10605 ax-mulass 10606 ax-distr 10607 ax-i2m1 10608 ax-1ne0 10609 ax-1rid 10610 ax-rnegex 10611 ax-rrecex 10612 ax-cnre 10613 ax-pre-lttri 10614 ax-pre-lttrn 10615 ax-pre-ltadd 10616 ax-pre-mulgt0 10617 ax-pre-sup 10618

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-nel 3127 df-ral 3146 df-rex 3147 df-reu 3148 df-rmo 3149 df-rab 3150 df-v 3499 df-sbc 3776 df-csb 3887 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-pss 3957 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-tp 4575 df-op 4577 df-uni 4842 df-iun 4924 df-br 5070 df-opab 5132 df-mpt 5150 df-tr 5176 df-id 5463 df-eprel 5468 df-po 5477 df-so 5478 df-fr 5517 df-we 5519 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-pred 6151 df-ord 6197 df-on 6198 df-lim 6199 df-suc 6200 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-riota 7117 df-ov 7162 df-oprab 7163 df-mpo 7164 df-om 7584 df-2nd 7693 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-er 8292 df-map 8411 df-en 8513 df-dom 8514 df-sdom 8515 df-sup 8909 df-pnf 10680 df-mnf 10681 df-xr 10682 df-ltxr 10683 df-le 10684 df-sub 10875 df-neg 10876 df-div 11301 df-nn 11642 df-2 11703 df-3 11704 df-n0 11901 df-z 11985 df-uz 12247 df-rp 12393 df-icc 12748 df-seq 13373 df-exp 13433 df-cj 14461 df-re 14462 df-im 14463 df-sqrt 14597 df-abs 14598 df-cncf 23489

This theorem is referenced by: ivthlem3 24057

W3C validator