Step | Hyp | Ref
| Expression |
1 | | ioossre 12106 |
. . . . 5
⊢ (𝐴(,)𝐵) ⊆ ℝ |
2 | | dvivth.1 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵)) |
3 | 1, 2 | sseldi 3566 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℝ) |
4 | | dvivth.2 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵)) |
5 | 1, 4 | sseldi 3566 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℝ) |
6 | | dvivth.5 |
. . . . 5
⊢ (𝜑 → 𝑀 < 𝑁) |
7 | 3, 5, 6 | ltled 10064 |
. . . 4
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
8 | | dvivth.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
9 | | cncff 22504 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
11 | 10 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑦) ∈ ℝ) |
12 | | dvfre 23520 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
13 | 10, 1, 12 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
14 | | dvivth.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
15 | 4, 14 | eleqtrrd 2691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ dom (ℝ D 𝐹)) |
16 | 13, 15 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑁) ∈ ℝ) |
17 | 2, 14 | eleqtrrd 2691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ dom (ℝ D 𝐹)) |
18 | 13, 17 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑀) ∈ ℝ) |
19 | | iccssre 12126 |
. . . . . . . . . . . 12
⊢
((((ℝ D 𝐹)‘𝑁) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑀) ∈ ℝ) → (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)) ⊆ ℝ) |
20 | 16, 18, 19 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)) ⊆ ℝ) |
21 | | dvivth.6 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀))) |
22 | 20, 21 | sseldd 3569 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℝ) |
23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ) |
24 | 1 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
25 | 24 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℝ) |
26 | 23, 25 | remulcld 9949 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐶 · 𝑦) ∈ ℝ) |
27 | 11, 26 | resubcld 10337 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑦) − (𝐶 · 𝑦)) ∈ ℝ) |
28 | | dvivth.7 |
. . . . . . 7
⊢ 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦))) |
29 | 27, 28 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
30 | | iccssioo2 12117 |
. . . . . . 7
⊢ ((𝑀 ∈ (𝐴(,)𝐵) ∧ 𝑁 ∈ (𝐴(,)𝐵)) → (𝑀[,]𝑁) ⊆ (𝐴(,)𝐵)) |
31 | 2, 4, 30 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ (𝐴(,)𝐵)) |
32 | 29, 31 | fssresd 5984 |
. . . . 5
⊢ (𝜑 → (𝐺 ↾ (𝑀[,]𝑁)):(𝑀[,]𝑁)⟶ℝ) |
33 | | ax-resscn 9872 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
34 | 33 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ⊆
ℂ) |
35 | | fss 5969 |
. . . . . . . . 9
⊢ ((𝐺:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
36 | 29, 33, 35 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
37 | 28 | oveq2i 6560 |
. . . . . . . . . . 11
⊢ (ℝ
D 𝐺) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦)))) |
38 | | reelprrecn 9907 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} |
39 | 38 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
40 | 11 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑦) ∈ ℂ) |
41 | 14 | feq2d 5944 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℝ)) |
42 | 13, 41 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ) |
43 | 42 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑦) ∈ ℝ) |
44 | 10 | feqmptd 6159 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦))) |
45 | 44 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦)))) |
46 | 42 | feqmptd 6159 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D 𝐹) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦))) |
47 | 45, 46 | eqtr3d 2646 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑦))) |
48 | 26 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐶 · 𝑦) ∈ ℂ) |
49 | | remulcl 9900 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐶 · 𝑦) ∈ ℝ) |
50 | 22, 49 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐶 · 𝑦) ∈ ℝ) |
51 | 50 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐶 · 𝑦) ∈ ℂ) |
52 | 22 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐶 ∈ ℝ) |
53 | 34 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
54 | | 1cnd 9935 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℂ) |
55 | 39 | dvmptid 23526 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1)) |
56 | 22 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ ℂ) |
57 | 39, 53, 54, 55, 56 | dvmptcmul 23533 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (𝐶 · 𝑦))) = (𝑦 ∈ ℝ ↦ (𝐶 · 1))) |
58 | 56 | mulid1d 9936 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶 · 1) = 𝐶) |
59 | 58 | mpteq2dv 4673 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝐶 · 1)) = (𝑦 ∈ ℝ ↦ 𝐶)) |
60 | 57, 59 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (𝐶 · 𝑦))) = (𝑦 ∈ ℝ ↦ 𝐶)) |
61 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
62 | 61 | tgioo2 22414 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
63 | | iooretop 22379 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
64 | 63 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran
(,))) |
65 | 39, 51, 52, 60, 24, 62, 61, 64 | dvmptres 23532 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝐶 · 𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 𝐶)) |
66 | 39, 40, 43, 47, 48, 23, 65 | dvmptsub 23536 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝐶 · 𝑦)))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))) |
67 | 37, 66 | syl5eq 2656 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D 𝐺) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))) |
68 | 67 | dmeqd 5248 |
. . . . . . . . 9
⊢ (𝜑 → dom (ℝ D 𝐺) = dom (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))) |
69 | | dmmptg 5549 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
(𝐴(,)𝐵)(((ℝ D 𝐹)‘𝑦) − 𝐶) ∈ V → dom (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)) = (𝐴(,)𝐵)) |
70 | | ovex 6577 |
. . . . . . . . . . 11
⊢
(((ℝ D 𝐹)‘𝑦) − 𝐶) ∈ V |
71 | 70 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐴(,)𝐵) → (((ℝ D 𝐹)‘𝑦) − 𝐶) ∈ V) |
72 | 69, 71 | mprg 2910 |
. . . . . . . . 9
⊢ dom
(𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)) = (𝐴(,)𝐵) |
73 | 68, 72 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
74 | | dvcn 23490 |
. . . . . . . 8
⊢
(((ℝ ⊆ ℂ ∧ 𝐺:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D
𝐺) = (𝐴(,)𝐵)) → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
75 | 34, 36, 24, 73, 74 | syl31anc 1321 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
76 | | rescncf 22508 |
. . . . . . 7
⊢ ((𝑀[,]𝑁) ⊆ (𝐴(,)𝐵) → (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ) → (𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ))) |
77 | 31, 75, 76 | sylc 63 |
. . . . . 6
⊢ (𝜑 → (𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) |
78 | | cncffvrn 22509 |
. . . . . 6
⊢ ((ℝ
⊆ ℂ ∧ (𝐺
↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℂ)) → ((𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℝ) ↔ (𝐺 ↾ (𝑀[,]𝑁)):(𝑀[,]𝑁)⟶ℝ)) |
79 | 33, 77, 78 | sylancr 694 |
. . . . 5
⊢ (𝜑 → ((𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℝ) ↔ (𝐺 ↾ (𝑀[,]𝑁)):(𝑀[,]𝑁)⟶ℝ)) |
80 | 32, 79 | mpbird 246 |
. . . 4
⊢ (𝜑 → (𝐺 ↾ (𝑀[,]𝑁)) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
81 | 3, 5, 7, 80 | evthicc 23035 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ (𝑀[,]𝑁)∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ∧ ∃𝑥 ∈ (𝑀[,]𝑁)∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑧))) |
82 | 81 | simpld 474 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ (𝑀[,]𝑁)∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥)) |
83 | | fvres 6117 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝑀[,]𝑁) → ((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) = (𝐺‘𝑧)) |
84 | | fvres 6117 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑀[,]𝑁) → ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) = (𝐺‘𝑥)) |
85 | 83, 84 | breqan12rd 4600 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑀[,]𝑁) ∧ 𝑧 ∈ (𝑀[,]𝑁)) → (((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ↔ (𝐺‘𝑧) ≤ (𝐺‘𝑥))) |
86 | 85 | ralbidva 2968 |
. . . . . 6
⊢ (𝑥 ∈ (𝑀[,]𝑁) → (∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ↔ ∀𝑧 ∈ (𝑀[,]𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) |
87 | 86 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) ↔ ∀𝑧 ∈ (𝑀[,]𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) |
88 | | ioossicc 12130 |
. . . . . 6
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) |
89 | | ssralv 3629 |
. . . . . 6
⊢ ((𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) → (∀𝑧 ∈ (𝑀[,]𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) |
90 | 88, 89 | ax-mp 5 |
. . . . 5
⊢
(∀𝑧 ∈
(𝑀[,]𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥)) |
91 | 87, 90 | syl6bi 242 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) |
92 | 31 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝑥 ∈ (𝐴(,)𝐵)) |
93 | 42 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ) |
94 | 92, 93 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ) |
95 | 94 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) |
96 | 95 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) |
97 | 56 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐶 ∈ ℂ) |
98 | 67 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℝ D 𝐺)‘𝑥) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))‘𝑥)) |
99 | 98 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((ℝ D 𝐺)‘𝑥) = ((𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))‘𝑥)) |
100 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘𝑥)) |
101 | 100 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (((ℝ D 𝐹)‘𝑦) − 𝐶) = (((ℝ D 𝐹)‘𝑥) − 𝐶)) |
102 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶)) |
103 | | ovex 6577 |
. . . . . . . . . . . 12
⊢
(((ℝ D 𝐹)‘𝑥) − 𝐶) ∈ V |
104 | 101, 102,
103 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶)) |
105 | 92, 104 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑦) − 𝐶))‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶)) |
106 | 99, 105 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((ℝ D 𝐺)‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶)) |
107 | 106 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐺)‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶)) |
108 | 29 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
109 | 1 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝐴(,)𝐵) ⊆ ℝ) |
110 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ (𝑀(,)𝑁)) |
111 | 88, 31 | syl5ss 3579 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀(,)𝑁) ⊆ (𝐴(,)𝐵)) |
112 | 111 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝑀(,)𝑁) ⊆ (𝐴(,)𝐵)) |
113 | 92 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ (𝐴(,)𝐵)) |
114 | 73 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
115 | 113, 114 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ dom (ℝ D 𝐺)) |
116 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥)) |
117 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → (𝐺‘𝑧) = (𝐺‘𝑤)) |
118 | 117 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑤 → ((𝐺‘𝑧) ≤ (𝐺‘𝑥) ↔ (𝐺‘𝑤) ≤ (𝐺‘𝑥))) |
119 | 118 | cbvralv 3147 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
(𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) ↔ ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥)) |
120 | 116, 119 | sylib 207 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥)) |
121 | 108, 109,
110, 112, 115, 120 | dvferm 23555 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐺)‘𝑥) = 0) |
122 | 107, 121 | eqtr3d 2646 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (((ℝ D 𝐹)‘𝑥) − 𝐶) = 0) |
123 | 96, 97, 122 | subeq0d 10279 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 ∈ (𝑀(,)𝑁) ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) = 𝐶) |
124 | 123 | exp32 629 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶))) |
125 | | vex 3176 |
. . . . . . 7
⊢ 𝑥 ∈ V |
126 | 125 | elpr 4146 |
. . . . . 6
⊢ (𝑥 ∈ {𝑀, 𝑁} ↔ (𝑥 = 𝑀 ∨ 𝑥 = 𝑁)) |
127 | 106 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐺)‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶)) |
128 | 29 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
129 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝐴(,)𝐵) ⊆ ℝ) |
130 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 = 𝑀) |
131 | | eliooord 12104 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑀 ∧ 𝑀 < 𝐵)) |
132 | 2, 131 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 < 𝑀 ∧ 𝑀 < 𝐵)) |
133 | 132 | simpld 474 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 < 𝑀) |
134 | | ne0i 3880 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅) |
135 | | ndmioo 12073 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
(𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) → (𝐴(,)𝐵) = ∅) |
136 | 135 | necon1ai 2809 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴(,)𝐵) ≠ ∅ → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
137 | 2, 134, 136 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
138 | 137 | simpld 474 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
139 | 5 | rexrd 9968 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
140 | | elioo2 12087 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ*
∧ 𝑁 ∈
ℝ*) → (𝑀 ∈ (𝐴(,)𝑁) ↔ (𝑀 ∈ ℝ ∧ 𝐴 < 𝑀 ∧ 𝑀 < 𝑁))) |
141 | 138, 139,
140 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 ∈ (𝐴(,)𝑁) ↔ (𝑀 ∈ ℝ ∧ 𝐴 < 𝑀 ∧ 𝑀 < 𝑁))) |
142 | 3, 133, 6, 141 | mpbir3and 1238 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝑁)) |
143 | 142 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑀 ∈ (𝐴(,)𝑁)) |
144 | 130, 143 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ (𝐴(,)𝑁)) |
145 | 137 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
146 | | eliooord 12104 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑁 ∧ 𝑁 < 𝐵)) |
147 | 4, 146 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 < 𝑁 ∧ 𝑁 < 𝐵)) |
148 | 147 | simprd 478 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 < 𝐵) |
149 | | xrltle 11858 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑁 < 𝐵 → 𝑁 ≤ 𝐵)) |
150 | 139, 145,
149 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 < 𝐵 → 𝑁 ≤ 𝐵)) |
151 | 148, 150 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ≤ 𝐵) |
152 | | iooss2 12082 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ*
∧ 𝑁 ≤ 𝐵) → (𝐴(,)𝑁) ⊆ (𝐴(,)𝐵)) |
153 | 145, 151,
152 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴(,)𝑁) ⊆ (𝐴(,)𝐵)) |
154 | 153 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝐴(,)𝑁) ⊆ (𝐴(,)𝐵)) |
155 | 92 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ (𝐴(,)𝐵)) |
156 | 73 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
157 | 155, 156 | eleqtrrd 2691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ dom (ℝ D 𝐺)) |
158 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥)) |
159 | 158, 119 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥)) |
160 | 130 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝑥(,)𝑁) = (𝑀(,)𝑁)) |
161 | 160 | raleqdv 3121 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (∀𝑤 ∈ (𝑥(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥) ↔ ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥))) |
162 | 159, 161 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑤 ∈ (𝑥(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥)) |
163 | 128, 129,
144, 154, 157, 162 | dvferm1 23552 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐺)‘𝑥) ≤ 0) |
164 | 127, 163 | eqbrtrrd 4607 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (((ℝ D 𝐹)‘𝑥) − 𝐶) ≤ 0) |
165 | 94 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ) |
166 | 22 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐶 ∈ ℝ) |
167 | 165, 166 | suble0d 10497 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((((ℝ D 𝐹)‘𝑥) − 𝐶) ≤ 0 ↔ ((ℝ D 𝐹)‘𝑥) ≤ 𝐶)) |
168 | 164, 167 | mpbid 221 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) ≤ 𝐶) |
169 | | elicc2 12109 |
. . . . . . . . . . . . . 14
⊢
((((ℝ D 𝐹)‘𝑁) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑀) ∈ ℝ) → (𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)) ↔ (𝐶 ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ≤ 𝐶 ∧ 𝐶 ≤ ((ℝ D 𝐹)‘𝑀)))) |
170 | 16, 18, 169 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶 ∈ (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑀)) ↔ (𝐶 ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ≤ 𝐶 ∧ 𝐶 ≤ ((ℝ D 𝐹)‘𝑀)))) |
171 | 21, 170 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ≤ 𝐶 ∧ 𝐶 ≤ ((ℝ D 𝐹)‘𝑀))) |
172 | 171 | simp3d 1068 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ≤ ((ℝ D 𝐹)‘𝑀)) |
173 | 172 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐶 ≤ ((ℝ D 𝐹)‘𝑀)) |
174 | 130 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) = ((ℝ D 𝐹)‘𝑀)) |
175 | 173, 174 | breqtrrd 4611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐶 ≤ ((ℝ D 𝐹)‘𝑥)) |
176 | 165, 166 | letri3d 10058 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (((ℝ D 𝐹)‘𝑥) = 𝐶 ↔ (((ℝ D 𝐹)‘𝑥) ≤ 𝐶 ∧ 𝐶 ≤ ((ℝ D 𝐹)‘𝑥)))) |
177 | 168, 175,
176 | mpbir2and 959 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑀 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) = 𝐶) |
178 | 177 | exp32 629 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 = 𝑀 → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶))) |
179 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 = 𝑁) |
180 | 179 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) = ((ℝ D 𝐹)‘𝑁)) |
181 | 171 | simp2d 1067 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑁) ≤ 𝐶) |
182 | 181 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑁) ≤ 𝐶) |
183 | 180, 182 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) ≤ 𝐶) |
184 | 29 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐺:(𝐴(,)𝐵)⟶ℝ) |
185 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝐴(,)𝐵) ⊆ ℝ) |
186 | 3 | rexrd 9968 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈
ℝ*) |
187 | | elioo2 12087 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑁 ∈ (𝑀(,)𝐵) ↔ (𝑁 ∈ ℝ ∧ 𝑀 < 𝑁 ∧ 𝑁 < 𝐵))) |
188 | 186, 145,
187 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 ∈ (𝑀(,)𝐵) ↔ (𝑁 ∈ ℝ ∧ 𝑀 < 𝑁 ∧ 𝑁 < 𝐵))) |
189 | 5, 6, 148, 188 | mpbir3and 1238 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ (𝑀(,)𝐵)) |
190 | 189 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑁 ∈ (𝑀(,)𝐵)) |
191 | 179, 190 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ (𝑀(,)𝐵)) |
192 | | xrltle 11858 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ*
∧ 𝑀 ∈
ℝ*) → (𝐴 < 𝑀 → 𝐴 ≤ 𝑀)) |
193 | 138, 186,
192 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 < 𝑀 → 𝐴 ≤ 𝑀)) |
194 | 133, 193 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ≤ 𝑀) |
195 | | iooss1 12081 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≤ 𝑀) → (𝑀(,)𝐵) ⊆ (𝐴(,)𝐵)) |
196 | 138, 194,
195 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀(,)𝐵) ⊆ (𝐴(,)𝐵)) |
197 | 196 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝑀(,)𝐵) ⊆ (𝐴(,)𝐵)) |
198 | 92 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ (𝐴(,)𝐵)) |
199 | 73 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
200 | 198, 199 | eleqtrrd 2691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝑥 ∈ dom (ℝ D 𝐺)) |
201 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥)) |
202 | 201, 119 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥)) |
203 | 179 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (𝑀(,)𝑥) = (𝑀(,)𝑁)) |
204 | 203 | raleqdv 3121 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (∀𝑤 ∈ (𝑀(,)𝑥)(𝐺‘𝑤) ≤ (𝐺‘𝑥) ↔ ∀𝑤 ∈ (𝑀(,)𝑁)(𝐺‘𝑤) ≤ (𝐺‘𝑥))) |
205 | 202, 204 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ∀𝑤 ∈ (𝑀(,)𝑥)(𝐺‘𝑤) ≤ (𝐺‘𝑥)) |
206 | 184, 185,
191, 197, 200, 205 | dvferm2 23554 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 0 ≤ ((ℝ D 𝐺)‘𝑥)) |
207 | 106 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐺)‘𝑥) = (((ℝ D 𝐹)‘𝑥) − 𝐶)) |
208 | 206, 207 | breqtrd 4609 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 0 ≤ (((ℝ D 𝐹)‘𝑥) − 𝐶)) |
209 | 94 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ) |
210 | 22 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐶 ∈ ℝ) |
211 | 209, 210 | subge0d 10496 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (0 ≤ (((ℝ D 𝐹)‘𝑥) − 𝐶) ↔ 𝐶 ≤ ((ℝ D 𝐹)‘𝑥))) |
212 | 208, 211 | mpbid 221 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → 𝐶 ≤ ((ℝ D 𝐹)‘𝑥)) |
213 | 209, 210 | letri3d 10058 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → (((ℝ D 𝐹)‘𝑥) = 𝐶 ↔ (((ℝ D 𝐹)‘𝑥) ≤ 𝐶 ∧ 𝐶 ≤ ((ℝ D 𝐹)‘𝑥)))) |
214 | 183, 212,
213 | mpbir2and 959 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) ∧ (𝑥 = 𝑁 ∧ ∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥))) → ((ℝ D 𝐹)‘𝑥) = 𝐶) |
215 | 214 | exp32 629 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 = 𝑁 → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶))) |
216 | 178, 215 | jaod 394 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → ((𝑥 = 𝑀 ∨ 𝑥 = 𝑁) → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶))) |
217 | 126, 216 | syl5bi 231 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 ∈ {𝑀, 𝑁} → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶))) |
218 | | elun 3715 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝑀(,)𝑁) ∪ {𝑀, 𝑁}) ↔ (𝑥 ∈ (𝑀(,)𝑁) ∨ 𝑥 ∈ {𝑀, 𝑁})) |
219 | | prunioo 12172 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ* ∧ 𝑀
≤ 𝑁) → ((𝑀(,)𝑁) ∪ {𝑀, 𝑁}) = (𝑀[,]𝑁)) |
220 | 186, 139,
7, 219 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀(,)𝑁) ∪ {𝑀, 𝑁}) = (𝑀[,]𝑁)) |
221 | 220 | eleq2d 2673 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ((𝑀(,)𝑁) ∪ {𝑀, 𝑁}) ↔ 𝑥 ∈ (𝑀[,]𝑁))) |
222 | 218, 221 | syl5bbr 273 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝑀(,)𝑁) ∨ 𝑥 ∈ {𝑀, 𝑁}) ↔ 𝑥 ∈ (𝑀[,]𝑁))) |
223 | 222 | biimpar 501 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ∨ 𝑥 ∈ {𝑀, 𝑁})) |
224 | 124, 217,
223 | mpjaod 395 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (∀𝑧 ∈ (𝑀(,)𝑁)(𝐺‘𝑧) ≤ (𝐺‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶)) |
225 | 91, 224 | syld 46 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) → ((ℝ D 𝐹)‘𝑥) = 𝐶)) |
226 | 225 | reximdva 3000 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ (𝑀[,]𝑁)∀𝑧 ∈ (𝑀[,]𝑁)((𝐺 ↾ (𝑀[,]𝑁))‘𝑧) ≤ ((𝐺 ↾ (𝑀[,]𝑁))‘𝑥) → ∃𝑥 ∈ (𝑀[,]𝑁)((ℝ D 𝐹)‘𝑥) = 𝐶)) |
227 | 82, 226 | mpd 15 |
1
⊢ (𝜑 → ∃𝑥 ∈ (𝑀[,]𝑁)((ℝ D 𝐹)‘𝑥) = 𝐶) |