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 24522

Description: Lemma for ivth 24523, 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 4011	. . . . . 6 ⊢ 𝑆 ⊆ (𝐴[,]𝐵)
4		ivth.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5		ivth.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
6		iccssre 13090	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
7	4, 5, 6	syl2anc 583	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
8	3, 7	sstrid 3928	. . . . 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 24520	. . . . . . 7 ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
16	15	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
17	16	ne0d 4266	. . . . 5 ⊢ (𝜑 → 𝑆 ≠ ∅)
18	15	simprd 495	. . . . . 6 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵)
19		brralrspcev 5130	. . . . . 6 ⊢ ((𝐵 ∈ ℝ ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
20	5, 18, 19	syl2anc 583	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
21	8, 17, 20	suprcld 11868	. . . 4 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ ℝ)
22	1, 21	eqeltrid 2843	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
23	14	simpld 494	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐴) < 𝑈)
24	4, 5, 9, 10, 11, 12, 13, 14, 2, 1	ivthlem2 24521	. . . . . 6 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < 𝑈)
25	12	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → 𝐹 ∈ (𝐷–cn→ℂ))
26	8, 17, 20, 16	suprubd 11867	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < ))
27	26, 1	breqtrrdi 5112	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≤ 𝐶)
28	8, 17, 20	3jca 1126	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
29		suprleub 11871	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
30	28, 5, 29	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
31	18, 30	mpbird 256	. . . . . . . . . . . . 13 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ≤ 𝐵)
32	1, 31	eqbrtrid 5105	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ≤ 𝐵)
33		elicc2 13073	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
34	4, 5, 33	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
35	22, 27, 32, 34	mpbir3and 1340	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))
36	11, 35	sseldd 3918	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ 𝐷)
37	36	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → 𝐶 ∈ 𝐷)
38		fveq2 6756	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶))
39	38	eleq1d 2823	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐶) ∈ ℝ))
40	13	ralrimiva 3107	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
41	39, 40, 35	rspcdva 3554	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℝ)
42		difrp 12697	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ ℝ ∧ (𝐹‘𝐶) ∈ ℝ) → (𝑈 < (𝐹‘𝐶) ↔ ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺))
43	9, 41, 42	syl2anc 583	. . . . . . . . . 10 ⊢ (𝜑 → (𝑈 < (𝐹‘𝐶) ↔ ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺))
44	43	biimpa 476	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺)
45		cncfi 23963	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐷–cn→ℂ) ∧ 𝐶 ∈ 𝐷 ∧ ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)))
46	25, 37, 44, 45	syl3anc 1369	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)))
47		ssralv 3983	. . . . . . . . . . . 12 ⊢ ((𝐴[,]𝐵) ⊆ 𝐷 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈))))
48	11, 47	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈))))
49	48	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈))))
50	22	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 ∈ ℝ)
51		ltsubrp 12695	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℝ ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) < 𝐶)
52	50, 51	sylancom 587	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) < 𝐶)
53	52, 1	breqtrdi 5111	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) < sup(𝑆, ℝ, < ))
54	28	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
55		rpre 12667	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ⁺ → 𝑧 ∈ ℝ)
56	55	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → 𝑧 ∈ ℝ)
57	50, 56	resubcld 11333	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) ∈ ℝ)
58		suprlub 11869	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ (𝐶 − 𝑧) ∈ ℝ) → ((𝐶 − 𝑧) < sup(𝑆, ℝ, < ) ↔ ∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦))
59	54, 57, 58	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ((𝐶 − 𝑧) < sup(𝑆, ℝ, < ) ↔ ∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦))
60	53, 59	mpbid 231	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦)
61	3	sseli 3913	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝑆 → 𝑦 ∈ (𝐴[,]𝐵))
62	61	ad2antrl 724	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ∈ (𝐴[,]𝐵))
63		simplll 771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝜑)
64	63, 7	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝐴[,]𝐵) ⊆ ℝ)
65	64, 62	sseldd 3918	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ∈ ℝ)
66	63, 22	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝐶 ∈ ℝ)
67	63, 28	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
68		simprl 767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ∈ 𝑆)
69		suprub 11866	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ sup(𝑆, ℝ, < ))
70	67, 68, 69	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ≤ sup(𝑆, ℝ, < ))
71	70, 1	breqtrrdi 5112	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ≤ 𝐶)
72	65, 66, 71	abssuble0d 15072	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (abs‘(𝑦 − 𝐶)) = (𝐶 − 𝑦))
73	56	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑧 ∈ ℝ)
74		simprr 769	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝐶 − 𝑧) < 𝑦)
75	66, 73, 65, 74	ltsub23d 11510	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝐶 − 𝑦) < 𝑧)
76	72, 75	eqbrtrd 5092	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (abs‘(𝑦 − 𝐶)) < 𝑧)
77	62, 76, 68	jca32 515	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝑦 ∈ (𝐴[,]𝐵) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)))
78	77	ex 412	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ((𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦) → (𝑦 ∈ (𝐴[,]𝐵) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆))))
79	78	reximdv2 3198	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦 → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)))
80	60, 79	mpd 15	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆))
81		r19.29 3183	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)))
82		pm3.45 621	. . . . . . . . . . . . . . 15 ⊢ (((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → (((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆)))
83	82	imp 406	. . . . . . . . . . . . . 14 ⊢ ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆))
84		fveq2 6756	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
85	84	eleq1d 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑦) ∈ ℝ))
86	40	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
87	61	ad2antll 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ (𝐴[,]𝐵))
88	85, 86, 87	rspcdva 3554	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝑦) ∈ ℝ)
89	41	ad2antrr 722	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝐶) ∈ ℝ)
90	9	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → 𝑈 ∈ ℝ)
91	89, 90	resubcld 11333	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((𝐹‘𝐶) − 𝑈) ∈ ℝ)
92	88, 89, 91	absdifltd 15073	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ↔ (((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + ((𝐹‘𝐶) − 𝑈)))))
93	89	recnd 10934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝐶) ∈ ℂ)
94	90	recnd 10934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → 𝑈 ∈ ℂ)
95	93, 94	nncand 11267	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) = 𝑈)
96	95	breq1d 5080	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) ↔ 𝑈 < (𝐹‘𝑦)))
97	84	breq1d 5080	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑈 ↔ (𝐹‘𝑦) ≤ 𝑈))
98	97, 2	elrab2 3620	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ (𝐴[,]𝐵) ∧ (𝐹‘𝑦) ≤ 𝑈))
99	98	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝑆 → (𝐹‘𝑦) ≤ 𝑈)
100	99	ad2antll 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝑦) ≤ 𝑈)
101	88, 90, 100	lensymd 11056	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝑦))
102	101	pm2.21d 121	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝑈 < (𝐹‘𝑦) → ¬ 𝑈 < (𝐹‘𝐶)))
103	96, 102	sylbid 239	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) → ¬ 𝑈 < (𝐹‘𝐶)))
104	103	adantrd 491	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + ((𝐹‘𝐶) − 𝑈))) → ¬ 𝑈 < (𝐹‘𝐶)))
105	92, 104	sylbid 239	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) → ¬ 𝑈 < (𝐹‘𝐶)))
106	105	expr 456	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝑦 ∈ 𝑆 → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) → ¬ 𝑈 < (𝐹‘𝐶))))
107	106	impcomd 411	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆) → ¬ 𝑈 < (𝐹‘𝐶)))
108	107	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆) → ¬ 𝑈 < (𝐹‘𝐶)))
109	83, 108	syl5 34	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝐶)))
110	109	rexlimdva 3212	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝐶)))
111	81, 110	syl5 34	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝐶)))
112	80, 111	mpan2d 690	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ¬ 𝑈 < (𝐹‘𝐶)))
113	49, 112	syld 47	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ¬ 𝑈 < (𝐹‘𝐶)))
114	113	rexlimdva 3212	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → (∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ¬ 𝑈 < (𝐹‘𝐶)))
115	46, 114	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → ¬ 𝑈 < (𝐹‘𝐶))
116	115	pm2.01da 795	. . . . . 6 ⊢ (𝜑 → ¬ 𝑈 < (𝐹‘𝐶))
117	41, 9	lttri3d 11045	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝐶) = 𝑈 ↔ (¬ (𝐹‘𝐶) < 𝑈 ∧ ¬ 𝑈 < (𝐹‘𝐶))))
118	24, 116, 117	mpbir2and 709	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐶) = 𝑈)
119	23, 118	breqtrrd 5098	. . . 4 ⊢ (𝜑 → (𝐹‘𝐴) < (𝐹‘𝐶))
120	41	ltnrd 11039	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < (𝐹‘𝐶))
121		fveq2 6756	. . . . . . . . . 10 ⊢ (𝐶 = 𝐴 → (𝐹‘𝐶) = (𝐹‘𝐴))
122	121	breq1d 5080	. . . . . . . . 9 ⊢ (𝐶 = 𝐴 → ((𝐹‘𝐶) < (𝐹‘𝐶) ↔ (𝐹‘𝐴) < (𝐹‘𝐶)))
123	122	notbid 317	. . . . . . . 8 ⊢ (𝐶 = 𝐴 → (¬ (𝐹‘𝐶) < (𝐹‘𝐶) ↔ ¬ (𝐹‘𝐴) < (𝐹‘𝐶)))
124	120, 123	syl5ibcom 244	. . . . . . 7 ⊢ (𝜑 → (𝐶 = 𝐴 → ¬ (𝐹‘𝐴) < (𝐹‘𝐶)))
125	124	necon2ad 2957	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝐴) < (𝐹‘𝐶) → 𝐶 ≠ 𝐴))
126	125, 27	jctild 525	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝐴) < (𝐹‘𝐶) → (𝐴 ≤ 𝐶 ∧ 𝐶 ≠ 𝐴)))
127	4, 22	ltlend 11050	. . . . 5 ⊢ (𝜑 → (𝐴 < 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐶 ≠ 𝐴)))
128	126, 127	sylibrd 258	. . . 4 ⊢ (𝜑 → ((𝐹‘𝐴) < (𝐹‘𝐶) → 𝐴 < 𝐶))
129	119, 128	mpd 15	. . 3 ⊢ (𝜑 → 𝐴 < 𝐶)
130	14	simprd 495	. . . . 5 ⊢ (𝜑 → 𝑈 < (𝐹‘𝐵))
131	118, 130	eqbrtrd 5092	. . . 4 ⊢ (𝜑 → (𝐹‘𝐶) < (𝐹‘𝐵))
132		fveq2 6756	. . . . . . . . . 10 ⊢ (𝐵 = 𝐶 → (𝐹‘𝐵) = (𝐹‘𝐶))
133	132	breq2d 5082	. . . . . . . . 9 ⊢ (𝐵 = 𝐶 → ((𝐹‘𝐶) < (𝐹‘𝐵) ↔ (𝐹‘𝐶) < (𝐹‘𝐶)))
134	133	notbid 317	. . . . . . . 8 ⊢ (𝐵 = 𝐶 → (¬ (𝐹‘𝐶) < (𝐹‘𝐵) ↔ ¬ (𝐹‘𝐶) < (𝐹‘𝐶)))
135	120, 134	syl5ibrcom 246	. . . . . . 7 ⊢ (𝜑 → (𝐵 = 𝐶 → ¬ (𝐹‘𝐶) < (𝐹‘𝐵)))
136	135	necon2ad 2957	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐵 ≠ 𝐶))
137	136, 32	jctild 525	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
138	22, 5	ltlend 11050	. . . . 5 ⊢ (𝜑 → (𝐶 < 𝐵 ↔ (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
139	137, 138	sylibrd 258	. . . 4 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵))
140	131, 139	mpd 15	. . 3 ⊢ (𝜑 → 𝐶 < 𝐵)
141	4	rexrd 10956	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
142	5	rexrd 10956	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
143		elioo2 13049	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
144	141, 142, 143	syl2anc 583	. . 3 ⊢ (𝜑 → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
145	22, 129, 140, 144	mpbir3and 1340	. 2 ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))
146	145, 118	jca 511	1 ⊢ (𝜑 → (𝐶 ∈ (𝐴(,)𝐵) ∧ (𝐹‘𝐶) = 𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 {crab 3067 ⊆ wss 3883 ∅c0 4253 class class class wbr 5070 ‘cfv 6418 (class class class)co 7255 supcsup 9129 ℂcc 10800 ℝcr 10801 + caddc 10805 ℝ^*cxr 10939 < clt 10940 ≤ cle 10941 − cmin 11135 ℝ⁺crp 12659 (,)cioo 13008 [,]cicc 13011 abscabs 14873 –cn→ccncf 23945

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-sup 9131 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-rp 12660 df-ioo 13012 df-icc 13015 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-cncf 23947

This theorem is referenced by: ivth 24523

W3C validator