c1liplem1 - Metamath Proof Explorer

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

Theorem c1liplem1 24050

Description: Lemma for c1lip1 24051. (Contributed by Stefan O'Rear, 15-Nov-2014.)

**Hypotheses**
Ref	Expression
c1liplem1.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
c1liplem1.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
c1liplem1.le	⊢ (𝜑 → 𝐴 ≤ 𝐵)
c1liplem1.f	⊢ (𝜑 → 𝐹 ∈ (ℂ ↑_pm ℝ))
c1liplem1.dv	⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
c1liplem1.cn	⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
c1liplem1.k	⊢ 𝐾 = sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < )

**Assertion**
Ref	Expression
c1liplem1	⊢ (𝜑 → (𝐾 ∈ ℝ ∧ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥))))))

Distinct variable groups: 𝜑,𝑥,𝑦 𝑥,𝐴,𝑦 𝑥,𝐵,𝑦 𝑥,𝐹,𝑦 Allowed substitution hints: 𝐾(𝑥,𝑦)

Proof of Theorem c1liplem1 Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		c1liplem1.k	. . 3 ⊢ 𝐾 = sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < )
2		imassrn 5659	. . . . . 6 ⊢ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ⊆ ran abs
3		absf 14362	. . . . . . 7 ⊢ abs:ℂ⟶ℝ
4		frn 6229	. . . . . . 7 ⊢ (abs:ℂ⟶ℝ → ran abs ⊆ ℝ)
5	3, 4	ax-mp 5	. . . . . 6 ⊢ ran abs ⊆ ℝ
6	2, 5	sstri 3770	. . . . 5 ⊢ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ⊆ ℝ
7	6	a1i 11	. . . 4 ⊢ (𝜑 → (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ⊆ ℝ)
8		dvf 23962	. . . . . . . 8 ⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
9		ffun 6226	. . . . . . . 8 ⊢ ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun (ℝ D 𝐹))
10	8, 9	ax-mp 5	. . . . . . 7 ⊢ Fun (ℝ D 𝐹)
11	10	a1i 11	. . . . . 6 ⊢ (𝜑 → Fun (ℝ D 𝐹))
12		c1liplem1.dv	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
13		cncff 22975	. . . . . . . 8 ⊢ (((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ) → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ)
14		fdm 6231	. . . . . . . 8 ⊢ (((ℝ D 𝐹) ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ → dom ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) = (𝐴[,]𝐵))
15	12, 13, 14	3syl 18	. . . . . . 7 ⊢ (𝜑 → dom ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) = (𝐴[,]𝐵))
16		ssdmres 5595	. . . . . . 7 ⊢ ((𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) = (𝐴[,]𝐵))
17	15, 16	sylibr 225	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹))
18		c1liplem1.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ)
19	18	rexrd 10343	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
20		c1liplem1.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℝ)
21	20	rexrd 10343	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
22		c1liplem1.le	. . . . . . 7 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
23		lbicc2 12492	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
24	19, 21, 22, 23	syl3anc 1490	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
25		funfvima2 6686	. . . . . . 7 ⊢ ((Fun (ℝ D 𝐹) ∧ (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) → (𝐴 ∈ (𝐴[,]𝐵) → ((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))
26	25	imp 395	. . . . . 6 ⊢ (((Fun (ℝ D 𝐹) ∧ (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) ∧ 𝐴 ∈ (𝐴[,]𝐵)) → ((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))
27	11, 17, 24, 26	syl21anc 866	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))
28		ffun 6226	. . . . . . 7 ⊢ (abs:ℂ⟶ℝ → Fun abs)
29	3, 28	ax-mp 5	. . . . . 6 ⊢ Fun abs
30		imassrn 5659	. . . . . . . 8 ⊢ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) ⊆ ran (ℝ D 𝐹)
31		frn 6229	. . . . . . . . 9 ⊢ ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ → ran (ℝ D 𝐹) ⊆ ℂ)
32	8, 31	ax-mp 5	. . . . . . . 8 ⊢ ran (ℝ D 𝐹) ⊆ ℂ
33	30, 32	sstri 3770	. . . . . . 7 ⊢ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) ⊆ ℂ
34	3	fdmi 6233	. . . . . . 7 ⊢ dom abs = ℂ
35	33, 34	sseqtr4i 3798	. . . . . 6 ⊢ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) ⊆ dom abs
36		funfvima2 6686	. . . . . 6 ⊢ ((Fun abs ∧ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) ⊆ dom abs) → (((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → (abs‘((ℝ D 𝐹)‘𝐴)) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))))
37	29, 35, 36	mp2an 683	. . . . 5 ⊢ (((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → (abs‘((ℝ D 𝐹)‘𝐴)) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))
38		ne0i 4085	. . . . 5 ⊢ ((abs‘((ℝ D 𝐹)‘𝐴)) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ≠ ∅)
39	27, 37, 38	3syl 18	. . . 4 ⊢ (𝜑 → (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ≠ ∅)
40		ax-resscn 10246	. . . . . . . 8 ⊢ ℝ ⊆ ℂ
41		ssid 3783	. . . . . . . 8 ⊢ ℂ ⊆ ℂ
42		cncfss 22981	. . . . . . . 8 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ))
43	40, 41, 42	mp2an 683	. . . . . . 7 ⊢ ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ)
44	43, 12	sseldi 3759	. . . . . 6 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
45		cniccbdd 23519	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑎 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎)
46	18, 20, 44, 45	syl3anc 1490	. . . . 5 ⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎)
47		fvelima 6437	. . . . . . . . . 10 ⊢ ((Fun abs ∧ 𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) → ∃𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))(abs‘𝑦) = 𝑏)
48	29, 47	mpan 681	. . . . . . . . 9 ⊢ (𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → ∃𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))(abs‘𝑦) = 𝑏)
49		fvelima 6437	. . . . . . . . . . . . . 14 ⊢ ((Fun (ℝ D 𝐹) ∧ 𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → ∃𝑏 ∈ (𝐴[,]𝐵)((ℝ D 𝐹)‘𝑏) = 𝑦)
50	10, 49	mpan 681	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → ∃𝑏 ∈ (𝐴[,]𝐵)((ℝ D 𝐹)‘𝑏) = 𝑦)
51		fvres 6394	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ (𝐴[,]𝐵) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏) = ((ℝ D 𝐹)‘𝑏))
52	51	adantl 473	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏) = ((ℝ D 𝐹)‘𝑏))
53	52	fveq2d 6379	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏)) = (abs‘((ℝ D 𝐹)‘𝑏)))
54		2fveq3 6380	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑏 → (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) = (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏)))
55	54	breq1d 4819	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑏 → ((abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ↔ (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏)) ≤ 𝑎))
56	55	rspccva 3460	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏)) ≤ 𝑎)
57	53, 56	eqbrtrrd 4833	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (abs‘((ℝ D 𝐹)‘𝑏)) ≤ 𝑎)
58	57	adantll 705	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (abs‘((ℝ D 𝐹)‘𝑏)) ≤ 𝑎)
59		fveq2 6375	. . . . . . . . . . . . . . . 16 ⊢ (((ℝ D 𝐹)‘𝑏) = 𝑦 → (abs‘((ℝ D 𝐹)‘𝑏)) = (abs‘𝑦))
60	59	breq1d 4819	. . . . . . . . . . . . . . 15 ⊢ (((ℝ D 𝐹)‘𝑏) = 𝑦 → ((abs‘((ℝ D 𝐹)‘𝑏)) ≤ 𝑎 ↔ (abs‘𝑦) ≤ 𝑎))
61	58, 60	syl5ibcom 236	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (((ℝ D 𝐹)‘𝑏) = 𝑦 → (abs‘𝑦) ≤ 𝑎))
62	61	rexlimdva 3178	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → (∃𝑏 ∈ (𝐴[,]𝐵)((ℝ D 𝐹)‘𝑏) = 𝑦 → (abs‘𝑦) ≤ 𝑎))
63	50, 62	syl5 34	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → (𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → (abs‘𝑦) ≤ 𝑎))
64	63	imp 395	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) ∧ 𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → (abs‘𝑦) ≤ 𝑎)
65		breq1 4812	. . . . . . . . . . 11 ⊢ ((abs‘𝑦) = 𝑏 → ((abs‘𝑦) ≤ 𝑎 ↔ 𝑏 ≤ 𝑎))
66	64, 65	syl5ibcom 236	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) ∧ 𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → ((abs‘𝑦) = 𝑏 → 𝑏 ≤ 𝑎))
67	66	rexlimdva 3178	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → (∃𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))(abs‘𝑦) = 𝑏 → 𝑏 ≤ 𝑎))
68	48, 67	syl5 34	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → (𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → 𝑏 ≤ 𝑎))
69	68	ralrimiv 3112	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎)
70	69	ex 401	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 → ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎))
71	70	reximdva 3163	. . . . 5 ⊢ (𝜑 → (∃𝑎 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 → ∃𝑎 ∈ ℝ ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎))
72	46, 71	mpd 15	. . . 4 ⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎)
73		suprcl 11237	. . . 4 ⊢ (((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ⊆ ℝ ∧ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ≠ ∅ ∧ ∃𝑎 ∈ ℝ ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎) → sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < ) ∈ ℝ)
74	7, 39, 72, 73	syl3anc 1490	. . 3 ⊢ (𝜑 → sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < ) ∈ ℝ)
75	1, 74	syl5eqel 2848	. 2 ⊢ (𝜑 → 𝐾 ∈ ℝ)
76		simplrr 796	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ (𝐴[,]𝐵))
77		fvres 6394	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝐴[,]𝐵) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑦) = (𝐹‘𝑦))
78	76, 77	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑦) = (𝐹‘𝑦))
79		c1liplem1.cn	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
80		cncff 22975	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ) → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ)
81	79, 80	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ)
82	81	ad2antrr 717	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ)
83	82, 76	ffvelrnd 6550	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑦) ∈ ℝ)
84	83	recnd 10322	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑦) ∈ ℂ)
85	78, 84	eqeltrrd 2845	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹‘𝑦) ∈ ℂ)
86		simplrl 795	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ (𝐴[,]𝐵))
87		fvres 6394	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑥) = (𝐹‘𝑥))
88	86, 87	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑥) = (𝐹‘𝑥))
89	82, 86	ffvelrnd 6550	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑥) ∈ ℝ)
90	89	recnd 10322	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑥) ∈ ℂ)
91	88, 90	eqeltrrd 2845	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹‘𝑥) ∈ ℂ)
92	85, 91	subcld 10646	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹‘𝑦) − (𝐹‘𝑥)) ∈ ℂ)
93		iccssre 12457	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
94	18, 20, 93	syl2anc 579	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
95	94	ad2antrr 717	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐴[,]𝐵) ⊆ ℝ)
96	95, 76	sseldd 3762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℝ)
97	95, 86	sseldd 3762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℝ)
98	96, 97	resubcld 10712	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦 − 𝑥) ∈ ℝ)
99	98	recnd 10322	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦 − 𝑥) ∈ ℂ)
100		simpr 477	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 < 𝑦)
101		difrp 12066	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 < 𝑦 ↔ (𝑦 − 𝑥) ∈ ℝ⁺))
102	97, 96, 101	syl2anc 579	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥 < 𝑦 ↔ (𝑦 − 𝑥) ∈ ℝ⁺))
103	100, 102	mpbid 223	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦 − 𝑥) ∈ ℝ⁺)
104	103	rpne0d 12075	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦 − 𝑥) ≠ 0)
105	92, 99, 104	absdivd 14479	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (abs‘(𝑦 − 𝑥))))
106	6	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ⊆ ℝ)
107	39	ad2antrr 717	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ≠ ∅)
108	72	ad2antrr 717	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ∃𝑎 ∈ ℝ ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎)
109	29	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → Fun abs)
110	92, 99, 104	divcld 11055	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ℂ)
111	110, 34	syl6eleqr 2855	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ dom abs)
112	97	rexrd 10343	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℝ^*)
113	96	rexrd 10343	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℝ^*)
114	97, 96, 100	ltled 10439	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ≤ 𝑦)
115		ubicc2 12493	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑥 ≤ 𝑦) → 𝑦 ∈ (𝑥[,]𝑦))
116	112, 113, 114, 115	syl3anc 1490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ (𝑥[,]𝑦))
117		fvres 6394	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝑥[,]𝑦) → ((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) = (𝐹‘𝑦))
118	116, 117	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) = (𝐹‘𝑦))
119		lbicc2 12492	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑥 ≤ 𝑦) → 𝑥 ∈ (𝑥[,]𝑦))
120	112, 113, 114, 119	syl3anc 1490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ (𝑥[,]𝑦))
121		fvres 6394	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝑥[,]𝑦) → ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥) = (𝐹‘𝑥))
122	120, 121	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥) = (𝐹‘𝑥))
123	118, 122	oveq12d 6860	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) = ((𝐹‘𝑦) − (𝐹‘𝑥)))
124	123	oveq1d 6857	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))
125		iccss2 12446	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑥[,]𝑦) ⊆ (𝐴[,]𝐵))
126	125	ad2antlr 718	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥[,]𝑦) ⊆ (𝐴[,]𝐵))
127	126	resabs1d 5603	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ (𝑥[,]𝑦)) = (𝐹 ↾ (𝑥[,]𝑦)))
128	79	ad2antrr 717	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
129		rescncf 22979	. . . . . . . . . . . . . . 15 ⊢ ((𝑥[,]𝑦) ⊆ (𝐴[,]𝐵) → ((𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ (𝑥[,]𝑦)) ∈ ((𝑥[,]𝑦)–cn→ℝ)))
130	126, 128, 129	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ (𝑥[,]𝑦)) ∈ ((𝑥[,]𝑦)–cn→ℝ))
131	127, 130	eqeltrrd 2845	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹 ↾ (𝑥[,]𝑦)) ∈ ((𝑥[,]𝑦)–cn→ℝ))
132	40	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ℝ ⊆ ℂ)
133		c1liplem1.f	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑_pm ℝ))
134	133	ad2antrr 717	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝐹 ∈ (ℂ ↑_pm ℝ))
135		cnex 10270	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℂ ∈ V
136		reex 10280	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℝ ∈ V
137	135, 136	elpm2 8092	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (ℂ ↑_pm ℝ) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ))
138	137	simplbi 491	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (ℂ ↑_pm ℝ) → 𝐹:dom 𝐹⟶ℂ)
139	134, 138	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝐹:dom 𝐹⟶ℂ)
140	137	simprbi 490	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (ℂ ↑_pm ℝ) → dom 𝐹 ⊆ ℝ)
141	134, 140	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → dom 𝐹 ⊆ ℝ)
142		iccssre 12457	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥[,]𝑦) ⊆ ℝ)
143	97, 96, 142	syl2anc 579	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥[,]𝑦) ⊆ ℝ)
144		eqid 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
145	144	tgioo2 22885	. . . . . . . . . . . . . . . . . 18 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
146	144, 145	dvres 23966	. . . . . . . . . . . . . . . . 17 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:dom 𝐹⟶ℂ) ∧ (dom 𝐹 ⊆ ℝ ∧ (𝑥[,]𝑦) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑥[,]𝑦))))
147	132, 139, 141, 143, 146	syl22anc 867	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑥[,]𝑦))))
148		iccntr 22903	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑥[,]𝑦)) = (𝑥(,)𝑦))
149	97, 96, 148	syl2anc 579	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((int‘(topGen‘ran (,)))‘(𝑥[,]𝑦)) = (𝑥(,)𝑦))
150	149	reseq2d 5565	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑥[,]𝑦))) = ((ℝ D 𝐹) ↾ (𝑥(,)𝑦)))
151	147, 150	eqtrd 2799	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = ((ℝ D 𝐹) ↾ (𝑥(,)𝑦)))
152	151	dmeqd 5494	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → dom (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = dom ((ℝ D 𝐹) ↾ (𝑥(,)𝑦)))
153		ioossicc 12461	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥(,)𝑦) ⊆ (𝑥[,]𝑦)
154	153, 126	syl5ss 3772	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥(,)𝑦) ⊆ (𝐴[,]𝐵))
155	17	ad2antrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹))
156	154, 155	sstrd 3771	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥(,)𝑦) ⊆ dom (ℝ D 𝐹))
157		ssdmres 5595	. . . . . . . . . . . . . . 15 ⊢ ((𝑥(,)𝑦) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝑥(,)𝑦)) = (𝑥(,)𝑦))
158	156, 157	sylib 209	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → dom ((ℝ D 𝐹) ↾ (𝑥(,)𝑦)) = (𝑥(,)𝑦))
159	152, 158	eqtrd 2799	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → dom (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = (𝑥(,)𝑦))
160	97, 96, 100, 131, 159	mvth 24046	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ∃𝑎 ∈ (𝑥(,)𝑦)((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)))
161	151	fveq1d 6377	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = (((ℝ D 𝐹) ↾ (𝑥(,)𝑦))‘𝑎))
162	161	adantrr 708	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → ((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = (((ℝ D 𝐹) ↾ (𝑥(,)𝑦))‘𝑎))
163		fvres 6394	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ (𝑥(,)𝑦) → (((ℝ D 𝐹) ↾ (𝑥(,)𝑦))‘𝑎) = ((ℝ D 𝐹)‘𝑎))
164	163	ad2antll 720	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → (((ℝ D 𝐹) ↾ (𝑥(,)𝑦))‘𝑎) = ((ℝ D 𝐹)‘𝑎))
165	162, 164	eqtrd 2799	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → ((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((ℝ D 𝐹)‘𝑎))
166	10	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → Fun (ℝ D 𝐹))
167	17	ad2antrr 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹))
168	154	sseld 3760	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑎 ∈ (𝑥(,)𝑦) → 𝑎 ∈ (𝐴[,]𝐵)))
169	168	impr 446	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → 𝑎 ∈ (𝐴[,]𝐵))
170		funfvima2 6686	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun (ℝ D 𝐹) ∧ (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) → (𝑎 ∈ (𝐴[,]𝐵) → ((ℝ D 𝐹)‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))
171	170	imp 395	. . . . . . . . . . . . . . . . 17 ⊢ (((Fun (ℝ D 𝐹) ∧ (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) ∧ 𝑎 ∈ (𝐴[,]𝐵)) → ((ℝ D 𝐹)‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))
172	166, 167, 169, 171	syl21anc 866	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → ((ℝ D 𝐹)‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))
173	165, 172	eqeltrd 2844	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → ((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))
174		eleq1 2832	. . . . . . . . . . . . . . 15 ⊢ (((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) → (((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) ↔ ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))
175	173, 174	syl5ibcom 236	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → (((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))
176	175	expr 448	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑎 ∈ (𝑥(,)𝑦) → (((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))))
177	176	rexlimdv 3177	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (∃𝑎 ∈ (𝑥(,)𝑦)((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))
178	160, 177	mpd 15	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))
179	124, 178	eqeltrrd 2845	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))
180		funfvima 6685	. . . . . . . . . . 11 ⊢ ((Fun abs ∧ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ dom abs) → ((((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))))
181	180	imp 395	. . . . . . . . . 10 ⊢ (((Fun abs ∧ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ dom abs) ∧ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))
182	109, 111, 179, 181	syl21anc 866	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))
183		suprub 11238	. . . . . . . . 9 ⊢ ((((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ⊆ ℝ ∧ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ≠ ∅ ∧ ∃𝑎 ∈ ℝ ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎) ∧ (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ≤ sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < ))
184	106, 107, 108, 182, 183	syl31anc 1492	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ≤ sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < ))
185	184, 1	syl6breqr 4851	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ≤ 𝐾)
186	105, 185	eqbrtrrd 4833	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (abs‘(𝑦 − 𝑥))) ≤ 𝐾)
187	92	abscld 14460	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ∈ ℝ)
188	75	ad2antrr 717	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝐾 ∈ ℝ)
189	99, 104	absrpcld 14472	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(𝑦 − 𝑥)) ∈ ℝ⁺)
190	187, 188, 189	ledivmuld 12123	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (abs‘(𝑦 − 𝑥))) ≤ 𝐾 ↔ (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ ((abs‘(𝑦 − 𝑥)) · 𝐾)))
191	186, 190	mpbid 223	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ ((abs‘(𝑦 − 𝑥)) · 𝐾))
192	189	rpcnd 12072	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(𝑦 − 𝑥)) ∈ ℂ)
193	188	recnd 10322	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝐾 ∈ ℂ)
194	192, 193	mulcomd 10315	. . . . 5 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((abs‘(𝑦 − 𝑥)) · 𝐾) = (𝐾 · (abs‘(𝑦 − 𝑥))))
195	191, 194	breqtrd 4835	. . . 4 ⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥))))
196	195	ex 401	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥)))))
197	196	ralrimivva 3118	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥)))))
198	75, 197	jca 507	1 ⊢ (𝜑 → (𝐾 ∈ ℝ ∧ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 197 ∧ wa 384 = wceq 1652 ∈ wcel 2155 ≠ wne 2937 ∀wral 3055 ∃wrex 3056 ⊆ wss 3732 ∅c0 4079 class class class wbr 4809 dom cdm 5277 ran crn 5278 ↾ cres 5279 “ cima 5280 Fun wfun 6062 ⟶wf 6064 ‘cfv 6068 (class class class)co 6842 ↑_pm cpm 8061 supcsup 8553 ℂcc 10187 ℝcr 10188 · cmul 10194 ℝ^*cxr 10327 < clt 10328 ≤ cle 10329 − cmin 10520 / cdiv 10938 ℝ⁺crp 12028 (,)cioo 12377 [,]cicc 12380 abscabs 14259 TopOpenctopn 16348 topGenctg 16364 ℂ_fldccnfld 20019 intcnt 21101 –cn→ccncf 22958 D cdv 23918

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-rep 4930 ax-sep 4941 ax-nul 4949 ax-pow 5001 ax-pr 5062 ax-un 7147 ax-inf2 8753 ax-cnex 10245 ax-resscn 10246 ax-1cn 10247 ax-icn 10248 ax-addcl 10249 ax-addrcl 10250 ax-mulcl 10251 ax-mulrcl 10252 ax-mulcom 10253 ax-addass 10254 ax-mulass 10255 ax-distr 10256 ax-i2m1 10257 ax-1ne0 10258 ax-1rid 10259 ax-rnegex 10260 ax-rrecex 10261 ax-cnre 10262 ax-pre-lttri 10263 ax-pre-lttrn 10264 ax-pre-ltadd 10265 ax-pre-mulgt0 10266 ax-pre-sup 10267 ax-addf 10268 ax-mulf 10269

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3or 1108 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-nel 3041 df-ral 3060 df-rex 3061 df-reu 3062 df-rmo 3063 df-rab 3064 df-v 3352 df-sbc 3597 df-csb 3692 df-dif 3735 df-un 3737 df-in 3739 df-ss 3746 df-pss 3748 df-nul 4080 df-if 4244 df-pw 4317 df-sn 4335 df-pr 4337 df-tp 4339 df-op 4341 df-uni 4595 df-int 4634 df-iun 4678 df-iin 4679 df-br 4810 df-opab 4872 df-mpt 4889 df-tr 4912 df-id 5185 df-eprel 5190 df-po 5198 df-so 5199 df-fr 5236 df-se 5237 df-we 5238 df-xp 5283 df-rel 5284 df-cnv 5285 df-co 5286 df-dm 5287 df-rn 5288 df-res 5289 df-ima 5290 df-pred 5865 df-ord 5911 df-on 5912 df-lim 5913 df-suc 5914 df-iota 6031 df-fun 6070 df-fn 6071 df-f 6072 df-f1 6073 df-fo 6074 df-f1o 6075 df-fv 6076 df-isom 6077 df-riota 6803 df-ov 6845 df-oprab 6846 df-mpt2 6847 df-of 7095 df-om 7264 df-1st 7366 df-2nd 7367 df-supp 7498 df-wrecs 7610 df-recs 7672 df-rdg 7710 df-1o 7764 df-2o 7765 df-oadd 7768 df-er 7947 df-map 8062 df-pm 8063 df-ixp 8114 df-en 8161 df-dom 8162 df-sdom 8163 df-fin 8164 df-fsupp 8483 df-fi 8524 df-sup 8555 df-inf 8556 df-oi 8622 df-card 9016 df-cda 9243 df-pnf 10330 df-mnf 10331 df-xr 10332 df-ltxr 10333 df-le 10334 df-sub 10522 df-neg 10523 df-div 10939 df-nn 11275 df-2 11335 df-3 11336 df-4 11337 df-5 11338 df-6 11339 df-7 11340 df-8 11341 df-9 11342 df-n0 11539 df-z 11625 df-dec 11741 df-uz 11887 df-q 11990 df-rp 12029 df-xneg 12146 df-xadd 12147 df-xmul 12148 df-ioo 12381 df-ico 12383 df-icc 12384 df-fz 12534 df-fzo 12674 df-seq 13009 df-exp 13068 df-hash 13322 df-cj 14124 df-re 14125 df-im 14126 df-sqrt 14260 df-abs 14261 df-struct 16132 df-ndx 16133 df-slot 16134 df-base 16136 df-sets 16137 df-ress 16138 df-plusg 16227 df-mulr 16228 df-starv 16229 df-sca 16230 df-vsca 16231 df-ip 16232 df-tset 16233 df-ple 16234 df-ds 16236 df-unif 16237 df-hom 16238 df-cco 16239 df-rest 16349 df-topn 16350 df-0g 16368 df-gsum 16369 df-topgen 16370 df-pt 16371 df-prds 16374 df-xrs 16428 df-qtop 16433 df-imas 16434 df-xps 16436 df-mre 16512 df-mrc 16513 df-acs 16515 df-mgm 17508 df-sgrp 17550 df-mnd 17561 df-submnd 17602 df-mulg 17808 df-cntz 18013 df-cmn 18461 df-psmet 20011 df-xmet 20012 df-met 20013 df-bl 20014 df-mopn 20015 df-fbas 20016 df-fg 20017 df-cnfld 20020 df-top 20978 df-topon 20995 df-topsp 21017 df-bases 21030 df-cld 21103 df-ntr 21104 df-cls 21105 df-nei 21182 df-lp 21220 df-perf 21221 df-cn 21311 df-cnp 21312 df-haus 21399 df-cmp 21470 df-tx 21645 df-hmeo 21838 df-fil 21929 df-fm 22021 df-flim 22022 df-flf 22023 df-xms 22404 df-ms 22405 df-tms 22406 df-cncf 22960 df-limc 23921 df-dv 23922

This theorem is referenced by: c1lip1 24051

W3C validator