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 25807

Description: Lemma for ivth 25808, 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 4010	. . . . . 6 ⊢ 𝑆 ⊆ (𝐴[,]𝐵)
4		ivth.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5		ivth.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
6		iccssre 13590	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
7	4, 5, 6	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
8	3, 7	sstrid 3924	. . . . 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 25805	. . . . . . 7 ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
16	15	simpld 500	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
17	16	ne0d 4291	. . . . 5 ⊢ (𝜑 → 𝑆 ≠ ∅)
18	15	simprd 501	. . . . . 6 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵)
19		brralrspcev 5169	. . . . . 6 ⊢ ((𝐵 ∈ ℝ ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
20	5, 18, 19	syl2anc 596	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
21	8, 17, 20	suprcld 12310	. . . 4 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ ℝ)
22	1, 21	eqeltrid 2868	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
23	14	simpld 500	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐴) < 𝑈)
24	4, 5, 9, 10, 11, 12, 13, 14, 2, 1	ivthlem2 25806	. . . . . 6 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < 𝑈)
25	12	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → 𝐹 ∈ (𝐷–cn→ℂ))
26	8, 17, 20, 16	suprubd 12309	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < ))
27	26, 1	breqtrrdi 5151	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≤ 𝐶)
28	8, 17, 20	3jca 1146	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
29		suprleub 12313	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
30	28, 5, 29	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
31	18, 30	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ≤ 𝐵)
32	1, 31	eqbrtrid 5144	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ≤ 𝐵)
33		elicc2 13572	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
34	4, 5, 33	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
35	22, 27, 32, 34	mpbir3and 1361	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))
36	11, 35	sseldd 3914	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ 𝐷)
37	36	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → 𝐶 ∈ 𝐷)
38		fveq2 6911	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶))
39	38	eleq1d 2849	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐶) ∈ ℝ))
40	13	ralrimiva 3158	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
41	39, 40, 35	rspcdva 3581	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℝ)
42		difrp 13190	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ ℝ ∧ (𝐹‘𝐶) ∈ ℝ) → (𝑈 < (𝐹‘𝐶) ↔ ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺))
43	9, 41, 42	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (𝑈 < (𝐹‘𝐶) ↔ ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺))
44	43	biimpa 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺)
45		cncfi 25248	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐷–cn→ℂ) ∧ 𝐶 ∈ 𝐷 ∧ ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)))
46	25, 37, 44, 45	syl3anc 1399	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)))
47		ssralv 3982	. . . . . . . . . . . 12 ⊢ ((𝐴[,]𝐵) ⊆ 𝐷 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈))))
48	11, 47	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈))))
49	48	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈))))
50	22	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → 𝐶 ∈ ℝ)
51		ltsubrp 13188	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℝ ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) < 𝐶)
52	50, 51	sylancom 600	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) < 𝐶)
53	52, 1	breqtrdi 5150	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) < sup(𝑆, ℝ, < ))
54	28	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
55		rpre 13159	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ⁺ → 𝑧 ∈ ℝ)
56	55	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → 𝑧 ∈ ℝ)
57	50, 56	resubcld 11774	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) ∈ ℝ)
58		suprlub 12311	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ (𝐶 − 𝑧) ∈ ℝ) → ((𝐶 − 𝑧) < sup(𝑆, ℝ, < ) ↔ ∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦))
59	54, 57, 58	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ((𝐶 − 𝑧) < sup(𝑆, ℝ, < ) ↔ ∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦))
60	53, 59	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦)
61	3	sseli 3909	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝑆 → 𝑦 ∈ (𝐴[,]𝐵))
62	61	ad2antrl 741	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ∈ (𝐴[,]𝐵))
63		simplll 787	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝜑)
64	63, 7	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝐴[,]𝐵) ⊆ ℝ)
65	64, 62	sseldd 3914	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ∈ ℝ)
66	63, 22	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝐶 ∈ ℝ)
67	63, 28	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
68		simprl 783	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ∈ 𝑆)
69		suprub 12308	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ sup(𝑆, ℝ, < ))
70	67, 68, 69	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ≤ sup(𝑆, ℝ, < ))
71	70, 1	breqtrrdi 5151	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ≤ 𝐶)
72	65, 66, 71	abssuble0d 15634	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (abs‘(𝑦 − 𝐶)) = (𝐶 − 𝑦))
73	56	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑧 ∈ ℝ)
74		simprr 785	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝐶 − 𝑧) < 𝑦)
75	66, 73, 65, 74	ltsub23d 11951	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝐶 − 𝑦) < 𝑧)
76	72, 75	eqbrtrd 5131	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (abs‘(𝑦 − 𝐶)) < 𝑧)
77	62, 76, 68	jca32 525	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝑦 ∈ (𝐴[,]𝐵) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)))
78	77	ex 418	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ((𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦) → (𝑦 ∈ (𝐴[,]𝐵) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆))))
79	78	reximdv2 3176	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦 → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)))
80	60, 79	mpd 16	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆))
81		r19.29 3129	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)))
82		pm3.45 634	. . . . . . . . . . . . . . 15 ⊢ (((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → (((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆)))
83	82	imp 412	. . . . . . . . . . . . . 14 ⊢ ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆))
84		fveq2 6911	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
85	84	eleq1d 2849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑦) ∈ ℝ))
86	40	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
87	61	ad2antll 742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ (𝐴[,]𝐵))
88	85, 86, 87	rspcdva 3581	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝑦) ∈ ℝ)
89	41	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝐶) ∈ ℝ)
90	9	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → 𝑈 ∈ ℝ)
91	89, 90	resubcld 11774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((𝐹‘𝐶) − 𝑈) ∈ ℝ)
92	88, 89, 91	absdifltd 15635	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ↔ (((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + ((𝐹‘𝐶) − 𝑈)))))
93	89	recnd 11367	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝐶) ∈ ℂ)
94	90	recnd 11367	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → 𝑈 ∈ ℂ)
95	93, 94	nncand 11704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) = 𝑈)
96	95	breq1d 5116	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) ↔ 𝑈 < (𝐹‘𝑦)))
97	84	breq1d 5116	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑈 ↔ (𝐹‘𝑦) ≤ 𝑈))
98	97, 2	elrab2 3652	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ (𝐴[,]𝐵) ∧ (𝐹‘𝑦) ≤ 𝑈))
99	98	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝑆 → (𝐹‘𝑦) ≤ 𝑈)
100	99	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝑦) ≤ 𝑈)
101	88, 90, 100	lensymd 11491	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝑦))
102	101	pm2.21d 122	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝑈 < (𝐹‘𝑦) → ¬ 𝑈 < (𝐹‘𝐶)))
103	96, 102	sylbid 243	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) → ¬ 𝑈 < (𝐹‘𝐶)))
104	103	adantrd 497	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + ((𝐹‘𝐶) − 𝑈))) → ¬ 𝑈 < (𝐹‘𝐶)))
105	92, 104	sylbid 243	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) → ¬ 𝑈 < (𝐹‘𝐶)))
106	105	expr 462	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝑦 ∈ 𝑆 → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) → ¬ 𝑈 < (𝐹‘𝐶))))
107	106	impcomd 417	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆) → ¬ 𝑈 < (𝐹‘𝐶)))
108	107	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆) → ¬ 𝑈 < (𝐹‘𝐶)))
109	83, 108	syl5 35	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝐶)))
110	109	rexlimdva 3167	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝐶)))
111	81, 110	syl5 35	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝐶)))
112	80, 111	mpan2d 707	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ¬ 𝑈 < (𝐹‘𝐶)))
113	49, 112	syld 48	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ¬ 𝑈 < (𝐹‘𝐶)))
114	113	rexlimdva 3167	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → (∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ¬ 𝑈 < (𝐹‘𝐶)))
115	46, 114	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → ¬ 𝑈 < (𝐹‘𝐶))
116	115	pm2.01da 811	. . . . . 6 ⊢ (𝜑 → ¬ 𝑈 < (𝐹‘𝐶))
117	41, 9	lttri3d 11480	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝐶) = 𝑈 ↔ (¬ (𝐹‘𝐶) < 𝑈 ∧ ¬ 𝑈 < (𝐹‘𝐶))))
118	24, 116, 117	mpbir2and 726	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐶) = 𝑈)
119	23, 118	breqtrrd 5137	. . . 4 ⊢ (𝜑 → (𝐹‘𝐴) < (𝐹‘𝐶))
120	41	ltnrd 11474	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < (𝐹‘𝐶))
121		fveq2 6911	. . . . . . . . . 10 ⊢ (𝐶 = 𝐴 → (𝐹‘𝐶) = (𝐹‘𝐴))
122	121	breq1d 5116	. . . . . . . . 9 ⊢ (𝐶 = 𝐴 → ((𝐹‘𝐶) < (𝐹‘𝐶) ↔ (𝐹‘𝐴) < (𝐹‘𝐶)))
123	122	notbid 321	. . . . . . . 8 ⊢ (𝐶 = 𝐴 → (¬ (𝐹‘𝐶) < (𝐹‘𝐶) ↔ ¬ (𝐹‘𝐴) < (𝐹‘𝐶)))
124	120, 123	syl5ibcom 248	. . . . . . 7 ⊢ (𝜑 → (𝐶 = 𝐴 → ¬ (𝐹‘𝐴) < (𝐹‘𝐶)))
125	124	necon2ad 2974	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝐴) < (𝐹‘𝐶) → 𝐶 ≠ 𝐴))
126	125, 27	jctild 535	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝐴) < (𝐹‘𝐶) → (𝐴 ≤ 𝐶 ∧ 𝐶 ≠ 𝐴)))
127	4, 22	ltlend 11485	. . . . 5 ⊢ (𝜑 → (𝐴 < 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐶 ≠ 𝐴)))
128	126, 127	sylibrd 262	. . . 4 ⊢ (𝜑 → ((𝐹‘𝐴) < (𝐹‘𝐶) → 𝐴 < 𝐶))
129	119, 128	mpd 16	. . 3 ⊢ (𝜑 → 𝐴 < 𝐶)
130	14	simprd 501	. . . . 5 ⊢ (𝜑 → 𝑈 < (𝐹‘𝐵))
131	118, 130	eqbrtrd 5131	. . . 4 ⊢ (𝜑 → (𝐹‘𝐶) < (𝐹‘𝐵))
132		fveq2 6911	. . . . . . . . . 10 ⊢ (𝐵 = 𝐶 → (𝐹‘𝐵) = (𝐹‘𝐶))
133	132	breq2d 5118	. . . . . . . . 9 ⊢ (𝐵 = 𝐶 → ((𝐹‘𝐶) < (𝐹‘𝐵) ↔ (𝐹‘𝐶) < (𝐹‘𝐶)))
134	133	notbid 321	. . . . . . . 8 ⊢ (𝐵 = 𝐶 → (¬ (𝐹‘𝐶) < (𝐹‘𝐵) ↔ ¬ (𝐹‘𝐶) < (𝐹‘𝐶)))
135	120, 134	syl5ibrcom 250	. . . . . . 7 ⊢ (𝜑 → (𝐵 = 𝐶 → ¬ (𝐹‘𝐶) < (𝐹‘𝐵)))
136	135	necon2ad 2974	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐵 ≠ 𝐶))
137	136, 32	jctild 535	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
138	22, 5	ltlend 11485	. . . . 5 ⊢ (𝜑 → (𝐶 < 𝐵 ↔ (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
139	137, 138	sylibrd 262	. . . 4 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵))
140	131, 139	mpd 16	. . 3 ⊢ (𝜑 → 𝐶 < 𝐵)
141	4	rexrd 11389	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
142	5	rexrd 11389	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
143		elioo2 13547	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
144	141, 142, 143	syl2anc 596	. . 3 ⊢ (𝜑 → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
145	22, 129, 140, 144	mpbir3and 1361	. 2 ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))
146	145, 118	jca 521	1 ⊢ (𝜑 → (𝐶 ∈ (𝐴(,)𝐵) ∧ (𝐹‘𝐶) = 𝑈))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 {crab 3416 ⊆ wss 3900 ∅c0 4281 class class class wbr 5106 ‘cfv 6561 (class class class)co 7446 supcsup 9462 ℂcc 11228 ℝcr 11229 + caddc 11233 ℝ^*cxr 11372 < clt 11373 ≤ cle 11374 − cmin 11571 ℝ⁺crp 13150 (,)cioo 13506 [,]cicc 13509 abscabs 15433 –cn→ccncf 25230

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307 ax-pre-sup 11308

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-om 7905 df-1st 8028 df-2nd 8029 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-er 8748 df-map 8880 df-en 9005 df-dom 9006 df-sdom 9007 df-sup 9464 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-div 12004 df-nn 12366 df-2 12435 df-3 12436 df-n0 12637 df-z 12724 df-uz 12996 df-rp 13151 df-ioo 13510 df-icc 13513 df-seq 14175 df-exp 14235 df-cj 15298 df-re 15299 df-im 15300 df-sqrt 15434 df-abs 15435 df-cncf 25232

This theorem is used by: ivth 25808

W3C validator