ivthlem3 - Metamath Proof Explorer

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

Theorem ivthlem3 24723

Description: Lemma for ivth 24724, the intermediate value theorem. Show that (𝐹‘𝐶) cannot be greater than 𝑈, and so establish the existence of a root of the function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised 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
ivthlem3	⊢ (𝜑 → (𝐶 ∈ (𝐴(,)𝐵) ∧ (𝐹‘𝐶) = 𝑈))

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

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

Step	Hyp	Ref	Expression
1		ivth.11	. . . 4 ⊢ 𝐶 = sup(𝑆, ℝ, < )
2		ivth.10	. . . . . . 7 ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈}
3	2	ssrab3 4032	. . . . . 6 ⊢ 𝑆 ⊆ (𝐴[,]𝐵)
4		ivth.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5		ivth.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
6		iccssre 13267	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
7	4, 5, 6	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
8	3, 7	sstrid 3947	. . . . 5 ⊢ (𝜑 → 𝑆 ⊆ ℝ)
9		ivth.3	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ ℝ)
10		ivth.4	. . . . . . . 8 ⊢ (𝜑 → 𝐴 < 𝐵)
11		ivth.5	. . . . . . . 8 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
12		ivth.7	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))
13		ivth.8	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)
14		ivth.9	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))
15	4, 5, 9, 10, 11, 12, 13, 14, 2	ivthlem1 24721	. . . . . . 7 ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
16	15	simpld 496	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
17	16	ne0d 4287	. . . . 5 ⊢ (𝜑 → 𝑆 ≠ ∅)
18	15	simprd 497	. . . . . 6 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵)
19		brralrspcev 5157	. . . . . 6 ⊢ ((𝐵 ∈ ℝ ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
20	5, 18, 19	syl2anc 585	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
21	8, 17, 20	suprcld 12044	. . . 4 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ ℝ)
22	1, 21	eqeltrid 2842	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
23	14	simpld 496	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐴) < 𝑈)
24	4, 5, 9, 10, 11, 12, 13, 14, 2, 1	ivthlem2 24722	. . . . . 6 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < 𝑈)
25	12	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → 𝐹 ∈ (𝐷–cn→ℂ))
26	8, 17, 20, 16	suprubd 12043	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < ))
27	26, 1	breqtrrdi 5139	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≤ 𝐶)
28	8, 17, 20	3jca 1128	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
29		suprleub 12047	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
30	28, 5, 29	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
31	18, 30	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ≤ 𝐵)
32	1, 31	eqbrtrid 5132	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ≤ 𝐵)
33		elicc2 13250	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
34	4, 5, 33	syl2anc 585	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
35	22, 27, 32, 34	mpbir3and 1342	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))
36	11, 35	sseldd 3937	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ 𝐷)
37	36	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → 𝐶 ∈ 𝐷)
38		fveq2 6830	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶))
39	38	eleq1d 2822	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐶) ∈ ℝ))
40	13	ralrimiva 3140	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
41	39, 40, 35	rspcdva 3575	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℝ)
42		difrp 12874	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ ℝ ∧ (𝐹‘𝐶) ∈ ℝ) → (𝑈 < (𝐹‘𝐶) ↔ ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺))
43	9, 41, 42	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → (𝑈 < (𝐹‘𝐶) ↔ ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺))
44	43	biimpa 478	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺)
45		cncfi 24163	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐷–cn→ℂ) ∧ 𝐶 ∈ 𝐷 ∧ ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)))
46	25, 37, 44, 45	syl3anc 1371	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)))
47		ssralv 4002	. . . . . . . . . . . 12 ⊢ ((𝐴[,]𝐵) ⊆ 𝐷 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈))))
48	11, 47	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈))))
49	48	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈))))
50	22	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 ∈ ℝ)
51		ltsubrp 12872	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℝ ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) < 𝐶)
52	50, 51	sylancom 589	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) < 𝐶)
53	52, 1	breqtrdi 5138	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) < sup(𝑆, ℝ, < ))
54	28	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
55		rpre 12844	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ⁺ → 𝑧 ∈ ℝ)
56	55	adantl 483	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → 𝑧 ∈ ℝ)
57	50, 56	resubcld 11509	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) ∈ ℝ)
58		suprlub 12045	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ (𝐶 − 𝑧) ∈ ℝ) → ((𝐶 − 𝑧) < sup(𝑆, ℝ, < ) ↔ ∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦))
59	54, 57, 58	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ((𝐶 − 𝑧) < sup(𝑆, ℝ, < ) ↔ ∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦))
60	53, 59	mpbid 231	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦)
61	3	sseli 3932	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝑆 → 𝑦 ∈ (𝐴[,]𝐵))
62	61	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ∈ (𝐴[,]𝐵))
63		simplll 773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝜑)
64	63, 7	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝐴[,]𝐵) ⊆ ℝ)
65	64, 62	sseldd 3937	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ∈ ℝ)
66	63, 22	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝐶 ∈ ℝ)
67	63, 28	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
68		simprl 769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ∈ 𝑆)
69		suprub 12042	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ sup(𝑆, ℝ, < ))
70	67, 68, 69	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ≤ sup(𝑆, ℝ, < ))
71	70, 1	breqtrrdi 5139	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ≤ 𝐶)
72	65, 66, 71	abssuble0d 15244	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (abs‘(𝑦 − 𝐶)) = (𝐶 − 𝑦))
73	56	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑧 ∈ ℝ)
74		simprr 771	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝐶 − 𝑧) < 𝑦)
75	66, 73, 65, 74	ltsub23d 11686	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝐶 − 𝑦) < 𝑧)
76	72, 75	eqbrtrd 5119	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (abs‘(𝑦 − 𝐶)) < 𝑧)
77	62, 76, 68	jca32 517	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝑦 ∈ (𝐴[,]𝐵) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)))
78	77	ex 414	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ((𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦) → (𝑦 ∈ (𝐴[,]𝐵) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆))))
79	78	reximdv2 3158	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦 → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)))
80	60, 79	mpd 15	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆))
81		r19.29 3114	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)))
82		pm3.45 623	. . . . . . . . . . . . . . 15 ⊢ (((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → (((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆)))
83	82	imp 408	. . . . . . . . . . . . . 14 ⊢ ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆))
84		fveq2 6830	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
85	84	eleq1d 2822	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑦) ∈ ℝ))
86	40	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
87	61	ad2antll 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ (𝐴[,]𝐵))
88	85, 86, 87	rspcdva 3575	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝑦) ∈ ℝ)
89	41	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝐶) ∈ ℝ)
90	9	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → 𝑈 ∈ ℝ)
91	89, 90	resubcld 11509	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((𝐹‘𝐶) − 𝑈) ∈ ℝ)
92	88, 89, 91	absdifltd 15245	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ↔ (((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + ((𝐹‘𝐶) − 𝑈)))))
93	89	recnd 11109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝐶) ∈ ℂ)
94	90	recnd 11109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → 𝑈 ∈ ℂ)
95	93, 94	nncand 11443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) = 𝑈)
96	95	breq1d 5107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) ↔ 𝑈 < (𝐹‘𝑦)))
97	84	breq1d 5107	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑈 ↔ (𝐹‘𝑦) ≤ 𝑈))
98	97, 2	elrab2 3641	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ (𝐴[,]𝐵) ∧ (𝐹‘𝑦) ≤ 𝑈))
99	98	simprbi 498	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝑆 → (𝐹‘𝑦) ≤ 𝑈)
100	99	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝑦) ≤ 𝑈)
101	88, 90, 100	lensymd 11232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝑦))
102	101	pm2.21d 121	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝑈 < (𝐹‘𝑦) → ¬ 𝑈 < (𝐹‘𝐶)))
103	96, 102	sylbid 239	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) → ¬ 𝑈 < (𝐹‘𝐶)))
104	103	adantrd 493	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + ((𝐹‘𝐶) − 𝑈))) → ¬ 𝑈 < (𝐹‘𝐶)))
105	92, 104	sylbid 239	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) → ¬ 𝑈 < (𝐹‘𝐶)))
106	105	expr 458	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝑦 ∈ 𝑆 → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) → ¬ 𝑈 < (𝐹‘𝐶))))
107	106	impcomd 413	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆) → ¬ 𝑈 < (𝐹‘𝐶)))
108	107	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆) → ¬ 𝑈 < (𝐹‘𝐶)))
109	83, 108	syl5 34	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝐶)))
110	109	rexlimdva 3149	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝐶)))
111	81, 110	syl5 34	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝐶)))
112	80, 111	mpan2d 692	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ¬ 𝑈 < (𝐹‘𝐶)))
113	49, 112	syld 47	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ¬ 𝑈 < (𝐹‘𝐶)))
114	113	rexlimdva 3149	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → (∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ¬ 𝑈 < (𝐹‘𝐶)))
115	46, 114	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → ¬ 𝑈 < (𝐹‘𝐶))
116	115	pm2.01da 797	. . . . . 6 ⊢ (𝜑 → ¬ 𝑈 < (𝐹‘𝐶))
117	41, 9	lttri3d 11221	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝐶) = 𝑈 ↔ (¬ (𝐹‘𝐶) < 𝑈 ∧ ¬ 𝑈 < (𝐹‘𝐶))))
118	24, 116, 117	mpbir2and 711	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐶) = 𝑈)
119	23, 118	breqtrrd 5125	. . . 4 ⊢ (𝜑 → (𝐹‘𝐴) < (𝐹‘𝐶))
120	41	ltnrd 11215	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < (𝐹‘𝐶))
121		fveq2 6830	. . . . . . . . . 10 ⊢ (𝐶 = 𝐴 → (𝐹‘𝐶) = (𝐹‘𝐴))
122	121	breq1d 5107	. . . . . . . . 9 ⊢ (𝐶 = 𝐴 → ((𝐹‘𝐶) < (𝐹‘𝐶) ↔ (𝐹‘𝐴) < (𝐹‘𝐶)))
123	122	notbid 318	. . . . . . . 8 ⊢ (𝐶 = 𝐴 → (¬ (𝐹‘𝐶) < (𝐹‘𝐶) ↔ ¬ (𝐹‘𝐴) < (𝐹‘𝐶)))
124	120, 123	syl5ibcom 245	. . . . . . 7 ⊢ (𝜑 → (𝐶 = 𝐴 → ¬ (𝐹‘𝐴) < (𝐹‘𝐶)))
125	124	necon2ad 2956	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝐴) < (𝐹‘𝐶) → 𝐶 ≠ 𝐴))
126	125, 27	jctild 527	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝐴) < (𝐹‘𝐶) → (𝐴 ≤ 𝐶 ∧ 𝐶 ≠ 𝐴)))
127	4, 22	ltlend 11226	. . . . 5 ⊢ (𝜑 → (𝐴 < 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐶 ≠ 𝐴)))
128	126, 127	sylibrd 259	. . . 4 ⊢ (𝜑 → ((𝐹‘𝐴) < (𝐹‘𝐶) → 𝐴 < 𝐶))
129	119, 128	mpd 15	. . 3 ⊢ (𝜑 → 𝐴 < 𝐶)
130	14	simprd 497	. . . . 5 ⊢ (𝜑 → 𝑈 < (𝐹‘𝐵))
131	118, 130	eqbrtrd 5119	. . . 4 ⊢ (𝜑 → (𝐹‘𝐶) < (𝐹‘𝐵))
132		fveq2 6830	. . . . . . . . . 10 ⊢ (𝐵 = 𝐶 → (𝐹‘𝐵) = (𝐹‘𝐶))
133	132	breq2d 5109	. . . . . . . . 9 ⊢ (𝐵 = 𝐶 → ((𝐹‘𝐶) < (𝐹‘𝐵) ↔ (𝐹‘𝐶) < (𝐹‘𝐶)))
134	133	notbid 318	. . . . . . . 8 ⊢ (𝐵 = 𝐶 → (¬ (𝐹‘𝐶) < (𝐹‘𝐵) ↔ ¬ (𝐹‘𝐶) < (𝐹‘𝐶)))
135	120, 134	syl5ibrcom 247	. . . . . . 7 ⊢ (𝜑 → (𝐵 = 𝐶 → ¬ (𝐹‘𝐶) < (𝐹‘𝐵)))
136	135	necon2ad 2956	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐵 ≠ 𝐶))
137	136, 32	jctild 527	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
138	22, 5	ltlend 11226	. . . . 5 ⊢ (𝜑 → (𝐶 < 𝐵 ↔ (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
139	137, 138	sylibrd 259	. . . 4 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵))
140	131, 139	mpd 15	. . 3 ⊢ (𝜑 → 𝐶 < 𝐵)
141	4	rexrd 11131	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
142	5	rexrd 11131	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
143		elioo2 13226	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
144	141, 142, 143	syl2anc 585	. . 3 ⊢ (𝜑 → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
145	22, 129, 140, 144	mpbir3and 1342	. 2 ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))
146	145, 118	jca 513	1 ⊢ (𝜑 → (𝐶 ∈ (𝐴(,)𝐵) ∧ (𝐹‘𝐶) = 𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 {crab 3404 ⊆ wss 3902 ∅c0 4274 class class class wbr 5097 ‘cfv 6484 (class class class)co 7342 supcsup 9302 ℂcc 10975 ℝcr 10976 + caddc 10980 ℝ^*cxr 11114 < clt 11115 ≤ cle 11116 − cmin 11311 ℝ⁺crp 12836 (,)cioo 13185 [,]cicc 13188 abscabs 15045 –cn→ccncf 24145

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-sep 5248 ax-nul 5255 ax-pow 5313 ax-pr 5377 ax-un 7655 ax-cnex 11033 ax-resscn 11034 ax-1cn 11035 ax-icn 11036 ax-addcl 11037 ax-addrcl 11038 ax-mulcl 11039 ax-mulrcl 11040 ax-mulcom 11041 ax-addass 11042 ax-mulass 11043 ax-distr 11044 ax-i2m1 11045 ax-1ne0 11046 ax-1rid 11047 ax-rnegex 11048 ax-rrecex 11049 ax-cnre 11050 ax-pre-lttri 11051 ax-pre-lttrn 11052 ax-pre-ltadd 11053 ax-pre-mulgt0 11054 ax-pre-sup 11055

This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3444 df-sbc 3732 df-csb 3848 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3921 df-nul 4275 df-if 4479 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4858 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5181 df-tr 5215 df-id 5523 df-eprel 5529 df-po 5537 df-so 5538 df-fr 5580 df-we 5582 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6243 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6436 df-fun 6486 df-fn 6487 df-f 6488 df-f1 6489 df-fo 6490 df-f1o 6491 df-fv 6492 df-riota 7298 df-ov 7345 df-oprab 7346 df-mpo 7347 df-om 7786 df-1st 7904 df-2nd 7905 df-frecs 8172 df-wrecs 8203 df-recs 8277 df-rdg 8316 df-er 8574 df-map 8693 df-en 8810 df-dom 8811 df-sdom 8812 df-sup 9304 df-pnf 11117 df-mnf 11118 df-xr 11119 df-ltxr 11120 df-le 11121 df-sub 11313 df-neg 11314 df-div 11739 df-nn 12080 df-2 12142 df-3 12143 df-n0 12340 df-z 12426 df-uz 12689 df-rp 12837 df-ioo 13189 df-icc 13192 df-seq 13828 df-exp 13889 df-cj 14910 df-re 14911 df-im 14912 df-sqrt 15046 df-abs 15047 df-cncf 24147

This theorem is referenced by: ivth 24724

W3C validator