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 25778

Description: Lemma for ivth 25780. 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 486	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → 𝐹 ∈ (𝐷–cn→ℂ))
3		ivth.5	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
4		ivth.11	. . . . . . . 8 ⊢ 𝐶 = sup(𝑆, ℝ, < )
5		ivth.10	. . . . . . . . . . 11 ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈}
6	5	ssrab3 4007	. . . . . . . . . 10 ⊢ 𝑆 ⊆ (𝐴[,]𝐵)
7		ivth.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
8		ivth.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9		iccssre 13563	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
10	7, 8, 9	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
11	6, 10	sstrid 3919	. . . . . . . . 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 25777	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
17	16	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
18	17	ne0d 4287	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ≠ ∅)
19	16	simprd 501	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵)
20		brralrspcev 5164	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
21	8, 19, 20	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
22	11, 18, 21	suprcld 12283	. . . . . . . 8 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ ℝ)
23	4, 22	eqeltrid 2864	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℝ)
24	11, 18, 21, 17	suprubd 12282	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < ))
25	24, 4	breqtrrdi 5146	. . . . . . 7 ⊢ (𝜑 → 𝐴 ≤ 𝐶)
26	11, 18, 21	3jca 1146	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
27		suprleub 12286	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
28	26, 8, 27	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
29	19, 28	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ≤ 𝐵)
30	4, 29	eqbrtrid 5139	. . . . . . 7 ⊢ (𝜑 → 𝐶 ≤ 𝐵)
31		elicc2 13545	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
32	7, 8, 31	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
33	23, 25, 30, 32	mpbir3and 1361	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))
34	3, 33	sseldd 3909	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝐷)
35	34	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → 𝐶 ∈ 𝐷)
36		fveq2 6885	. . . . . . . 8 ⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶))
37	36	eleq1d 2845	. . . . . . 7 ⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐶) ∈ ℝ))
38	14	ralrimiva 3154	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
39	37, 38, 33	rspcdva 3577	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℝ)
40		difrp 13163	. . . . . 6 ⊢ (((𝐹‘𝐶) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹‘𝐶) < 𝑈 ↔ (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺))
41	39, 12, 40	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝐶) < 𝑈 ↔ (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺))
42	41	biimpa 482	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺)
43		cncfi 25220	. . . 4 ⊢ ((𝐹 ∈ (𝐷–cn→ℂ) ∧ 𝐶 ∈ 𝐷 ∧ (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))))
44	2, 35, 42, 43	syl3anc 1398	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))))
45		ssralv 3977	. . . . . . 7 ⊢ ((𝐴[,]𝐵) ⊆ 𝐷 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))))
46	3, 45	syl 18	. . . . . 6 ⊢ (𝜑 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))))
47	46	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))))
48	8	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐵 ∈ ℝ)
49	23	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 ∈ ℝ)
50		rphalfcl 13152	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ⁺ → (𝑧 / 2) ∈ ℝ⁺)
51	50	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝑧 / 2) ∈ ℝ⁺)
52	51	rpred 13167	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝑧 / 2) ∈ ℝ)
53	49, 52	readdcld 11341	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 + (𝑧 / 2)) ∈ ℝ)
54	48, 53	ifcld 4528	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ)
55	7	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
56	25	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐴 ≤ 𝐶)
57	15	simprd 501	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 < (𝐹‘𝐵))
58		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
59	58	eleq1d 2845	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐵) ∈ ℝ))
60	7	rexrd 11362	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
61	8	rexrd 11362	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
62	7, 8, 13	ltled 11461	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
63		ubicc2 13599	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
64	60, 61, 62, 63	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
65	59, 38, 64	rspcdva 3577	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ)
66		lttr 11389	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝐶) ∈ ℝ ∧ 𝑈 ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ) → (((𝐹‘𝐶) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)) → (𝐹‘𝐶) < (𝐹‘𝐵)))
67	39, 12, 65, 66	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐹‘𝐶) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)) → (𝐹‘𝐶) < (𝐹‘𝐵)))
68	57, 67	mpan2d 707	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝐶) < 𝑈 → (𝐹‘𝐶) < (𝐹‘𝐵)))
69	68	imp 412	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (𝐹‘𝐶) < (𝐹‘𝐵))
70	69	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐹‘𝐶) < (𝐹‘𝐵))
71	39	ltnrd 11447	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < (𝐹‘𝐶))
72		fveq2 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 𝐶 → (𝐹‘𝐵) = (𝐹‘𝐶))
73	72	breq2d 5114	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 = 𝐶 → ((𝐹‘𝐶) < (𝐹‘𝐵) ↔ (𝐹‘𝐶) < (𝐹‘𝐶)))
74	73	notbid 321	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = 𝐶 → (¬ (𝐹‘𝐶) < (𝐹‘𝐵) ↔ ¬ (𝐹‘𝐶) < (𝐹‘𝐶)))
75	71, 74	syl5ibrcom 250	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 = 𝐶 → ¬ (𝐹‘𝐶) < (𝐹‘𝐵)))
76	75	necon2ad 2970	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐵 ≠ 𝐶))
77	76, 30	jctild 535	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
78	23, 8	ltlend 11458	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 < 𝐵 ↔ (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
79	77, 78	sylibrd 262	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵))
80	79	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵))
81	70, 80	mpd 16	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 < 𝐵)
82	49, 51	ltaddrpd 13200	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 < (𝐶 + (𝑧 / 2)))
83		breq2 5106	. . . . . . . . . . . 12 ⊢ (𝐵 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < 𝐵 ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))
84		breq2 5106	. . . . . . . . . . . 12 ⊢ ((𝐶 + (𝑧 / 2)) = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < (𝐶 + (𝑧 / 2)) ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))
85	83, 84	ifboth 4521	. . . . . . . . . . 11 ⊢ ((𝐶 < 𝐵 ∧ 𝐶 < (𝐶 + (𝑧 / 2))) → 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
86	81, 82, 85	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
87	49, 54, 86	ltled 11461	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
88	55, 49, 54, 56, 87	letrd 11470	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
89		min1 13322	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ ∧ (𝐶 + (𝑧 / 2)) ∈ ℝ) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)
90	48, 53, 89	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)
91		elicc2 13545	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)))
92	7, 8, 91	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)))
93	92	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)))
94	54, 88, 90, 93	mpbir3and 1361	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵))
95	49, 54, 87	abssubge0d 15606	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) = (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶))
96		rpre 13132	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ⁺ → 𝑧 ∈ ℝ)
97	96	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝑧 ∈ ℝ)
98	49, 97	readdcld 11341	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 + 𝑧) ∈ ℝ)
99		min2 13323	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ (𝐶 + (𝑧 / 2)) ∈ ℝ) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ (𝐶 + (𝑧 / 2)))
100	48, 53, 99	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ (𝐶 + (𝑧 / 2)))
101		rphalflt 13154	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ⁺ → (𝑧 / 2) < 𝑧)
102	101	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝑧 / 2) < 𝑧)
103	52, 97, 49, 102	ltadd2dd 11472	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 + (𝑧 / 2)) < (𝐶 + 𝑧))
104	54, 53, 98, 100, 103	lelttrd 11471	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) < (𝐶 + 𝑧))
105	54, 49, 97	ltsubadd2d 11917	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ((if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶) < 𝑧 ↔ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) < (𝐶 + 𝑧)))
106	104, 105	mpbird 260	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶) < 𝑧)
107	95, 106	eqbrtrd 5126	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧)
108		fvoveq1 7443	. . . . . . . . . 10 ⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (abs‘(𝑦 − 𝐶)) = (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)))
109	108	breq1d 5112	. . . . . . . . 9 ⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → ((abs‘(𝑦 − 𝐶)) < 𝑧 ↔ (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧))
110		breq2 5106	. . . . . . . . 9 ⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < 𝑦 ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))
111	109, 110	anbi12d 644	. . . . . . . 8 ⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦) ↔ ((abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧 ∧ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))))
112	111	rspcev 3576	. . . . . . 7 ⊢ ((if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ∧ ((abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧 ∧ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦))
113	94, 107, 86, 112	syl12anc 850	. . . . . 6 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦))
114		r19.29 3125	. . . . . . 7 ⊢ ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)))
115		pm3.45 634	. . . . . . . . . 10 ⊢ (((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → (((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ∧ 𝐶 < 𝑦)))
116	115	imp 412	. . . . . . . . 9 ⊢ ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ∧ 𝐶 < 𝑦))
117		simprr 785	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝐶 < 𝑦)
118		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
119	118	eleq1d 2845	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑦) ∈ ℝ))
120		simplll 787	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝜑)
121	120, 38	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
122		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑦 ∈ (𝐴[,]𝐵))
123	119, 121, 122	rspcdva 3577	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝑦) ∈ ℝ)
124	120, 39	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝐶) ∈ ℝ)
125	120, 12	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑈 ∈ ℝ)
126	125, 124	resubcld 11747	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑈 − (𝐹‘𝐶)) ∈ ℝ)
127	123, 124, 126	absdifltd 15608	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ↔ (((𝐹‘𝐶) − (𝑈 − (𝐹‘𝐶))) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))))))
128		ltle 11401	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹‘𝑦) < 𝑈 → (𝐹‘𝑦) ≤ 𝑈))
129	123, 125, 128	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < 𝑈 → (𝐹‘𝑦) ≤ 𝑈))
130	124	recnd 11340	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝐶) ∈ ℂ)
131	125	recnd 11340	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑈 ∈ ℂ)
132	130, 131	pncan3d 11675	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) = 𝑈)
133	132	breq2d 5114	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) ↔ (𝐹‘𝑦) < 𝑈))
134	118	breq1d 5112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑈 ↔ (𝐹‘𝑦) ≤ 𝑈))
135	134, 5	elrab2 3648	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ (𝐴[,]𝐵) ∧ (𝐹‘𝑦) ≤ 𝑈))
136	135	baib 545	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (𝐴[,]𝐵) → (𝑦 ∈ 𝑆 ↔ (𝐹‘𝑦) ≤ 𝑈))
137	136	ad2antrl 741	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 ↔ (𝐹‘𝑦) ≤ 𝑈))
138	129, 133, 137	3imtr4d 297	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) → 𝑦 ∈ 𝑆))
139		suprub 12281	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ sup(𝑆, ℝ, < ))
140	139, 4	breqtrrdi 5146	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ 𝐶)
141	140	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) → (𝑦 ∈ 𝑆 → 𝑦 ≤ 𝐶))
142	120, 26, 141	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 → 𝑦 ≤ 𝐶))
143	120, 10	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐴[,]𝐵) ⊆ ℝ)
144	143, 122	sseldd 3909	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑦 ∈ ℝ)
145	120, 23	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝐶 ∈ ℝ)
146	144, 145	lenltd 11459	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ≤ 𝐶 ↔ ¬ 𝐶 < 𝑦))
147	142, 146	sylibd 242	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 → ¬ 𝐶 < 𝑦))
148	138, 147	syld 48	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) → ¬ 𝐶 < 𝑦))
149	148	adantld 496	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((((𝐹‘𝐶) − (𝑈 − (𝐹‘𝐶))) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶)))) → ¬ 𝐶 < 𝑦))
150	127, 149	sylbid 243	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) → ¬ 𝐶 < 𝑦))
151	117, 150	mt2d 137	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ¬ (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))
152	151	pm2.21d 122	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) → ¬ (𝐹‘𝐶) < 𝑈))
153	152	expr 462	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐶 < 𝑦 → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) → ¬ (𝐹‘𝐶) < 𝑈)))
154	153	impcomd 417	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ∧ 𝐶 < 𝑦) → ¬ (𝐹‘𝐶) < 𝑈))
155	116, 154	syl5 35	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ¬ (𝐹‘𝐶) < 𝑈))
156	155	rexlimdva 3163	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ¬ (𝐹‘𝐶) < 𝑈))
157	114, 156	syl5 35	. . . . . 6 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ¬ (𝐹‘𝐶) < 𝑈))
158	113, 157	mpan2d 707	. . . . 5 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ¬ (𝐹‘𝐶) < 𝑈))
159	47, 158	syld 48	. . . 4 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ¬ (𝐹‘𝐶) < 𝑈))
160	159	rexlimdva 3163	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ¬ (𝐹‘𝐶) < 𝑈))
161	44, 160	mpd 16	. 2 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → ¬ (𝐹‘𝐶) < 𝑈)
162	161	pm2.01da 811	1 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < 𝑈)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 {crab 3412 ⊆ wss 3895 ∅c0 4278 ifcif 4481 class class class wbr 5102 ‘cfv 6538 (class class class)co 7420 supcsup 9435 ℂcc 11201 ℝcr 11202 + caddc 11206 ℝ^*cxr 11345 < clt 11346 ≤ cle 11347 − cmin 11544 / cdiv 11976 2c2 12400 ℝ⁺crp 13123 [,]cicc 13482 abscabs 15406 –cn→ccncf 25202

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280 ax-pre-sup 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-2nd 8002 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-er 8720 df-map 8852 df-en 8977 df-dom 8978 df-sdom 8979 df-sup 9437 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-div 11977 df-nn 12339 df-2 12408 df-3 12409 df-n0 12610 df-z 12697 df-uz 12969 df-rp 13124 df-icc 13486 df-seq 14148 df-exp 14208 df-cj 15271 df-re 15272 df-im 15273 df-sqrt 15407 df-abs 15408 df-cncf 25204

This theorem is used by: ivthlem3 25779

W3C validator