Step | Hyp | Ref
| Expression |
1 | | dvivth.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵)) |
2 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑀 ∈ (𝐴(,)𝐵)) |
3 | | dvivth.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵)) |
4 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑁 ∈ (𝐴(,)𝐵)) |
5 | | dvivth.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
6 | | cncff 22504 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
8 | 7 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑤) ∈ ℝ) |
9 | 8 | renegcld 10336 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → -(𝐹‘𝑤) ∈ ℝ) |
10 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) |
11 | 9, 10 | fmptd 6292 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)):(𝐴(,)𝐵)⟶ℝ) |
12 | | ax-resscn 9872 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
13 | | ssid 3587 |
. . . . . . . . . . . . . . 15
⊢ ℂ
⊆ ℂ |
14 | | cncfss 22510 |
. . . . . . . . . . . . . . 15
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℝ) ⊆ ((𝐴(,)𝐵)–cn→ℂ)) |
15 | 12, 13, 14 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝐵)–cn→ℝ) ⊆ ((𝐴(,)𝐵)–cn→ℂ) |
16 | 15, 5 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
17 | 10 | negfcncf 22530 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
19 | | cncffvrn 22509 |
. . . . . . . . . . . 12
⊢ ((ℝ
⊆ ℂ ∧ (𝑤
∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)):(𝐴(,)𝐵)⟶ℝ)) |
20 | 12, 18, 19 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)):(𝐴(,)𝐵)⟶ℝ)) |
21 | 11, 20 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
23 | | reelprrecn 9907 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ℝ ∈ {ℝ,
ℂ}) |
25 | 7 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
26 | 25 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑤) ∈ ℝ) |
27 | 26 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑤) ∈ ℂ) |
28 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ ((ℝ
D 𝐹)‘𝑤) ∈ V |
29 | 28 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑤) ∈ V) |
30 | 25 | feqmptd 6159 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝐹 = (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑤))) |
31 | 30 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D 𝐹) = (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑤)))) |
32 | | ioossre 12106 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴(,)𝐵) ⊆ ℝ |
33 | | dvfre 23520 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
34 | 7, 32, 33 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
35 | | dvivth.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
36 | 35 | feq2d 5944 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℝ)) |
37 | 34, 36 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ) |
39 | 38 | feqmptd 6159 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D 𝐹) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑤))) |
40 | 31, 39 | eqtr3d 2646 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑤))) |
41 | 24, 27, 29, 40 | dvmptneg 23535 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))) |
42 | 41 | dmeqd 5248 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → dom (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))) = dom (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))) |
43 | | dmmptg 5549 |
. . . . . . . . . . 11
⊢
(∀𝑤 ∈
(𝐴(,)𝐵)-((ℝ D 𝐹)‘𝑤) ∈ V → dom (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) = (𝐴(,)𝐵)) |
44 | | negex 10158 |
. . . . . . . . . . . 12
⊢
-((ℝ D 𝐹)‘𝑤) ∈ V |
45 | 44 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ (𝐴(,)𝐵) → -((ℝ D 𝐹)‘𝑤) ∈ V) |
46 | 43, 45 | mprg 2910 |
. . . . . . . . . 10
⊢ dom
(𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) = (𝐴(,)𝐵) |
47 | 42, 46 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → dom (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))) = (𝐴(,)𝐵)) |
48 | | simprl 790 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑀 < 𝑁) |
49 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁))) |
50 | 37, 1 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑀) ∈ ℝ) |
51 | 50 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D 𝐹)‘𝑀) ∈ ℝ) |
52 | 3, 35 | eleqtrrd 2691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ dom (ℝ D 𝐹)) |
53 | 34, 52 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑁) ∈ ℝ) |
54 | 53 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D 𝐹)‘𝑁) ∈ ℝ) |
55 | | iccssre 12126 |
. . . . . . . . . . . . . . 15
⊢
((((ℝ D 𝐹)‘𝑀) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ∈ ℝ) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ℝ) |
56 | 50, 53, 55 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ℝ) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ℝ) |
58 | 57, 49 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ ℝ) |
59 | | iccneg 12164 |
. . . . . . . . . . . 12
⊢
((((ℝ D 𝐹)‘𝑀) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ↔ -𝑥 ∈ (-((ℝ D 𝐹)‘𝑁)[,]-((ℝ D 𝐹)‘𝑀)))) |
60 | 51, 54, 58, 59 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ↔ -𝑥 ∈ (-((ℝ D 𝐹)‘𝑁)[,]-((ℝ D 𝐹)‘𝑀)))) |
61 | 49, 60 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → -𝑥 ∈ (-((ℝ D 𝐹)‘𝑁)[,]-((ℝ D 𝐹)‘𝑀))) |
62 | 41 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑁) = ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑁)) |
63 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑁 → ((ℝ D 𝐹)‘𝑤) = ((ℝ D 𝐹)‘𝑁)) |
64 | 63 | negeqd 10154 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑁 → -((ℝ D 𝐹)‘𝑤) = -((ℝ D 𝐹)‘𝑁)) |
65 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) |
66 | | negex 10158 |
. . . . . . . . . . . . . 14
⊢
-((ℝ D 𝐹)‘𝑁) ∈ V |
67 | 64, 65, 66 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (𝐴(,)𝐵) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑁) = -((ℝ D 𝐹)‘𝑁)) |
68 | 4, 67 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑁) = -((ℝ D 𝐹)‘𝑁)) |
69 | 62, 68 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑁) = -((ℝ D 𝐹)‘𝑁)) |
70 | 41 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑀) = ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑀)) |
71 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑀 → ((ℝ D 𝐹)‘𝑤) = ((ℝ D 𝐹)‘𝑀)) |
72 | 71 | negeqd 10154 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑀 → -((ℝ D 𝐹)‘𝑤) = -((ℝ D 𝐹)‘𝑀)) |
73 | | negex 10158 |
. . . . . . . . . . . . . 14
⊢
-((ℝ D 𝐹)‘𝑀) ∈ V |
74 | 72, 65, 73 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ (𝐴(,)𝐵) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑀) = -((ℝ D 𝐹)‘𝑀)) |
75 | 2, 74 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑀) = -((ℝ D 𝐹)‘𝑀)) |
76 | 70, 75 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑀) = -((ℝ D 𝐹)‘𝑀)) |
77 | 69, 76 | oveq12d 6567 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑁)[,]((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑀)) = (-((ℝ D 𝐹)‘𝑁)[,]-((ℝ D 𝐹)‘𝑀))) |
78 | 61, 77 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → -𝑥 ∈ (((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑁)[,]((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑀))) |
79 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ (((𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))‘𝑦) − (-𝑥 · 𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (((𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))‘𝑦) − (-𝑥 · 𝑦))) |
80 | 2, 4, 22, 47, 48, 78, 79 | dvivthlem2 23576 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → -𝑥 ∈ ran (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))) |
81 | 41 | rneqd 5274 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ran (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))) = ran (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))) |
82 | 80, 81 | eleqtrd 2690 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → -𝑥 ∈ ran (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))) |
83 | | negex 10158 |
. . . . . . . 8
⊢ -𝑥 ∈ V |
84 | 65 | elrnmpt 5293 |
. . . . . . . 8
⊢ (-𝑥 ∈ V → (-𝑥 ∈ ran (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)-𝑥 = -((ℝ D 𝐹)‘𝑤))) |
85 | 83, 84 | ax-mp 5 |
. . . . . . 7
⊢ (-𝑥 ∈ ran (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)-𝑥 = -((ℝ D 𝐹)‘𝑤)) |
86 | 82, 85 | sylib 207 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ∃𝑤 ∈ (𝐴(,)𝐵)-𝑥 = -((ℝ D 𝐹)‘𝑤)) |
87 | 58 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ ℂ) |
88 | 87 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℂ) |
89 | 24, 27, 29, 40 | dvmptcl 23528 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑤) ∈ ℂ) |
90 | 88, 89 | neg11ad 10267 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (-𝑥 = -((ℝ D 𝐹)‘𝑤) ↔ 𝑥 = ((ℝ D 𝐹)‘𝑤))) |
91 | | eqcom 2617 |
. . . . . . . 8
⊢ (𝑥 = ((ℝ D 𝐹)‘𝑤) ↔ ((ℝ D 𝐹)‘𝑤) = 𝑥) |
92 | 90, 91 | syl6bb 275 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (-𝑥 = -((ℝ D 𝐹)‘𝑤) ↔ ((ℝ D 𝐹)‘𝑤) = 𝑥)) |
93 | 92 | rexbidva 3031 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (∃𝑤 ∈ (𝐴(,)𝐵)-𝑥 = -((ℝ D 𝐹)‘𝑤) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑤) = 𝑥)) |
94 | 86, 93 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ∃𝑤 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑤) = 𝑥) |
95 | | ffn 5958 |
. . . . . . 7
⊢ ((ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℝ → (ℝ D 𝐹) Fn (𝐴(,)𝐵)) |
96 | 38, 95 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D 𝐹) Fn (𝐴(,)𝐵)) |
97 | | fvelrnb 6153 |
. . . . . 6
⊢ ((ℝ
D 𝐹) Fn (𝐴(,)𝐵) → (𝑥 ∈ ran (ℝ D 𝐹) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑤) = 𝑥)) |
98 | 96, 97 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (𝑥 ∈ ran (ℝ D 𝐹) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑤) = 𝑥)) |
99 | 94, 98 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ ran (ℝ D 𝐹)) |
100 | 99 | expr 641 |
. . 3
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → (𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) → 𝑥 ∈ ran (ℝ D 𝐹))) |
101 | 100 | ssrdv 3574 |
. 2
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) |
102 | | fveq2 6103 |
. . . . 5
⊢ (𝑀 = 𝑁 → ((ℝ D 𝐹)‘𝑀) = ((ℝ D 𝐹)‘𝑁)) |
103 | 102 | oveq1d 6564 |
. . . 4
⊢ (𝑀 = 𝑁 → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) = (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑁))) |
104 | 53 | rexrd 9968 |
. . . . 5
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑁) ∈
ℝ*) |
105 | | iccid 12091 |
. . . . 5
⊢
(((ℝ D 𝐹)‘𝑁) ∈ ℝ* →
(((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑁)) = {((ℝ D 𝐹)‘𝑁)}) |
106 | 104, 105 | syl 17 |
. . . 4
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑁)) = {((ℝ D 𝐹)‘𝑁)}) |
107 | 103, 106 | sylan9eqr 2666 |
. . 3
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) = {((ℝ D 𝐹)‘𝑁)}) |
108 | | ffn 5958 |
. . . . . . 7
⊢ ((ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℝ → (ℝ
D 𝐹) Fn dom (ℝ D
𝐹)) |
109 | 34, 108 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ℝ D 𝐹) Fn dom (ℝ D 𝐹)) |
110 | | fnfvelrn 6264 |
. . . . . 6
⊢
(((ℝ D 𝐹) Fn
dom (ℝ D 𝐹) ∧
𝑁 ∈ dom (ℝ D
𝐹)) → ((ℝ D
𝐹)‘𝑁) ∈ ran (ℝ D 𝐹)) |
111 | 109, 52, 110 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑁) ∈ ran (ℝ D 𝐹)) |
112 | 111 | snssd 4281 |
. . . 4
⊢ (𝜑 → {((ℝ D 𝐹)‘𝑁)} ⊆ ran (ℝ D 𝐹)) |
113 | 112 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → {((ℝ D 𝐹)‘𝑁)} ⊆ ran (ℝ D 𝐹)) |
114 | 107, 113 | eqsstrd 3602 |
. 2
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) |
115 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑁 ∈ (𝐴(,)𝐵)) |
116 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑀 ∈ (𝐴(,)𝐵)) |
117 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
118 | 35 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
119 | | simprl 790 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑁 < 𝑀) |
120 | | simprr 792 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁))) |
121 | | eqid 2610 |
. . . . 5
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝑥 · 𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝑥 · 𝑦))) |
122 | 115, 116,
117, 118, 119, 120, 121 | dvivthlem2 23576 |
. . . 4
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ ran (ℝ D 𝐹)) |
123 | 122 | expr 641 |
. . 3
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) → 𝑥 ∈ ran (ℝ D 𝐹))) |
124 | 123 | ssrdv 3574 |
. 2
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) |
125 | 32, 1 | sseldi 3566 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℝ) |
126 | 32, 3 | sseldi 3566 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℝ) |
127 | 125, 126 | lttri4d 10057 |
. 2
⊢ (𝜑 → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |
128 | 101, 114,
124, 127 | mpjao3dan 1387 |
1
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) |