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 25473

Description: Lemma for ivth 25474, 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 4079	. . . . . 6 ⊢ 𝑆 ⊆ (𝐴[,]𝐵)
4		ivth.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5		ivth.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
6		iccssre 13460	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
7	4, 5, 6	syl2anc 582	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
8	3, 7	sstrid 3991	. . . . 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 25471	. . . . . . 7 ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
16	15	simpld 493	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
17	16	ne0d 4338	. . . . 5 ⊢ (𝜑 → 𝑆 ≠ ∅)
18	15	simprd 494	. . . . . 6 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵)
19		brralrspcev 5213	. . . . . 6 ⊢ ((𝐵 ∈ ℝ ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
20	5, 18, 19	syl2anc 582	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)
21	8, 17, 20	suprcld 12229	. . . 4 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ ℝ)
22	1, 21	eqeltrid 2830	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
23	14	simpld 493	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐴) < 𝑈)
24	4, 5, 9, 10, 11, 12, 13, 14, 2, 1	ivthlem2 25472	. . . . . 6 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < 𝑈)
25	12	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → 𝐹 ∈ (𝐷–cn→ℂ))
26	8, 17, 20, 16	suprubd 12228	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < ))
27	26, 1	breqtrrdi 5195	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≤ 𝐶)
28	8, 17, 20	3jca 1125	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
29		suprleub 12232	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
30	28, 5, 29	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
31	18, 30	mpbird 256	. . . . . . . . . . . . 13 ⊢ (𝜑 → sup(𝑆, ℝ, < ) ≤ 𝐵)
32	1, 31	eqbrtrid 5188	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ≤ 𝐵)
33		elicc2 13443	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
34	4, 5, 33	syl2anc 582	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
35	22, 27, 32, 34	mpbir3and 1339	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))
36	11, 35	sseldd 3980	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ 𝐷)
37	36	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → 𝐶 ∈ 𝐷)
38		fveq2 6901	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶))
39	38	eleq1d 2811	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐶) ∈ ℝ))
40	13	ralrimiva 3136	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
41	39, 40, 35	rspcdva 3609	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℝ)
42		difrp 13066	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ ℝ ∧ (𝐹‘𝐶) ∈ ℝ) → (𝑈 < (𝐹‘𝐶) ↔ ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺))
43	9, 41, 42	syl2anc 582	. . . . . . . . . 10 ⊢ (𝜑 → (𝑈 < (𝐹‘𝐶) ↔ ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺))
44	43	biimpa 475	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺)
45		cncfi 24905	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐷–cn→ℂ) ∧ 𝐶 ∈ 𝐷 ∧ ((𝐹‘𝐶) − 𝑈) ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)))
46	25, 37, 44, 45	syl3anc 1368	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → ∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)))
47		ssralv 4048	. . . . . . . . . . . 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 13064	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℝ ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) < 𝐶)
52	50, 51	sylancom 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) < 𝐶)
53	52, 1	breqtrdi 5194	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) < sup(𝑆, ℝ, < ))
54	28	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
55		rpre 13036	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ⁺ → 𝑧 ∈ ℝ)
56	55	adantl 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → 𝑧 ∈ ℝ)
57	50, 56	resubcld 11692	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝐶 − 𝑧) ∈ ℝ)
58		suprlub 12230	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ (𝐶 − 𝑧) ∈ ℝ) → ((𝐶 − 𝑧) < sup(𝑆, ℝ, < ) ↔ ∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦))
59	54, 57, 58	syl2anc 582	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ((𝐶 − 𝑧) < sup(𝑆, ℝ, < ) ↔ ∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦))
60	53, 59	mpbid 231	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦)
61	3	sseli 3975	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝑆 → 𝑦 ∈ (𝐴[,]𝐵))
62	61	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ∈ (𝐴[,]𝐵))
63		simplll 773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝜑)
64	63, 7	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝐴[,]𝐵) ⊆ ℝ)
65	64, 62	sseldd 3980	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ∈ ℝ)
66	63, 22	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝐶 ∈ ℝ)
67	63, 28	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥))
68		simprl 769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ∈ 𝑆)
69		suprub 12227	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ sup(𝑆, ℝ, < ))
70	67, 68, 69	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ≤ sup(𝑆, ℝ, < ))
71	70, 1	breqtrrdi 5195	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑦 ≤ 𝐶)
72	65, 66, 71	abssuble0d 15437	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (abs‘(𝑦 − 𝐶)) = (𝐶 − 𝑦))
73	56	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → 𝑧 ∈ ℝ)
74		simprr 771	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝐶 − 𝑧) < 𝑦)
75	66, 73, 65, 74	ltsub23d 11869	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝐶 − 𝑦) < 𝑧)
76	72, 75	eqbrtrd 5175	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (abs‘(𝑦 − 𝐶)) < 𝑧)
77	62, 76, 68	jca32 514	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦)) → (𝑦 ∈ (𝐴[,]𝐵) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)))
78	77	ex 411	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ((𝑦 ∈ 𝑆 ∧ (𝐶 − 𝑧) < 𝑦) → (𝑦 ∈ (𝐴[,]𝐵) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆))))
79	78	reximdv2 3154	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (∃𝑦 ∈ 𝑆 (𝐶 − 𝑧) < 𝑦 → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)))
80	60, 79	mpd 15	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆))
81		r19.29 3104	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)))
82		pm3.45 620	. . . . . . . . . . . . . . 15 ⊢ (((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → (((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆)))
83	82	imp 405	. . . . . . . . . . . . . 14 ⊢ ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆))
84		fveq2 6901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
85	84	eleq1d 2811	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑦) ∈ ℝ))
86	40	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ)
87	61	ad2antll 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ (𝐴[,]𝐵))
88	85, 86, 87	rspcdva 3609	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝑦) ∈ ℝ)
89	41	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝐶) ∈ ℝ)
90	9	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → 𝑈 ∈ ℝ)
91	89, 90	resubcld 11692	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((𝐹‘𝐶) − 𝑈) ∈ ℝ)
92	88, 89, 91	absdifltd 15438	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ↔ (((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + ((𝐹‘𝐶) − 𝑈)))))
93	89	recnd 11292	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝐶) ∈ ℂ)
94	90	recnd 11292	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → 𝑈 ∈ ℂ)
95	93, 94	nncand 11626	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) = 𝑈)
96	95	breq1d 5163	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) ↔ 𝑈 < (𝐹‘𝑦)))
97	84	breq1d 5163	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑈 ↔ (𝐹‘𝑦) ≤ 𝑈))
98	97, 2	elrab2 3684	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ (𝐴[,]𝐵) ∧ (𝐹‘𝑦) ≤ 𝑈))
99	98	simprbi 495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝑆 → (𝐹‘𝑦) ≤ 𝑈)
100	99	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝐹‘𝑦) ≤ 𝑈)
101	88, 90, 100	lensymd 11415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝑦))
102	101	pm2.21d 121	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (𝑈 < (𝐹‘𝑦) → ¬ 𝑈 < (𝐹‘𝐶)))
103	96, 102	sylbid 239	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → (((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) → ¬ 𝑈 < (𝐹‘𝐶)))
104	103	adantrd 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((((𝐹‘𝐶) − ((𝐹‘𝐶) − 𝑈)) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + ((𝐹‘𝐶) − 𝑈))) → ¬ 𝑈 < (𝐹‘𝐶)))
105	92, 104	sylbid 239	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ (𝑧 ∈ ℝ⁺ ∧ 𝑦 ∈ 𝑆)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) → ¬ 𝑈 < (𝐹‘𝐶)))
106	105	expr 455	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (𝑦 ∈ 𝑆 → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) → ¬ 𝑈 < (𝐹‘𝐶))))
107	106	impcomd 410	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆) → ¬ 𝑈 < (𝐹‘𝐶)))
108	107	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈) ∧ 𝑦 ∈ 𝑆) → ¬ 𝑈 < (𝐹‘𝐶)))
109	83, 108	syl5 34	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝑦 ∈ 𝑆)) → ¬ 𝑈 < (𝐹‘𝐶)))
110	109	rexlimdva 3145	. . . . . . . . . . . 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 3145	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → (∃𝑧 ∈ ℝ⁺ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < ((𝐹‘𝐶) − 𝑈)) → ¬ 𝑈 < (𝐹‘𝐶)))
115	46, 114	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑈 < (𝐹‘𝐶)) → ¬ 𝑈 < (𝐹‘𝐶))
116	115	pm2.01da 797	. . . . . 6 ⊢ (𝜑 → ¬ 𝑈 < (𝐹‘𝐶))
117	41, 9	lttri3d 11404	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝐶) = 𝑈 ↔ (¬ (𝐹‘𝐶) < 𝑈 ∧ ¬ 𝑈 < (𝐹‘𝐶))))
118	24, 116, 117	mpbir2and 711	. . . . 5 ⊢ (𝜑 → (𝐹‘𝐶) = 𝑈)
119	23, 118	breqtrrd 5181	. . . 4 ⊢ (𝜑 → (𝐹‘𝐴) < (𝐹‘𝐶))
120	41	ltnrd 11398	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐹‘𝐶) < (𝐹‘𝐶))
121		fveq2 6901	. . . . . . . . . 10 ⊢ (𝐶 = 𝐴 → (𝐹‘𝐶) = (𝐹‘𝐴))
122	121	breq1d 5163	. . . . . . . . 9 ⊢ (𝐶 = 𝐴 → ((𝐹‘𝐶) < (𝐹‘𝐶) ↔ (𝐹‘𝐴) < (𝐹‘𝐶)))
123	122	notbid 317	. . . . . . . 8 ⊢ (𝐶 = 𝐴 → (¬ (𝐹‘𝐶) < (𝐹‘𝐶) ↔ ¬ (𝐹‘𝐴) < (𝐹‘𝐶)))
124	120, 123	syl5ibcom 244	. . . . . . 7 ⊢ (𝜑 → (𝐶 = 𝐴 → ¬ (𝐹‘𝐴) < (𝐹‘𝐶)))
125	124	necon2ad 2945	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝐴) < (𝐹‘𝐶) → 𝐶 ≠ 𝐴))
126	125, 27	jctild 524	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝐴) < (𝐹‘𝐶) → (𝐴 ≤ 𝐶 ∧ 𝐶 ≠ 𝐴)))
127	4, 22	ltlend 11409	. . . . 5 ⊢ (𝜑 → (𝐴 < 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐶 ≠ 𝐴)))
128	126, 127	sylibrd 258	. . . 4 ⊢ (𝜑 → ((𝐹‘𝐴) < (𝐹‘𝐶) → 𝐴 < 𝐶))
129	119, 128	mpd 15	. . 3 ⊢ (𝜑 → 𝐴 < 𝐶)
130	14	simprd 494	. . . . 5 ⊢ (𝜑 → 𝑈 < (𝐹‘𝐵))
131	118, 130	eqbrtrd 5175	. . . 4 ⊢ (𝜑 → (𝐹‘𝐶) < (𝐹‘𝐵))
132		fveq2 6901	. . . . . . . . . 10 ⊢ (𝐵 = 𝐶 → (𝐹‘𝐵) = (𝐹‘𝐶))
133	132	breq2d 5165	. . . . . . . . 9 ⊢ (𝐵 = 𝐶 → ((𝐹‘𝐶) < (𝐹‘𝐵) ↔ (𝐹‘𝐶) < (𝐹‘𝐶)))
134	133	notbid 317	. . . . . . . 8 ⊢ (𝐵 = 𝐶 → (¬ (𝐹‘𝐶) < (𝐹‘𝐵) ↔ ¬ (𝐹‘𝐶) < (𝐹‘𝐶)))
135	120, 134	syl5ibrcom 246	. . . . . . 7 ⊢ (𝜑 → (𝐵 = 𝐶 → ¬ (𝐹‘𝐶) < (𝐹‘𝐵)))
136	135	necon2ad 2945	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐵 ≠ 𝐶))
137	136, 32	jctild 524	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
138	22, 5	ltlend 11409	. . . . 5 ⊢ (𝜑 → (𝐶 < 𝐵 ↔ (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶)))
139	137, 138	sylibrd 258	. . . 4 ⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵))
140	131, 139	mpd 15	. . 3 ⊢ (𝜑 → 𝐶 < 𝐵)
141	4	rexrd 11314	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
142	5	rexrd 11314	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
143		elioo2 13419	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
144	141, 142, 143	syl2anc 582	. . 3 ⊢ (𝜑 → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
145	22, 129, 140, 144	mpbir3and 1339	. 2 ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))
146	145, 118	jca 510	1 ⊢ (𝜑 → (𝐶 ∈ (𝐴(,)𝐵) ∧ (𝐹‘𝐶) = 𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1534 ∈ wcel 2099 ≠ wne 2930 ∀wral 3051 ∃wrex 3060 {crab 3419 ⊆ wss 3947 ∅c0 4325 class class class wbr 5153 ‘cfv 6554 (class class class)co 7424 supcsup 9483 ℂcc 11156 ℝcr 11157 + caddc 11161 ℝ^*cxr 11297 < clt 11298 ≤ cle 11299 − cmin 11494 ℝ⁺crp 13028 (,)cioo 13378 [,]cicc 13381 abscabs 15239 –cn→ccncf 24887

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746 ax-cnex 11214 ax-resscn 11215 ax-1cn 11216 ax-icn 11217 ax-addcl 11218 ax-addrcl 11219 ax-mulcl 11220 ax-mulrcl 11221 ax-mulcom 11222 ax-addass 11223 ax-mulass 11224 ax-distr 11225 ax-i2m1 11226 ax-1ne0 11227 ax-1rid 11228 ax-rnegex 11229 ax-rrecex 11230 ax-cnre 11231 ax-pre-lttri 11232 ax-pre-lttrn 11233 ax-pre-ltadd 11234 ax-pre-mulgt0 11235 ax-pre-sup 11236

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-iun 5003 df-br 5154 df-opab 5216 df-mpt 5237 df-tr 5271 df-id 5580 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-we 5639 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-pred 6312 df-ord 6379 df-on 6380 df-lim 6381 df-suc 6382 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-riota 7380 df-ov 7427 df-oprab 7428 df-mpo 7429 df-om 7877 df-1st 8003 df-2nd 8004 df-frecs 8296 df-wrecs 8327 df-recs 8401 df-rdg 8440 df-er 8734 df-map 8857 df-en 8975 df-dom 8976 df-sdom 8977 df-sup 9485 df-pnf 11300 df-mnf 11301 df-xr 11302 df-ltxr 11303 df-le 11304 df-sub 11496 df-neg 11497 df-div 11922 df-nn 12265 df-2 12327 df-3 12328 df-n0 12525 df-z 12611 df-uz 12875 df-rp 13029 df-ioo 13382 df-icc 13385 df-seq 14022 df-exp 14082 df-cj 15104 df-re 15105 df-im 15106 df-sqrt 15240 df-abs 15241 df-cncf 24889

This theorem is referenced by: ivth 25474

W3C validator

	
		OSZAR »