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 25405

Description: Lemma for ivth 25407. 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 480	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → 𝐹 ∈ (𝐷–cn→ℂ))
3		ivth.5	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
4		ivth.11	. . . . . . . 8 ⊢ 𝐶 = sup(𝑆, ℝ, < )
5		ivth.10	. . . . . . . . . . 11 ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈}
6	5	ssrab3 4057	. . . . . . . . . 10 ⊢ 𝑆 ⊆ (𝐴[,]𝐵)
7		ivth.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
8		ivth.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9		iccssre 13446	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
10	7, 8, 9	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
11	6, 10	sstrid 3970	. . . . . . . . 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 25404	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
17	16	simpld 494	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
18	17	ne0d 4317	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ≠ ∅)
19	16	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵)
20		brralrspcev 5179	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
21	8, 19, 20	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
22	11, 18, 21	suprcld 12205	. . . . . . . 8 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ ℝ)
23	4, 22	eqeltrid 2838	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℝ)
24	11, 18, 21, 17	suprubd 12204	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < ))
25	24, 4	breqtrrdi 5161	. . . . . . 7 ⊢ (𝜑 → 𝐴 ≤ 𝐶)
26	11, 18, 21	3jca 1128	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
27		suprleub 12208	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
28	26, 8, 27	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
29	19, 28	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ≤ 𝐵)
30	4, 29	eqbrtrid 5154	. . . . . . 7 ⊢ (𝜑 → 𝐶 ≤ 𝐵)
31		elicc2 13428	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
32	7, 8, 31	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
33	23, 25, 30, 32	mpbir3and 1343	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))
34	3, 33	sseldd 3959	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝐷)
35	34	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → 𝐶 ∈ 𝐷)
36		fveq2 6876	. . . . . . . 8 ⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶))
37	36	eleq1d 2819	. . . . . . 7 ⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐶) ∈ ℝ))
38	14	ralrimiva 3132	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
39	37, 38, 33	rspcdva 3602	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℝ)
40		difrp 13047	. . . . . 6 ⊢ (((𝐹‘𝐶) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹‘𝐶) < 𝑈 ↔ (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺))
41	39, 12, 40	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝐶) < 𝑈 ↔ (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺))
42	41	biimpa 476	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺)
43		cncfi 24838	. . . 4 ⊢ ((𝐹 ∈ (𝐷–cn→ℂ) ∧ 𝐶 ∈ 𝐷 ∧ (𝑈 − (𝐹‘𝐶)) ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))))
44	2, 35, 42, 43	syl3anc 1373	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))))
45		ssralv 4027	. . . . . . 7 ⊢ ((𝐴[,]𝐵) ⊆ 𝐷 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))))
46	3, 45	syl 17	. . . . . 6 ⊢ (𝜑 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))))
47	46	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))))
48	8	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐵 ∈ ℝ)
49	23	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 ∈ ℝ)
50		rphalfcl 13036	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ⁺ → (𝑧 / 2) ∈ ℝ⁺)
51	50	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝑧 / 2) ∈ ℝ⁺)
52	51	rpred 13051	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝑧 / 2) ∈ ℝ)
53	49, 52	readdcld 11264	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 + (𝑧 / 2)) ∈ ℝ)
54	48, 53	ifcld 4547	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ)
55	7	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐴 ∈ ℝ)
56	25	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐴 ≤ 𝐶)
57	15	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 < (𝐹‘𝐵))
58		fveq2 6876	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵))
59	58	eleq1d 2819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐵) ∈ ℝ))
60	7	rexrd 11285	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
61	8	rexrd 11285	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
62	7, 8, 13	ltled 11383	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
63		ubicc2 13482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
64	60, 61, 62, 63	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
65	59, 38, 64	rspcdva 3602	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ)
66		lttr 11311	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝐶) ∈ ℝ ∧ 𝑈 ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ) → (((𝐹‘𝐶) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)) → (𝐹‘𝐶) < (𝐹‘𝐵)))
67	39, 12, 65, 66	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐹‘𝐶) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)) → (𝐹‘𝐶) < (𝐹‘𝐵)))
68	57, 67	mpan2d 694	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝐶) < 𝑈 → (𝐹‘𝐶) < (𝐹‘𝐵)))
69	68	imp 406	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (𝐹‘𝐶) < (𝐹‘𝐵))
70	69	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐹‘𝐶) < (𝐹‘𝐵))
71	39	ltnrd 11369	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < (𝐹‘𝐶))
72		fveq2 6876	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 𝐶 → (𝐹‘𝐵) = (𝐹‘𝐶))
73	72	breq2d 5131	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 = 𝐶 → ((𝐹‘𝐶) < (𝐹‘𝐵) ↔ (𝐹‘𝐶) < (𝐹‘𝐶)))
74	73	notbid 318	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = 𝐶 → (¬ (𝐹‘𝐶) < (𝐹‘𝐵) ↔ ¬ (𝐹‘𝐶) < (𝐹‘𝐶)))
75	71, 74	syl5ibrcom 247	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 = 𝐶 → ¬ (𝐹‘𝐶) < (𝐹‘𝐵)))
76	75	necon2ad 2947	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐵 ≠ 𝐶))
77	76, 30	jctild 525	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
78	23, 8	ltlend 11380	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 < 𝐵 ↔ (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
79	77, 78	sylibrd 259	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵))
80	79	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵))
81	70, 80	mpd 15	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 < 𝐵)
82	49, 51	ltaddrpd 13084	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 < (𝐶 + (𝑧 / 2)))
83		breq2 5123	. . . . . . . . . . . 12 ⊢ (𝐵 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < 𝐵 ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))
84		breq2 5123	. . . . . . . . . . . 12 ⊢ ((𝐶 + (𝑧 / 2)) = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < (𝐶 + (𝑧 / 2)) ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))
85	83, 84	ifboth 4540	. . . . . . . . . . 11 ⊢ ((𝐶 < 𝐵 ∧ 𝐶 < (𝐶 + (𝑧 / 2))) → 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
86	81, 82, 85	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
87	49, 54, 86	ltled 11383	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
88	55, 49, 54, 56, 87	letrd 11392	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))
89		min1 13205	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ ∧ (𝐶 + (𝑧 / 2)) ∈ ℝ) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)
90	48, 53, 89	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)
91		elicc2 13428	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)))
92	7, 8, 91	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)))
93	92	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵)))
94	54, 88, 90, 93	mpbir3and 1343	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵))
95	49, 54, 87	abssubge0d 15450	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) = (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶))
96		rpre 13017	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ⁺ → 𝑧 ∈ ℝ)
97	96	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → 𝑧 ∈ ℝ)
98	49, 97	readdcld 11264	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 + 𝑧) ∈ ℝ)
99		min2 13206	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ (𝐶 + (𝑧 / 2)) ∈ ℝ) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ (𝐶 + (𝑧 / 2)))
100	48, 53, 99	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ (𝐶 + (𝑧 / 2)))
101		rphalflt 13038	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ⁺ → (𝑧 / 2) < 𝑧)
102	101	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝑧 / 2) < 𝑧)
103	52, 97, 49, 102	ltadd2dd 11394	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 + (𝑧 / 2)) < (𝐶 + 𝑧))
104	54, 53, 98, 100, 103	lelttrd 11393	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) < (𝐶 + 𝑧))
105	54, 49, 97	ltsubadd2d 11835	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ((if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶) < 𝑧 ↔ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) < (𝐶 + 𝑧)))
106	104, 105	mpbird 257	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶) < 𝑧)
107	95, 106	eqbrtrd 5141	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧)
108		fvoveq1 7428	. . . . . . . . . 10 ⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (abs‘(𝑦 − 𝐶)) = (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)))
109	108	breq1d 5129	. . . . . . . . 9 ⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → ((abs‘(𝑦 − 𝐶)) < 𝑧 ↔ (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧))
110		breq2 5123	. . . . . . . . 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 3601	. . . . . . 7 ⊢ ((if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ∧ ((abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧 ∧ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦))
113	94, 107, 86, 112	syl12anc 836	. . . . . 6 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦))
114		r19.29 3101	. . . . . . 7 ⊢ ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)))
115		pm3.45 622	. . . . . . . . . 10 ⊢ (((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → (((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ∧ 𝐶 < 𝑦)))
116	115	imp 406	. . . . . . . . 9 ⊢ ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ∧ 𝐶 < 𝑦))
117		simprr 772	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝐶 < 𝑦)
118		fveq2 6876	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
119	118	eleq1d 2819	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑦) ∈ ℝ))
120		simplll 774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝜑)
121	120, 38	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
122		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑦 ∈ (𝐴[,]𝐵))
123	119, 121, 122	rspcdva 3602	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝑦) ∈ ℝ)
124	120, 39	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝐶) ∈ ℝ)
125	120, 12	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑈 ∈ ℝ)
126	125, 124	resubcld 11665	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑈 − (𝐹‘𝐶)) ∈ ℝ)
127	123, 124, 126	absdifltd 15452	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ↔ (((𝐹‘𝐶) − (𝑈 − (𝐹‘𝐶))) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))))))
128		ltle 11323	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹‘𝑦) < 𝑈 → (𝐹‘𝑦) ≤ 𝑈))
129	123, 125, 128	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < 𝑈 → (𝐹‘𝑦) ≤ 𝑈))
130	124	recnd 11263	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝐶) ∈ ℂ)
131	125	recnd 11263	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑈 ∈ ℂ)
132	130, 131	pncan3d 11597	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) = 𝑈)
133	132	breq2d 5131	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) ↔ (𝐹‘𝑦) < 𝑈))
134	118	breq1d 5129	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑈 ↔ (𝐹‘𝑦) ≤ 𝑈))
135	134, 5	elrab2 3674	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ (𝐴[,]𝐵) ∧ (𝐹‘𝑦) ≤ 𝑈))
136	135	baib 535	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (𝐴[,]𝐵) → (𝑦 ∈ 𝑆 ↔ (𝐹‘𝑦) ≤ 𝑈))
137	136	ad2antrl 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 ↔ (𝐹‘𝑦) ≤ 𝑈))
138	129, 133, 137	3imtr4d 294	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) → 𝑦 ∈ 𝑆))
139		suprub 12203	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ sup(𝑆, ℝ, < ))
140	139, 4	breqtrrdi 5161	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ 𝐶)
141	140	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) → (𝑦 ∈ 𝑆 → 𝑦 ≤ 𝐶))
142	120, 26, 141	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 → 𝑦 ≤ 𝐶))
143	120, 10	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐴[,]𝐵) ⊆ ℝ)
144	143, 122	sseldd 3959	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑦 ∈ ℝ)
145	120, 23	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝐶 ∈ ℝ)
146	144, 145	lenltd 11381	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ≤ 𝐶 ↔ ¬ 𝐶 < 𝑦))
147	142, 146	sylibd 239	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 → ¬ 𝐶 < 𝑦))
148	138, 147	syld 47	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) → ¬ 𝐶 < 𝑦))
149	148	adantld 490	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((((𝐹‘𝐶) − (𝑈 − (𝐹‘𝐶))) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶)))) → ¬ 𝐶 < 𝑦))
150	127, 149	sylbid 240	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) → ¬ 𝐶 < 𝑦))
151	117, 150	mt2d 136	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ¬ (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))
152	151	pm2.21d 121	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) → ¬ (𝐹‘𝐶) < 𝑈))
153	152	expr 456	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐶 < 𝑦 → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) → ¬ (𝐹‘𝐶) < 𝑈)))
154	153	impcomd 411	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ∧ 𝐶 < 𝑦) → ¬ (𝐹‘𝐶) < 𝑈))
155	116, 154	syl5 34	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ¬ (𝐹‘𝐶) < 𝑈))
156	155	rexlimdva 3141	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ¬ (𝐹‘𝐶) < 𝑈))
157	114, 156	syl5 34	. . . . . 6 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ¬ (𝐹‘𝐶) < 𝑈))
158	113, 157	mpan2d 694	. . . . 5 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ¬ (𝐹‘𝐶) < 𝑈))
159	47, 158	syld 47	. . . 4 ⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ¬ (𝐹‘𝐶) < 𝑈))
160	159	rexlimdva 3141	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ¬ (𝐹‘𝐶) < 𝑈))
161	44, 160	mpd 15	. 2 ⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → ¬ (𝐹‘𝐶) < 𝑈)
162	161	pm2.01da 798	1 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < 𝑈)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 {crab 3415 ⊆ wss 3926 ∅c0 4308 ifcif 4500 class class class wbr 5119 ‘cfv 6531 (class class class)co 7405 supcsup 9452 ℂcc 11127 ℝcr 11128 + caddc 11132 ℝ^*cxr 11268 < clt 11269 ≤ cle 11270 − cmin 11466 / cdiv 11894 2c2 12295 ℝ⁺crp 13008 [,]cicc 13365 abscabs 15253 –cn→ccncf 24820

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 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206 ax-pre-sup 11207

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-er 8719 df-map 8842 df-en 8960 df-dom 8961 df-sdom 8962 df-sup 9454 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-div 11895 df-nn 12241 df-2 12303 df-3 12304 df-n0 12502 df-z 12589 df-uz 12853 df-rp 13009 df-icc 13369 df-seq 14020 df-exp 14080 df-cj 15118 df-re 15119 df-im 15120 df-sqrt 15254 df-abs 15255 df-cncf 24822

This theorem is referenced by: ivthlem3 25406

W3C validator