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

Theorem dvivthlem1 24177
 Description: Lemma for dvivth 24179. (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.
StepHypRef Expression
1 ioossre 12530 . . . . 5 (𝐴(,)𝐵) ⊆ ℝ
2 dvivth.1 . . . . 5 (𝜑𝑀 ∈ (𝐴(,)𝐵))
31, 2sseldi 3825 . . . 4 (𝜑𝑀 ∈ ℝ)
4 dvivth.2 . . . . 5 (𝜑𝑁 ∈ (𝐴(,)𝐵))
51, 4sseldi 3825 . . . 4 (𝜑𝑁 ∈ ℝ)
6 dvivth.5 . . . . 5 (𝜑𝑀 < 𝑁)
73, 5, 6ltled 10511 . . . 4 (𝜑𝑀𝑁)
8 dvivth.3 . . . . . . . . . 10 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
9 cncff 23073 . . . . . . . . . 10 (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
108, 9syl 17 . . . . . . . . 9 (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
1110ffvelrnda 6613 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐹𝑦) ∈ ℝ)
12 dvfre 24120 . . . . . . . . . . . . . 14 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
1310, 1, 12sylancl 580 . . . . . . . . . . . . 13 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
14 dvivth.4 . . . . . . . . . . . . . 14 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
154, 14eleqtrrd 2909 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ dom (ℝ D 𝐹))
1613, 15ffvelrnd 6614 . . . . . . . . . . . 12 (𝜑 → ((ℝ D 𝐹)‘𝑁) ∈ ℝ)
172, 14eleqtrrd 2909 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ dom (ℝ D 𝐹))
1813, 17ffvelrnd 6614 . . . . . . . . . . . 12 (𝜑 → ((ℝ D 𝐹)‘𝑀) ∈ ℝ)
19 iccssre 12550 . . . . . . . . . . . 12 ((((ℝ D 𝐹)‘𝑁) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑀) ∈ ℝ) → (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)) ⊆ ℝ)
2016, 18, 19syl2anc 579 . . . . . . . . . . 11 (𝜑 → (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)) ⊆ ℝ)
21 dvivth.6 . . . . . . . . . . 11 (𝜑𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)))
2220, 21sseldd 3828 . . . . . . . . . 10 (𝜑𝐶 ∈ ℝ)
2322adantr 474 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ)
241a1i 11 . . . . . . . . . 10 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
2524sselda 3827 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℝ)
2623, 25remulcld 10394 . . . . . . . 8 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐶 · 𝑦) ∈ ℝ)
2711, 26resubcld 10789 . . . . . . 7 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((𝐹𝑦) − (𝐶 · 𝑦)) ∈ ℝ)
28 dvivth.7 . . . . . . 7 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑦) − (𝐶 · 𝑦)))
2927, 28fmptd 6638 . . . . . 6 (𝜑𝐺:(𝐴(,)𝐵)⟶ℝ)
30 iccssioo2 12541 . . . . . . 7 ((𝑀 ∈ (𝐴(,)𝐵) ∧ 𝑁 ∈ (𝐴(,)𝐵)) → (𝑀[,]𝑁) ⊆ (𝐴(,)𝐵))
312, 4, 30syl2anc 579 . . . . . 6 (𝜑 → (𝑀[,]𝑁) ⊆ (𝐴(,)𝐵))
3229, 31fssresd 6312 . . . . 5 (𝜑 → (𝐺 ↾ (𝑀[,]𝑁)):(𝑀[,]𝑁)⟶ℝ)
33 ax-resscn 10316 . . . . . 6 ℝ ⊆ ℂ
3433a1i 11 . . . . . . . 8 (𝜑 → ℝ ⊆ ℂ)
35 fss 6295 . . . . . . . . 9 ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
3629, 33, 35sylancl 580 . . . . . . . 8 (𝜑𝐺:(𝐴(,)𝐵)⟶ℂ)
3728oveq2i 6921 . . . . . . . . . . 11 (ℝ D 𝐺) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑦) − (𝐶 · 𝑦))))
38 reelprrecn 10351 . . . . . . . . . . . . 13 ℝ ∈ {ℝ, ℂ}
3938a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ {ℝ, ℂ})
4011recnd 10392 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐹𝑦) ∈ ℂ)
4114feq2d 6268 . . . . . . . . . . . . . 14 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ))
4213, 41mpbid 224 . . . . . . . . . . . . 13 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ)
4342ffvelrnda 6613 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑦) ∈ ℝ)
4410feqmptd 6500 . . . . . . . . . . . . . 14 (𝜑𝐹 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦)))
4544oveq2d 6926 . . . . . . . . . . . . 13 (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦))))
4642feqmptd 6500 . . . . . . . . . . . . 13 (𝜑 → (ℝ D 𝐹) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
4745, 46eqtr3d 2863 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦)))
4826recnd 10392 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → (𝐶 · 𝑦) ∈ ℂ)
49 remulcl 10344 . . . . . . . . . . . . . . 15 ((𝐶 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐶 · 𝑦) ∈ ℝ)
5022, 49sylan 575 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → (𝐶 · 𝑦) ∈ ℝ)
5150recnd 10392 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝐶 · 𝑦) ∈ ℂ)
5222adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → 𝐶 ∈ ℝ)
5334sselda 3827 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
54 1cnd 10358 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → 1 ∈ ℂ)
5539dvmptid 24126 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
5622recnd 10392 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℂ)
5739, 53, 54, 55, 56dvmptcmul 24133 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (𝐶 · 𝑦))) = (𝑦 ∈ ℝ ↦ (𝐶 · 1)))
5856mulid1d 10381 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 · 1) = 𝐶)
5958mpteq2dv 4970 . . . . . . . . . . . . . 14 (𝜑 → (𝑦 ∈ ℝ ↦ (𝐶 · 1)) = (𝑦 ∈ ℝ ↦ 𝐶))
6057, 59eqtrd 2861 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (𝐶 · 𝑦))) = (𝑦 ∈ ℝ ↦ 𝐶))
61 eqid 2825 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
6261tgioo2 22983 . . . . . . . . . . . . 13 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
63 iooretop 22946 . . . . . . . . . . . . . 14 (𝐴(,)𝐵) ∈ (topGen‘ran (,))
6463a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran (,)))
6539, 51, 52, 60, 24, 62, 61, 64dvmptres 24132 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐶 · 𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 𝐶))
6639, 40, 43, 47, 48, 23, 65dvmptsub 24136 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑦) − (𝐶 · 𝑦)))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)))
6737, 66syl5eq 2873 . . . . . . . . . 10 (𝜑 → (ℝ D 𝐺) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)))
6867dmeqd 5562 . . . . . . . . 9 (𝜑 → dom (ℝ D 𝐺) = dom (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)))
69 dmmptg 5877 . . . . . . . . . 10 (∀𝑦 ∈ (𝐴(,)𝐵)(((ℝ D 𝐹)‘𝑦) − 𝐶) ∈ V → dom (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)) = (𝐴(,)𝐵))
70 ovex 6942 . . . . . . . . . . 11 (((ℝ D 𝐹)‘𝑦) − 𝐶) ∈ V
7170a1i 11 . . . . . . . . . 10 (𝑦 ∈ (𝐴(,)𝐵) → (((ℝ D 𝐹)‘𝑦) − 𝐶) ∈ V)
7269, 71mprg 3135 . . . . . . . . 9 dom (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)) = (𝐴(,)𝐵)
7368, 72syl6eq 2877 . . . . . . . 8 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
74 dvcn 24090 . . . . . . . 8 (((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐺) = (𝐴(,)𝐵)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
7534, 36, 24, 73, 74syl31anc 1496 . . . . . . 7 (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
76 rescncf 23077 . . . . . . 7 ((𝑀[,]𝑁) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ) → (𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)))
7731, 75, 76sylc 65 . . . . . 6 (𝜑 → (𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ))
78 cncffvrn 23078 . . . . . 6 ((ℝ ⊆ ℂ ∧ (𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) → ((𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℝ) ↔ (𝐺 ↾ (𝑀[,]𝑁)):(𝑀[,]𝑁)⟶ℝ))
7933, 77, 78sylancr 581 . . . . 5 (𝜑 → ((𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℝ) ↔ (𝐺 ↾ (𝑀[,]𝑁)):(𝑀[,]𝑁)⟶ℝ))
8032, 79mpbird 249 . . . 4 (𝜑 → (𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℝ))
813, 5, 7, 80evthicc 23632 . . 3 (𝜑 → (∃𝑥 ∈ (𝑀[,]𝑁)∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ∧ ∃𝑥 ∈ (𝑀[,]𝑁)∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑧)))
8281simpld 490 . 2 (𝜑 → ∃𝑥 ∈ (𝑀[,]𝑁)∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥))
83 fvres 6456 . . . . . . . 8 (𝑧 ∈ (𝑀[,]𝑁) → ((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) = (𝐺𝑧))
84 fvres 6456 . . . . . . . 8 (𝑥 ∈ (𝑀[,]𝑁) → ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) = (𝐺𝑥))
8583, 84breqan12rd 4892 . . . . . . 7 ((𝑥 ∈ (𝑀[,]𝑁) ∧ 𝑧 ∈ (𝑀[,]𝑁)) → (((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ↔ (𝐺𝑧) ≤ (𝐺𝑥)))
8685ralbidva 3194 . . . . . 6 (𝑥 ∈ (𝑀[,]𝑁) → (∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ↔ ∀𝑧 ∈ (𝑀[,]𝑁)(𝐺𝑧) ≤ (𝐺𝑥)))
8786adantl 475 . . . . 5 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → (∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ↔ ∀𝑧 ∈ (𝑀[,]𝑁)(𝐺𝑧) ≤ (𝐺𝑥)))
88 ioossicc 12554 . . . . . 6 (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)
89 ssralv 3891 . . . . . 6 ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → (∀𝑧 ∈ (𝑀[,]𝑁)(𝐺𝑧) ≤ (𝐺𝑥) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥)))
9088, 89ax-mp 5 . . . . 5 (∀𝑧 ∈ (𝑀[,]𝑁)(𝐺𝑧) ≤ (𝐺𝑥) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))
9187, 90syl6bi 245 . . . 4 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → (∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥)))
9231sselda 3827 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → 𝑥 ∈ (𝐴(,)𝐵))
9342ffvelrnda 6613 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
9492, 93syldan 585 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
9594recnd 10392 . . . . . . . 8 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
9695adantr 474 . . . . . . 7 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
9756ad2antrr 717 . . . . . . 7 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝐶 ∈ ℂ)
9867fveq1d 6439 . . . . . . . . . . 11 (𝜑 → ((ℝ D 𝐺)‘𝑥) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))‘𝑥))
9998adantr 474 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → ((ℝ D 𝐺)‘𝑥) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))‘𝑥))
100 fveq2 6437 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘𝑥))
101100oveq1d 6925 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (((ℝ D 𝐹)‘𝑦) − 𝐶) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
102 eqid 2825 . . . . . . . . . . . 12 (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))
103 ovex 6942 . . . . . . . . . . . 12 (((ℝ D 𝐹)‘𝑥) − 𝐶) ∈ V
104101, 102, 103fvmpt 6533 . . . . . . . . . . 11 (𝑥 ∈ (𝐴(,)𝐵) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
10592, 104syl 17 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
10699, 105eqtrd 2861 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → ((ℝ D 𝐺)‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
107106adantr 474 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐺)‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
10829ad2antrr 717 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
1091a1i 11 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (𝐴(,)𝐵) ⊆ ℝ)
110 simprl 787 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝑥 ∈ (𝑀(,)𝑁))
11188, 31syl5ss 3838 . . . . . . . . . 10 (𝜑 → (𝑀(,)𝑁) ⊆ (𝐴(,)𝐵))
112111ad2antrr 717 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (𝑀(,)𝑁) ⊆ (𝐴(,)𝐵))
11392adantr 474 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝑥 ∈ (𝐴(,)𝐵))
11473ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
115113, 114eleqtrrd 2909 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝑥 ∈ dom (ℝ D 𝐺))
116 simprr 789 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))
117 fveq2 6437 . . . . . . . . . . . 12 (𝑧 = 𝑤 → (𝐺𝑧) = (𝐺𝑤))
118117breq1d 4885 . . . . . . . . . . 11 (𝑧 = 𝑤 → ((𝐺𝑧) ≤ (𝐺𝑥) ↔ (𝐺𝑤) ≤ (𝐺𝑥)))
119118cbvralv 3383 . . . . . . . . . 10 (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥) ↔ ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺𝑤) ≤ (𝐺𝑥))
120116, 119sylib 210 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺𝑤) ≤ (𝐺𝑥))
121108, 109, 110, 112, 115, 120dvferm 24157 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐺)‘𝑥) = 0)
122107, 121eqtr3d 2863 . . . . . . 7 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (((ℝ D 𝐹)‘𝑥) − 𝐶) = 0)
12396, 97, 122subeq0d 10728 . . . . . 6 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐹)‘𝑥) = 𝐶)
124123exp32 413 . . . . 5 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶)))
125 vex 3417 . . . . . . 7 𝑥 ∈ V
126125elpr 4422 . . . . . 6 (𝑥 ∈ {𝑀, 𝑁} ↔ (𝑥 = 𝑀𝑥 = 𝑁))
127106adantr 474 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐺)‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
12829ad2antrr 717 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
1291a1i 11 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (𝐴(,)𝐵) ⊆ ℝ)
130 simprl 787 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝑥 = 𝑀)
131 eliooord 12528 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑀𝑀 < 𝐵))
1322, 131syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 < 𝑀𝑀 < 𝐵))
133132simpld 490 . . . . . . . . . . . . . . 15 (𝜑𝐴 < 𝑀)
134 ne0i 4152 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
135 ndmioo 12497 . . . . . . . . . . . . . . . . . . 19 (¬ (𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = ∅)
136135necon1ai 3026 . . . . . . . . . . . . . . . . . 18 ((𝐴(,)𝐵) ≠ ∅ → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*))
1372, 134, 1363syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*))
138137simpld 490 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℝ*)
1395rexrd 10413 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℝ*)
140 elioo2 12511 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ*𝑁 ∈ ℝ*) → (𝑀 ∈ (𝐴(,)𝑁) ↔ (𝑀 ∈ ℝ ∧ 𝐴 < 𝑀𝑀 < 𝑁)))
141138, 139, 140syl2anc 579 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 ∈ (𝐴(,)𝑁) ↔ (𝑀 ∈ ℝ ∧ 𝐴 < 𝑀𝑀 < 𝑁)))
1423, 133, 6, 141mpbir3and 1446 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (𝐴(,)𝑁))
143142ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝑀 ∈ (𝐴(,)𝑁))
144130, 143eqeltrd 2906 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝑥 ∈ (𝐴(,)𝑁))
145137simprd 491 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ ℝ*)
146 eliooord 12528 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑁𝑁 < 𝐵))
1474, 146syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 < 𝑁𝑁 < 𝐵))
148147simprd 491 . . . . . . . . . . . . . . 15 (𝜑𝑁 < 𝐵)
149139, 145, 148xrltled 12276 . . . . . . . . . . . . . 14 (𝜑𝑁𝐵)
150 iooss2 12506 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℝ*𝑁𝐵) → (𝐴(,)𝑁) ⊆ (𝐴(,)𝐵))
151145, 149, 150syl2anc 579 . . . . . . . . . . . . 13 (𝜑 → (𝐴(,)𝑁) ⊆ (𝐴(,)𝐵))
152151ad2antrr 717 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (𝐴(,)𝑁) ⊆ (𝐴(,)𝐵))
15392adantr 474 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝑥 ∈ (𝐴(,)𝐵))
15473ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
155153, 154eleqtrrd 2909 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝑥 ∈ dom (ℝ D 𝐺))
156 simprr 789 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))
157156, 119sylib 210 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺𝑤) ≤ (𝐺𝑥))
158130oveq1d 6925 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (𝑥(,)𝑁) = (𝑀(,)𝑁))
159158raleqdv 3356 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (∀𝑤 ∈ (𝑥(,)𝑁)(𝐺𝑤) ≤ (𝐺𝑥) ↔ ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺𝑤) ≤ (𝐺𝑥)))
160157, 159mpbird 249 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ∀𝑤 ∈ (𝑥(,)𝑁)(𝐺𝑤) ≤ (𝐺𝑥))
161128, 129, 144, 152, 155, 160dvferm1 24154 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐺)‘𝑥) ≤ 0)
162127, 161eqbrtrrd 4899 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (((ℝ D 𝐹)‘𝑥) − 𝐶) ≤ 0)
16394adantr 474 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
16422ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝐶 ∈ ℝ)
165163, 164suble0d 10950 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((((ℝ D 𝐹)‘𝑥) − 𝐶) ≤ 0 ↔ ((ℝ D 𝐹)‘𝑥) ≤ 𝐶))
166162, 165mpbid 224 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐹)‘𝑥) ≤ 𝐶)
167 elicc2 12533 . . . . . . . . . . . . . 14 ((((ℝ D 𝐹)‘𝑁) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑀) ∈ ℝ) → (𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)) ↔ (𝐶 ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ≤ 𝐶𝐶 ≤ ((ℝ D 𝐹)‘𝑀))))
16816, 18, 167syl2anc 579 . . . . . . . . . . . . 13 (𝜑 → (𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)) ↔ (𝐶 ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ≤ 𝐶𝐶 ≤ ((ℝ D 𝐹)‘𝑀))))
16921, 168mpbid 224 . . . . . . . . . . . 12 (𝜑 → (𝐶 ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ≤ 𝐶𝐶 ≤ ((ℝ D 𝐹)‘𝑀)))
170169simp3d 1178 . . . . . . . . . . 11 (𝜑𝐶 ≤ ((ℝ D 𝐹)‘𝑀))
171170ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝐶 ≤ ((ℝ D 𝐹)‘𝑀))
172130fveq2d 6441 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐹)‘𝑥) = ((ℝ D 𝐹)‘𝑀))
173171, 172breqtrrd 4903 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝐶 ≤ ((ℝ D 𝐹)‘𝑥))
174163, 164letri3d 10505 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (((ℝ D 𝐹)‘𝑥) = 𝐶 ↔ (((ℝ D 𝐹)‘𝑥) ≤ 𝐶𝐶 ≤ ((ℝ D 𝐹)‘𝑥))))
175166, 173, 174mpbir2and 704 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐹)‘𝑥) = 𝐶)
176175exp32 413 . . . . . . 7 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 = 𝑀 → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶)))
177 simprl 787 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝑥 = 𝑁)
178177fveq2d 6441 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐹)‘𝑥) = ((ℝ D 𝐹)‘𝑁))
179169simp2d 1177 . . . . . . . . . . 11 (𝜑 → ((ℝ D 𝐹)‘𝑁) ≤ 𝐶)
180179ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐹)‘𝑁) ≤ 𝐶)
181178, 180eqbrtrd 4897 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐹)‘𝑥) ≤ 𝐶)
18229ad2antrr 717 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝐺:(𝐴(,)𝐵)⟶ℝ)
1831a1i 11 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (𝐴(,)𝐵) ⊆ ℝ)
1843rexrd 10413 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℝ*)
185 elioo2 12511 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑁 ∈ (𝑀(,)𝐵) ↔ (𝑁 ∈ ℝ ∧ 𝑀 < 𝑁𝑁 < 𝐵)))
186184, 145, 185syl2anc 579 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 ∈ (𝑀(,)𝐵) ↔ (𝑁 ∈ ℝ ∧ 𝑀 < 𝑁𝑁 < 𝐵)))
1875, 6, 148, 186mpbir3and 1446 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ (𝑀(,)𝐵))
188187ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝑁 ∈ (𝑀(,)𝐵))
189177, 188eqeltrd 2906 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝑥 ∈ (𝑀(,)𝐵))
190138, 184, 133xrltled 12276 . . . . . . . . . . . . . 14 (𝜑𝐴𝑀)
191 iooss1 12505 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐴𝑀) → (𝑀(,)𝐵) ⊆ (𝐴(,)𝐵))
192138, 190, 191syl2anc 579 . . . . . . . . . . . . 13 (𝜑 → (𝑀(,)𝐵) ⊆ (𝐴(,)𝐵))
193192ad2antrr 717 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (𝑀(,)𝐵) ⊆ (𝐴(,)𝐵))
19492adantr 474 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝑥 ∈ (𝐴(,)𝐵))
19573ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
196194, 195eleqtrrd 2909 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝑥 ∈ dom (ℝ D 𝐺))
197 simprr 789 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))
198197, 119sylib 210 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺𝑤) ≤ (𝐺𝑥))
199177oveq2d 6926 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (𝑀(,)𝑥) = (𝑀(,)𝑁))
200199raleqdv 3356 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (∀𝑤 ∈ (𝑀(,)𝑥)(𝐺𝑤) ≤ (𝐺𝑥) ↔ ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺𝑤) ≤ (𝐺𝑥)))
201198, 200mpbird 249 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ∀𝑤 ∈ (𝑀(,)𝑥)(𝐺𝑤) ≤ (𝐺𝑥))
202182, 183, 189, 193, 196, 201dvferm2 24156 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 0 ≤ ((ℝ D 𝐺)‘𝑥))
203106adantr 474 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐺)‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶))
204202, 203breqtrd 4901 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 0 ≤ (((ℝ D 𝐹)‘𝑥) − 𝐶))
20594adantr 474 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
20622ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝐶 ∈ ℝ)
207205, 206subge0d 10949 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (0 ≤ (((ℝ D 𝐹)‘𝑥) − 𝐶) ↔ 𝐶 ≤ ((ℝ D 𝐹)‘𝑥)))
208204, 207mpbid 224 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → 𝐶 ≤ ((ℝ D 𝐹)‘𝑥))
209205, 206letri3d 10505 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → (((ℝ D 𝐹)‘𝑥) = 𝐶 ↔ (((ℝ D 𝐹)‘𝑥) ≤ 𝐶𝐶 ≤ ((ℝ D 𝐹)‘𝑥))))
210181, 208, 209mpbir2and 704 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥))) → ((ℝ D 𝐹)‘𝑥) = 𝐶)
211210exp32 413 . . . . . . 7 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 = 𝑁 → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶)))
212176, 211jaod 890 . . . . . 6 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → ((𝑥 = 𝑀𝑥 = 𝑁) → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶)))
213126, 212syl5bi 234 . . . . 5 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 ∈ {𝑀, 𝑁} → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶)))
214 elun 3982 . . . . . . 7 (𝑥 ∈ ((𝑀(,)𝑁) ∪ {𝑀, 𝑁}) ↔ (𝑥 ∈ (𝑀(,)𝑁) ∨ 𝑥 ∈ {𝑀, 𝑁}))
215 prunioo 12601 . . . . . . . . 9 ((𝑀 ∈ ℝ*𝑁 ∈ ℝ*𝑀𝑁) → ((𝑀(,)𝑁) ∪ {𝑀, 𝑁}) = (𝑀[,]𝑁))
216184, 139, 7, 215syl3anc 1494 . . . . . . . 8 (𝜑 → ((𝑀(,)𝑁) ∪ {𝑀, 𝑁}) = (𝑀[,]𝑁))
217216eleq2d 2892 . . . . . . 7 (𝜑 → (𝑥 ∈ ((𝑀(,)𝑁) ∪ {𝑀, 𝑁}) ↔ 𝑥 ∈ (𝑀[,]𝑁)))
218214, 217syl5bbr 277 . . . . . 6 (𝜑 → ((𝑥 ∈ (𝑀(,)𝑁) ∨ 𝑥 ∈ {𝑀, 𝑁}) ↔ 𝑥 ∈ (𝑀[,]𝑁)))
219218biimpar 471 . . . . 5 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ∨ 𝑥 ∈ {𝑀, 𝑁}))
220124, 213, 219mpjaod 891 . . . 4 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺𝑧) ≤ (𝐺𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶))
22191, 220syld 47 . . 3 ((𝜑𝑥 ∈ (𝑀[,]𝑁)) → (∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶))
222221reximdva 3225 . 2 (𝜑 → (∃𝑥 ∈ (𝑀[,]𝑁)∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) → ∃𝑥 ∈ (𝑀[,]𝑁)((ℝ D 𝐹)‘𝑥) = 𝐶))
22382, 222mpd 15 1 (𝜑 → ∃𝑥 ∈ (𝑀[,]𝑁)((ℝ D 𝐹)‘𝑥) = 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 878   ∧ w3a 1111   = wceq 1656   ∈ wcel 2164   ≠ wne 2999  ∀wral 3117  ∃wrex 3118  Vcvv 3414   ∪ cun 3796   ⊆ wss 3798  ∅c0 4146  {cpr 4401   class class class wbr 4875   ↦ cmpt 4954  dom cdm 5346  ran crn 5347   ↾ cres 5348  ⟶wf 6123  ‘cfv 6127  (class class class)co 6910  ℂcc 10257  ℝcr 10258  0cc0 10259  1c1 10260   · cmul 10264  ℝ*cxr 10397   < clt 10398   ≤ cle 10399   − cmin 10592  (,)cioo 12470  [,]cicc 12473  TopOpenctopn 16442  topGenctg 16458  ℂfldccnfld 20113  –cn→ccncf 23056   D cdv 24033 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4996  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214  ax-inf2 8822  ax-cnex 10315  ax-resscn 10316  ax-1cn 10317  ax-icn 10318  ax-addcl 10319  ax-addrcl 10320  ax-mulcl 10321  ax-mulrcl 10322  ax-mulcom 10323  ax-addass 10324  ax-mulass 10325  ax-distr 10326  ax-i2m1 10327  ax-1ne0 10328  ax-1rid 10329  ax-rnegex 10330  ax-rrecex 10331  ax-cnre 10332  ax-pre-lttri 10333  ax-pre-lttrn 10334  ax-pre-ltadd 10335  ax-pre-mulgt0 10336  ax-pre-sup 10337  ax-addf 10338  ax-mulf 10339 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-int 4700  df-iun 4744  df-iin 4745  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-se 5306  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-isom 6136  df-riota 6871  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-of 7162  df-om 7332  df-1st 7433  df-2nd 7434  df-supp 7565  df-wrecs 7677  df-recs 7739  df-rdg 7777  df-1o 7831  df-2o 7832  df-oadd 7835  df-er 8014  df-map 8129  df-pm 8130  df-ixp 8182  df-en 8229  df-dom 8230  df-sdom 8231  df-fin 8232  df-fsupp 8551  df-fi 8592  df-sup 8623  df-inf 8624  df-oi 8691  df-card 9085  df-cda 9312  df-pnf 10400  df-mnf 10401  df-xr 10402  df-ltxr 10403  df-le 10404  df-sub 10594  df-neg 10595  df-div 11017  df-nn 11358  df-2 11421  df-3 11422  df-4 11423  df-5 11424  df-6 11425  df-7 11426  df-8 11427  df-9 11428  df-n0 11626  df-z 11712  df-dec 11829  df-uz 11976  df-q 12079  df-rp 12120  df-xneg 12239  df-xadd 12240  df-xmul 12241  df-ioo 12474  df-ico 12476  df-icc 12477  df-fz 12627  df-fzo 12768  df-seq 13103  df-exp 13162  df-hash 13418  df-cj 14223  df-re 14224  df-im 14225  df-sqrt 14359  df-abs 14360  df-struct 16231  df-ndx 16232  df-slot 16233  df-base 16235  df-sets 16236  df-ress 16237  df-plusg 16325  df-mulr 16326  df-starv 16327  df-sca 16328  df-vsca 16329  df-ip 16330  df-tset 16331  df-ple 16332  df-ds 16334  df-unif 16335  df-hom 16336  df-cco 16337  df-rest 16443  df-topn 16444  df-0g 16462  df-gsum 16463  df-topgen 16464  df-pt 16465  df-prds 16468  df-xrs 16522  df-qtop 16527  df-imas 16528  df-xps 16530  df-mre 16606  df-mrc 16607  df-acs 16609  df-mgm 17602  df-sgrp 17644  df-mnd 17655  df-submnd 17696  df-mulg 17902  df-cntz 18107  df-cmn 18555  df-psmet 20105  df-xmet 20106  df-met 20107  df-bl 20108  df-mopn 20109  df-fbas 20110  df-fg 20111  df-cnfld 20114  df-top 21076  df-topon 21093  df-topsp 21115  df-bases 21128  df-cld 21201  df-ntr 21202  df-cls 21203  df-nei 21280  df-lp 21318  df-perf 21319  df-cn 21409  df-cnp 21410  df-haus 21497  df-cmp 21568  df-tx 21743  df-hmeo 21936  df-fil 22027  df-fm 22119  df-flim 22120  df-flf 22121  df-xms 22502  df-ms 22503  df-tms 22504  df-cncf 23058  df-limc 24036  df-dv 24037 This theorem is referenced by:  dvivthlem2  24178
 Copyright terms: Public domain W3C validator