dvivthlem1 - Metamath Proof Explorer

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

Theorem dvivthlem1 23771

Description: Lemma for dvivth 23773. (Contributed by Mario Carneiro, 24-Feb-2015.)

**Hypotheses**
Ref	Expression
dvivth.1	⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵))
dvivth.2	⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵))
dvivth.3	⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
dvivth.4	⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
dvivth.5	⊢ (𝜑 → 𝑀 < 𝑁)
dvivth.6	⊢ (𝜑 → 𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)))
dvivth.7	⊢ 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦)))

**Assertion**
Ref	Expression
dvivthlem1	⊢ (𝜑 → ∃𝑥 ∈ (𝑀[,]𝑁)((ℝ D 𝐹)‘𝑥) = 𝐶)

Distinct variable groups: 𝑥,𝑦,𝐴 𝑥,𝐵,𝑦 𝑥,𝐹,𝑦 𝑥,𝐺 𝑥,𝑀,𝑦 𝑥,𝐶,𝑦 𝑥,𝑁,𝑦 𝜑,𝑥,𝑦 Allowed substitution hint: 𝐺(𝑦)

Proof of Theorem dvivthlem1 Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ioossre 12235	. . . . 5 ⊢ (𝐴(,)𝐵) ⊆ ℝ
2		dvivth.1	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵))
3	1, 2	sseldi 3601	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℝ)
4		dvivth.2	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵))
5	1, 4	sseldi 3601	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℝ)
6		dvivth.5	. . . . 5 ⊢ (𝜑 → 𝑀 < 𝑁)
7	3, 5, 6	ltled 10185	. . . 4 ⊢ (𝜑 → 𝑀 ≤ 𝑁)
8		dvivth.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
9		cncff 22696	. . . . . . . . . 10 ⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)
11	10	ffvelrnda 6359	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑦) ∈ ℝ)
12		dvfre 23714	. . . . . . . . . . . . . 14 ⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
13	10, 1, 12	sylancl 694	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
14		dvivth.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
15	4, 14	eleqtrrd 2704	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ dom (ℝ D 𝐹))
16	13, 15	ffvelrnd 6360	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℝ D 𝐹)‘𝑁) ∈ ℝ)
17	2, 14	eleqtrrd 2704	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ dom (ℝ D 𝐹))
18	13, 17	ffvelrnd 6360	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℝ D 𝐹)‘𝑀) ∈ ℝ)
19		iccssre 12255	. . . . . . . . . . . 12 ⊢ ((((ℝ D 𝐹)‘𝑁) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑀) ∈ ℝ) → (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)) ⊆ ℝ)
20	16, 18, 19	syl2anc 693	. . . . . . . . . . 11 ⊢ (𝜑 → (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)) ⊆ ℝ)
21		dvivth.6	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)))
22	20, 21	sseldd 3604	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
23	22	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ)
24	1	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
25	24	sselda 3603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℝ)
26	23, 25	remulcld 10070	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐶 · 𝑦) ∈ ℝ)
27	11, 26	resubcld 10458	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑦) − (𝐶 · 𝑦)) ∈ ℝ)
28		dvivth.7	. . . . . . 7 ⊢ 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦)))
29	27, 28	fmptd 6385	. . . . . 6 ⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ)
30		iccssioo2 12246	. . . . . . 7 ⊢ ((𝑀 ∈ (𝐴(,)𝐵) ∧ 𝑁 ∈ (𝐴(,)𝐵)) → (𝑀[,]𝑁) ⊆ (𝐴(,)𝐵))
31	2, 4, 30	syl2anc 693	. . . . . 6 ⊢ (𝜑 → (𝑀[,]𝑁) ⊆ (𝐴(,)𝐵))
32	29, 31	fssresd 6071	. . . . 5 ⊢ (𝜑 → (𝐺 ↾ (𝑀[,]𝑁)):(𝑀[,]𝑁)⟶ℝ)
33		ax-resscn 9993	. . . . . 6 ⊢ ℝ ⊆ ℂ
34	33	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ ⊆ ℂ)
35		fss 6056	. . . . . . . . 9 ⊢ ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
36	29, 33, 35	sylancl 694	. . . . . . . 8 ⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℂ)
37	28	oveq2i 6661	. . . . . . . . . . 11 ⊢ (ℝ D 𝐺) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦))))
38		reelprrecn 10028	. . . . . . . . . . . . 13 ⊢ ℝ ∈ {ℝ, ℂ}
39	38	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
40	11	recnd 10068	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑦) ∈ ℂ)
41	14	feq2d 6031	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ))
42	13, 41	mpbid 222	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ)
43	42	ffvelrnda 6359	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑦) ∈ ℝ)
44	10	feqmptd 6249	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)))
45	44	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦))))
46	42	feqmptd 6249	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ D 𝐹) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
47	45, 46	eqtr3d 2658	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
48	26	recnd 10068	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐶 · 𝑦) ∈ ℂ)
49		remulcl 10021	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐶 · 𝑦) ∈ ℝ)
50	22, 49	sylan 488	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐶 · 𝑦) ∈ ℝ)
51	50	recnd 10068	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐶 · 𝑦) ∈ ℂ)
52	22	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐶 ∈ ℝ)
53	34	sselda 3603	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
54		1cnd 10056	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈ ℂ)
55	39	dvmptid 23720	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
56	22	recnd 10068	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ ℂ)
57	39, 53, 54, 55, 56	dvmptcmul 23727	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (𝐶 · 𝑦))) = (𝑦 ∈ ℝ ↦ (𝐶 · 1)))
58	56	mulid1d 10057	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶 · 1) = 𝐶)
59	58	mpteq2dv 4745	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝐶 · 1)) = (𝑦 ∈ ℝ ↦ 𝐶))
60	57, 59	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (𝐶 · 𝑦))) = (𝑦 ∈ ℝ ↦ 𝐶))
61		eqid 2622	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
62	61	tgioo2 22606	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
63		iooretop 22569	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
64	63	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran (,)))
65	39, 51, 52, 60, 24, 62, 61, 64	dvmptres 23726	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐶 · 𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 𝐶))
66	39, 40, 43, 47, 48, 23, 65	dvmptsub 23730	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦)))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)))
67	37, 66	syl5eq 2668	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D 𝐺) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)))
68	67	dmeqd 5326	. . . . . . . . 9 ⊢ (𝜑 → dom (ℝ D 𝐺) = dom (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)))
69		dmmptg 5632	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ (𝐴(,)𝐵)(((ℝ D 𝐹)‘𝑦) − 𝐶) ∈ V → dom (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)) = (𝐴(,)𝐵))
70		ovex 6678	. . . . . . . . . . 11 ⊢ (((ℝ D 𝐹)‘𝑦) − 𝐶) ∈ V
71	70	a1i 11	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝐴(,)𝐵) → (((ℝ D 𝐹)‘𝑦) − 𝐶) ∈ V)
72	69, 71	mprg 2926	. . . . . . . . 9 ⊢ dom (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)) = (𝐴(,)𝐵)
73	68, 72	syl6eq 2672	. . . . . . . 8 ⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
74		dvcn 23684	. . . . . . . 8 ⊢ (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐺) = (𝐴(,)𝐵)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
75	34, 36, 24, 73, 74	syl31anc 1329	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
76		rescncf 22700	. . . . . . 7 ⊢ ((𝑀[,]𝑁) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ) → (𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)))
77	31, 75, 76	sylc 65	. . . . . 6 ⊢ (𝜑 → (𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ))
78		cncffvrn 22701	. . . . . 6 ⊢ ((ℝ ⊆ ℂ ∧ (𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) → ((𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℝ) ↔ (𝐺 ↾ (𝑀[,]𝑁)):(𝑀[,]𝑁)⟶ℝ))
79	33, 77, 78	sylancr 695	. . . . 5 ⊢ (𝜑 → ((𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℝ) ↔ (𝐺 ↾ (𝑀[,]𝑁)):(𝑀[,]𝑁)⟶ℝ))
80	32, 79	mpbird 247	. . . 4 ⊢ (𝜑 → (𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℝ))
81	3, 5, 7, 80	evthicc 23228	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ (𝑀[,]𝑁)∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ∧ ∃𝑥 ∈ (𝑀[,]𝑁)∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑧)))
82	81	simpld 475	. 2 ⊢ (𝜑 → ∃𝑥 ∈ (𝑀[,]𝑁)∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥))
83		fvres 6207	. . . . . . . 8 ⊢ (𝑧 ∈ (𝑀[,]𝑁) → ((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) = (𝐺‘𝑧))
84		fvres 6207	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑀[,]𝑁) → ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) = (𝐺‘𝑥))
85	83, 84	breqan12rd 4670	. . . . . . 7 ⊢ ((𝑥 ∈ (𝑀[,]𝑁) ∧ 𝑧 ∈ (𝑀[,]𝑁)) → (((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ↔ (𝐺‘𝑧) ≤ (𝐺‘𝑥)))
86	85	ralbidva 2985	. . . . . 6 ⊢ (𝑥 ∈ (𝑀[,]𝑁) → (∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ↔ ∀𝑧 ∈ (𝑀[,]𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥)))
87	86	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ↔ ∀𝑧 ∈ (𝑀[,]𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥)))
88		ioossicc 12259	. . . . . 6 ⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)
89		ssralv 3666	. . . . . 6 ⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → (∀𝑧 ∈ (𝑀[,]𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥)))
90	88, 89	ax-mp 5	. . . . 5 ⊢ (∀𝑧 ∈ (𝑀[,]𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))
91	87, 90	syl6bi 243	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥)))
92	31	sselda 3603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝑥 ∈ (𝐴(,)𝐵))
93	42	ffvelrnda 6359	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
94	92, 93	syldan 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
95	94	recnd 10068	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
96	95	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
97	56	ad2antrr 762	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐶 ∈ ℂ)
98	67	fveq1d 6193	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℝ D 𝐺)‘𝑥) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))‘𝑥))
99	98	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((ℝ D 𝐺)‘𝑥) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))‘𝑥))
100		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘𝑥))
101	100	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (((ℝ D 𝐹)‘𝑦) − 𝐶) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
102		eqid 2622	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))
103		ovex 6678	. . . . . . . . . . . 12 ⊢ (((ℝ D 𝐹)‘𝑥) − 𝐶) ∈ V
104	101, 102, 103	fvmpt 6282	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
105	92, 104	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
106	99, 105	eqtrd 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((ℝ D 𝐺)‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
107	106	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐺)‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
108	29	ad2antrr 762	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
109	1	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝐴(,)𝐵) ⊆ ℝ)
110		simprl 794	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ (𝑀(,)𝑁))
111	88, 31	syl5ss 3614	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝐴(,)𝐵))
112	111	ad2antrr 762	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝑀(,)𝑁) ⊆ (𝐴(,)𝐵))
113	92	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ (𝐴(,)𝐵))
114	73	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
115	113, 114	eleqtrrd 2704	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ dom (ℝ D 𝐺))
116		simprr 796	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))
117		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → (𝐺‘𝑧) = (𝐺‘𝑤))
118	117	breq1d 4663	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → ((𝐺‘𝑧) ≤ (𝐺‘𝑥) ↔ (𝐺‘𝑤) ≤ (𝐺‘𝑥)))
119	118	cbvralv 3171	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) ↔ ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥))
120	116, 119	sylib 208	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥))
121	108, 109, 110, 112, 115, 120	dvferm 23751	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐺)‘𝑥) = 0)
122	107, 121	eqtr3d 2658	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (((ℝ D 𝐹)‘𝑥) − 𝐶) = 0)
123	96, 97, 122	subeq0d 10400	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) = 𝐶)
124	123	exp32 631	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶)))
125		vex 3203	. . . . . . 7 ⊢ 𝑥 ∈ V
126	125	elpr 4198	. . . . . 6 ⊢ (𝑥 ∈ {𝑀, 𝑁} ↔ (𝑥 = 𝑀 ∨ 𝑥 = 𝑁))
127	106	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐺)‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
128	29	ad2antrr 762	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
129	1	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝐴(,)𝐵) ⊆ ℝ)
130		simprl 794	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 = 𝑀)
131		eliooord 12233	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑀 ∧ 𝑀 < 𝐵))
132	2, 131	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 < 𝑀 ∧ 𝑀 < 𝐵))
133	132	simpld 475	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 < 𝑀)
134		ne0i 3921	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
135		ndmioo 12202	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴(,)𝐵) = ∅)
136	135	necon1ai 2821	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴(,)𝐵) ≠ ∅ → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
137	2, 134, 136	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
138	137	simpld 475	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
139	5	rexrd 10089	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℝ^*)
140		elioo2 12216	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑁 ∈ ℝ^*) → (𝑀 ∈ (𝐴(,)𝑁) ↔ (𝑀 ∈ ℝ ∧ 𝐴 < 𝑀 ∧ 𝑀 < 𝑁)))
141	138, 139, 140	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 ∈ (𝐴(,)𝑁) ↔ (𝑀 ∈ ℝ ∧ 𝐴 < 𝑀 ∧ 𝑀 < 𝑁)))
142	3, 133, 6, 141	mpbir3and 1245	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝑁))
143	142	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑀 ∈ (𝐴(,)𝑁))
144	130, 143	eqeltrd 2701	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ (𝐴(,)𝑁))
145	137	simprd 479	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
146		eliooord 12233	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑁 ∧ 𝑁 < 𝐵))
147	4, 146	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 < 𝑁 ∧ 𝑁 < 𝐵))
148	147	simprd 479	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 < 𝐵)
149		xrltle 11982	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝑁 < 𝐵 → 𝑁 ≤ 𝐵))
150	139, 145, 149	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 < 𝐵 → 𝑁 ≤ 𝐵))
151	148, 150	mpd 15	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ≤ 𝐵)
152		iooss2 12211	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝑁 ≤ 𝐵) → (𝐴(,)𝑁) ⊆ (𝐴(,)𝐵))
153	145, 151, 152	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴(,)𝑁) ⊆ (𝐴(,)𝐵))
154	153	ad2antrr 762	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝐴(,)𝑁) ⊆ (𝐴(,)𝐵))
155	92	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ (𝐴(,)𝐵))
156	73	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
157	155, 156	eleqtrrd 2704	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ dom (ℝ D 𝐺))
158		simprr 796	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))
159	158, 119	sylib 208	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥))
160	130	oveq1d 6665	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝑥(,)𝑁) = (𝑀(,)𝑁))
161	160	raleqdv 3144	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (∀𝑤 ∈ (𝑥(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥) ↔ ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥)))
162	159, 161	mpbird 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑤 ∈ (𝑥(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥))
163	128, 129, 144, 154, 157, 162	dvferm1 23748	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐺)‘𝑥) ≤ 0)
164	127, 163	eqbrtrrd 4677	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (((ℝ D 𝐹)‘𝑥) − 𝐶) ≤ 0)
165	94	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
166	22	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐶 ∈ ℝ)
167	165, 166	suble0d 10618	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((((ℝ D 𝐹)‘𝑥) − 𝐶) ≤ 0 ↔ ((ℝ D 𝐹)‘𝑥) ≤ 𝐶))
168	164, 167	mpbid 222	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) ≤ 𝐶)
169		elicc2 12238	. . . . . . . . . . . . . 14 ⊢ ((((ℝ D 𝐹)‘𝑁) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑀) ∈ ℝ) → (𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)) ↔ (𝐶 ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ≤ 𝐶 ∧ 𝐶 ≤ ((ℝ D 𝐹)‘𝑀))))
170	16, 18, 169	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)) ↔ (𝐶 ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ≤ 𝐶 ∧ 𝐶 ≤ ((ℝ D 𝐹)‘𝑀))))
171	21, 170	mpbid 222	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ≤ 𝐶 ∧ 𝐶 ≤ ((ℝ D 𝐹)‘𝑀)))
172	171	simp3d 1075	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ≤ ((ℝ D 𝐹)‘𝑀))
173	172	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐶 ≤ ((ℝ D 𝐹)‘𝑀))
174	130	fveq2d 6195	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) = ((ℝ D 𝐹)‘𝑀))
175	173, 174	breqtrrd 4681	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐶 ≤ ((ℝ D 𝐹)‘𝑥))
176	165, 166	letri3d 10179	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (((ℝ D 𝐹)‘𝑥) = 𝐶 ↔ (((ℝ D 𝐹)‘𝑥) ≤ 𝐶 ∧ 𝐶 ≤ ((ℝ D 𝐹)‘𝑥))))
177	168, 175, 176	mpbir2and 957	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) = 𝐶)
178	177	exp32 631	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 = 𝑀 → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶)))
179		simprl 794	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 = 𝑁)
180	179	fveq2d 6195	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) = ((ℝ D 𝐹)‘𝑁))
181	171	simp2d 1074	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℝ D 𝐹)‘𝑁) ≤ 𝐶)
182	181	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑁) ≤ 𝐶)
183	180, 182	eqbrtrd 4675	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) ≤ 𝐶)
184	29	ad2antrr 762	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
185	1	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝐴(,)𝐵) ⊆ ℝ)
186	3	rexrd 10089	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ^*)
187		elioo2 12216	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝑁 ∈ (𝑀(,)𝐵) ↔ (𝑁 ∈ ℝ ∧ 𝑀 < 𝑁 ∧ 𝑁 < 𝐵)))
188	186, 145, 187	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 ∈ (𝑀(,)𝐵) ↔ (𝑁 ∈ ℝ ∧ 𝑀 < 𝑁 ∧ 𝑁 < 𝐵)))
189	5, 6, 148, 188	mpbir3and 1245	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ (𝑀(,)𝐵))
190	189	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑁 ∈ (𝑀(,)𝐵))
191	179, 190	eqeltrd 2701	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ (𝑀(,)𝐵))
192		xrltle 11982	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝑀 ∈ ℝ^*) → (𝐴 < 𝑀 → 𝐴 ≤ 𝑀))
193	138, 186, 192	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 < 𝑀 → 𝐴 ≤ 𝑀))
194	133, 193	mpd 15	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≤ 𝑀)
195		iooss1 12210	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≤ 𝑀) → (𝑀(,)𝐵) ⊆ (𝐴(,)𝐵))
196	138, 194, 195	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀(,)𝐵) ⊆ (𝐴(,)𝐵))
197	196	ad2antrr 762	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝑀(,)𝐵) ⊆ (𝐴(,)𝐵))
198	92	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ (𝐴(,)𝐵))
199	73	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
200	198, 199	eleqtrrd 2704	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ dom (ℝ D 𝐺))
201		simprr 796	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))
202	201, 119	sylib 208	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥))
203	179	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝑀(,)𝑥) = (𝑀(,)𝑁))
204	203	raleqdv 3144	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (∀𝑤 ∈ (𝑀(,)𝑥)(𝐺‘𝑤) ≤ (𝐺‘𝑥) ↔ ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥)))
205	202, 204	mpbird 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑤 ∈ (𝑀(,)𝑥)(𝐺‘𝑤) ≤ (𝐺‘𝑥))
206	184, 185, 191, 197, 200, 205	dvferm2 23750	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 0 ≤ ((ℝ D 𝐺)‘𝑥))
207	106	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐺)‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
208	206, 207	breqtrd 4679	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 0 ≤ (((ℝ D 𝐹)‘𝑥) − 𝐶))
209	94	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
210	22	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐶 ∈ ℝ)
211	209, 210	subge0d 10617	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (0 ≤ (((ℝ D 𝐹)‘𝑥) − 𝐶) ↔ 𝐶 ≤ ((ℝ D 𝐹)‘𝑥)))
212	208, 211	mpbid 222	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐶 ≤ ((ℝ D 𝐹)‘𝑥))
213	209, 210	letri3d 10179	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (((ℝ D 𝐹)‘𝑥) = 𝐶 ↔ (((ℝ D 𝐹)‘𝑥) ≤ 𝐶 ∧ 𝐶 ≤ ((ℝ D 𝐹)‘𝑥))))
214	183, 212, 213	mpbir2and 957	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) = 𝐶)
215	214	exp32 631	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 = 𝑁 → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶)))
216	178, 215	jaod 395	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((𝑥 = 𝑀 ∨ 𝑥 = 𝑁) → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶)))
217	126, 216	syl5bi 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 ∈ {𝑀, 𝑁} → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶)))
218		elun 3753	. . . . . . 7 ⊢ (𝑥 ∈ ((𝑀(,)𝑁) ∪ {𝑀, 𝑁}) ↔ (𝑥 ∈ (𝑀(,)𝑁) ∨ 𝑥 ∈ {𝑀, 𝑁}))
219		prunioo 12301	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝑁 ∈ ℝ^* ∧ 𝑀 ≤ 𝑁) → ((𝑀(,)𝑁) ∪ {𝑀, 𝑁}) = (𝑀[,]𝑁))
220	186, 139, 7, 219	syl3anc 1326	. . . . . . . 8 ⊢ (𝜑 → ((𝑀(,)𝑁) ∪ {𝑀, 𝑁}) = (𝑀[,]𝑁))
221	220	eleq2d 2687	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ((𝑀(,)𝑁) ∪ {𝑀, 𝑁}) ↔ 𝑥 ∈ (𝑀[,]𝑁)))
222	218, 221	syl5bbr 274	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝑀(,)𝑁) ∨ 𝑥 ∈ {𝑀, 𝑁}) ↔ 𝑥 ∈ (𝑀[,]𝑁)))
223	222	biimpar 502	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ∨ 𝑥 ∈ {𝑀, 𝑁}))
224	124, 217, 223	mpjaod 396	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶))
225	91, 224	syld 47	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶))
226	225	reximdva 3017	. 2 ⊢ (𝜑 → (∃𝑥 ∈ (𝑀[,]𝑁)∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) → ∃𝑥 ∈ (𝑀[,]𝑁)((ℝ D 𝐹)‘𝑥) = 𝐶))
227	82, 226	mpd 15	1 ⊢ (𝜑 → ∃𝑥 ∈ (𝑀[,]𝑁)((ℝ D 𝐹)‘𝑥) = 𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 Vcvv 3200 ∪ cun 3572 ⊆ wss 3574 ∅c0 3915 {cpr 4179 class class class wbr 4653 ↦ cmpt 4729 dom cdm 5114 ran crn 5115 ↾ cres 5116 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 · cmul 9941 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 (,)cioo 12175 [,]cicc 12178 TopOpenctopn 16082 topGenctg 16098 ℂ_fldccnfld 19746 –cn→ccncf 22679 D cdv 23627

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631

This theorem is referenced by: dvivthlem2 23772

W3C validator