Step | Hyp | Ref
| Expression |
1 | | dvivth.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (𝐴(,)𝐵)) |
2 | 1 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑀 ∈ (𝐴(,)𝐵)) |
3 | | dvivth.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ (𝐴(,)𝐵)) |
4 | 3 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑁 ∈ (𝐴(,)𝐵)) |
5 | | dvivth.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
6 | | cncff 22696 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
8 | 7 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑤) ∈ ℝ) |
9 | 8 | renegcld 10457 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → -(𝐹‘𝑤) ∈ ℝ) |
10 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) |
11 | 9, 10 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)):(𝐴(,)𝐵)⟶ℝ) |
12 | | ax-resscn 9993 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
13 | | ssid 3624 |
. . . . . . . . . . . . . . 15
⊢ ℂ
⊆ ℂ |
14 | | cncfss 22702 |
. . . . . . . . . . . . . . 15
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℝ) ⊆ ((𝐴(,)𝐵)–cn→ℂ)) |
15 | 12, 13, 14 | mp2an 708 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝐵)–cn→ℝ) ⊆ ((𝐴(,)𝐵)–cn→ℂ) |
16 | 15, 5 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
17 | 10 | negfcncf 22722 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
19 | | cncffvrn 22701 |
. . . . . . . . . . . 12
⊢ ((ℝ
⊆ ℂ ∧ (𝑤
∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)):(𝐴(,)𝐵)⟶ℝ)) |
20 | 12, 18, 19 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)):(𝐴(,)𝐵)⟶ℝ)) |
21 | 11, 20 | mpbird 247 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
22 | 21 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
23 | | reelprrecn 10028 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ℝ ∈ {ℝ,
ℂ}) |
25 | 7 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
26 | 25 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑤) ∈ ℝ) |
27 | 26 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑤) ∈ ℂ) |
28 | | fvexd 6203 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑤) ∈ V) |
29 | 25 | feqmptd 6249 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝐹 = (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑤))) |
30 | 29 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D 𝐹) = (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑤)))) |
31 | | ioossre 12235 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴(,)𝐵) ⊆ ℝ |
32 | | dvfre 23714 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
33 | 7, 31, 32 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
34 | | dvivth.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
35 | 34 | feq2d 6031 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℝ)) |
36 | 33, 35 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ) |
37 | 36 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ) |
38 | 37 | feqmptd 6249 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D 𝐹) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑤))) |
39 | 30, 38 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑤))) |
40 | 24, 27, 28, 39 | dvmptneg 23729 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))) |
41 | 40 | dmeqd 5326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → dom (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))) = dom (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))) |
42 | | dmmptg 5632 |
. . . . . . . . . . 11
⊢
(∀𝑤 ∈
(𝐴(,)𝐵)-((ℝ D 𝐹)‘𝑤) ∈ V → dom (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) = (𝐴(,)𝐵)) |
43 | | negex 10279 |
. . . . . . . . . . . 12
⊢
-((ℝ D 𝐹)‘𝑤) ∈ V |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ (𝐴(,)𝐵) → -((ℝ D 𝐹)‘𝑤) ∈ V) |
45 | 42, 44 | mprg 2926 |
. . . . . . . . . 10
⊢ dom
(𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) = (𝐴(,)𝐵) |
46 | 41, 45 | syl6eq 2672 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → dom (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))) = (𝐴(,)𝐵)) |
47 | | simprl 794 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑀 < 𝑁) |
48 | | simprr 796 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁))) |
49 | 36, 1 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑀) ∈ ℝ) |
50 | 49 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D 𝐹)‘𝑀) ∈ ℝ) |
51 | 3, 34 | eleqtrrd 2704 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ dom (ℝ D 𝐹)) |
52 | 33, 51 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑁) ∈ ℝ) |
53 | 52 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D 𝐹)‘𝑁) ∈ ℝ) |
54 | | iccssre 12255 |
. . . . . . . . . . . . . . 15
⊢
((((ℝ D 𝐹)‘𝑀) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ∈ ℝ) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ℝ) |
55 | 49, 52, 54 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ℝ) |
56 | 55 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ℝ) |
57 | 56, 48 | sseldd 3604 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ ℝ) |
58 | | iccneg 12293 |
. . . . . . . . . . . 12
⊢
((((ℝ D 𝐹)‘𝑀) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ↔ -𝑥 ∈ (-((ℝ D 𝐹)‘𝑁)[,]-((ℝ D 𝐹)‘𝑀)))) |
59 | 50, 53, 57, 58 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ↔ -𝑥 ∈ (-((ℝ D 𝐹)‘𝑁)[,]-((ℝ D 𝐹)‘𝑀)))) |
60 | 48, 59 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → -𝑥 ∈ (-((ℝ D 𝐹)‘𝑁)[,]-((ℝ D 𝐹)‘𝑀))) |
61 | 40 | fveq1d 6193 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑁) = ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑁)) |
62 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑁 → ((ℝ D 𝐹)‘𝑤) = ((ℝ D 𝐹)‘𝑁)) |
63 | 62 | negeqd 10275 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑁 → -((ℝ D 𝐹)‘𝑤) = -((ℝ D 𝐹)‘𝑁)) |
64 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) |
65 | | negex 10279 |
. . . . . . . . . . . . . 14
⊢
-((ℝ D 𝐹)‘𝑁) ∈ V |
66 | 63, 64, 65 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (𝐴(,)𝐵) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑁) = -((ℝ D 𝐹)‘𝑁)) |
67 | 4, 66 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑁) = -((ℝ D 𝐹)‘𝑁)) |
68 | 61, 67 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑁) = -((ℝ D 𝐹)‘𝑁)) |
69 | 40 | fveq1d 6193 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑀) = ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑀)) |
70 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑀 → ((ℝ D 𝐹)‘𝑤) = ((ℝ D 𝐹)‘𝑀)) |
71 | 70 | negeqd 10275 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑀 → -((ℝ D 𝐹)‘𝑤) = -((ℝ D 𝐹)‘𝑀)) |
72 | | negex 10279 |
. . . . . . . . . . . . . 14
⊢
-((ℝ D 𝐹)‘𝑀) ∈ V |
73 | 71, 64, 72 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ (𝐴(,)𝐵) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑀) = -((ℝ D 𝐹)‘𝑀)) |
74 | 2, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑀) = -((ℝ D 𝐹)‘𝑀)) |
75 | 69, 74 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑀) = -((ℝ D 𝐹)‘𝑀)) |
76 | 68, 75 | oveq12d 6668 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑁)[,]((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑀)) = (-((ℝ D 𝐹)‘𝑁)[,]-((ℝ D 𝐹)‘𝑀))) |
77 | 60, 76 | eleqtrrd 2704 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → -𝑥 ∈ (((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑁)[,]((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑀))) |
78 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ (((𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))‘𝑦) − (-𝑥 · 𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (((𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))‘𝑦) − (-𝑥 · 𝑦))) |
79 | 2, 4, 22, 46, 47, 77, 78 | dvivthlem2 23772 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → -𝑥 ∈ ran (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))) |
80 | 40 | rneqd 5353 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ran (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))) = ran (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))) |
81 | 79, 80 | eleqtrd 2703 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → -𝑥 ∈ ran (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))) |
82 | | negex 10279 |
. . . . . . . 8
⊢ -𝑥 ∈ V |
83 | 64 | elrnmpt 5372 |
. . . . . . . 8
⊢ (-𝑥 ∈ V → (-𝑥 ∈ ran (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)-𝑥 = -((ℝ D 𝐹)‘𝑤))) |
84 | 82, 83 | ax-mp 5 |
. . . . . . 7
⊢ (-𝑥 ∈ ran (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)-𝑥 = -((ℝ D 𝐹)‘𝑤)) |
85 | 81, 84 | sylib 208 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ∃𝑤 ∈ (𝐴(,)𝐵)-𝑥 = -((ℝ D 𝐹)‘𝑤)) |
86 | 57 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ ℂ) |
87 | 86 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℂ) |
88 | 24, 27, 28, 39 | dvmptcl 23722 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑤) ∈ ℂ) |
89 | 87, 88 | neg11ad 10388 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (-𝑥 = -((ℝ D 𝐹)‘𝑤) ↔ 𝑥 = ((ℝ D 𝐹)‘𝑤))) |
90 | | eqcom 2629 |
. . . . . . . 8
⊢ (𝑥 = ((ℝ D 𝐹)‘𝑤) ↔ ((ℝ D 𝐹)‘𝑤) = 𝑥) |
91 | 89, 90 | syl6bb 276 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (-𝑥 = -((ℝ D 𝐹)‘𝑤) ↔ ((ℝ D 𝐹)‘𝑤) = 𝑥)) |
92 | 91 | rexbidva 3049 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (∃𝑤 ∈ (𝐴(,)𝐵)-𝑥 = -((ℝ D 𝐹)‘𝑤) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑤) = 𝑥)) |
93 | 85, 92 | mpbid 222 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ∃𝑤 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑤) = 𝑥) |
94 | | ffn 6045 |
. . . . . . 7
⊢ ((ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℝ → (ℝ D 𝐹) Fn (𝐴(,)𝐵)) |
95 | 37, 94 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D 𝐹) Fn (𝐴(,)𝐵)) |
96 | | fvelrnb 6243 |
. . . . . 6
⊢ ((ℝ
D 𝐹) Fn (𝐴(,)𝐵) → (𝑥 ∈ ran (ℝ D 𝐹) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑤) = 𝑥)) |
97 | 95, 96 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (𝑥 ∈ ran (ℝ D 𝐹) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑤) = 𝑥)) |
98 | 93, 97 | mpbird 247 |
. . . 4
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ ran (ℝ D 𝐹)) |
99 | 98 | expr 643 |
. . 3
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → (𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) → 𝑥 ∈ ran (ℝ D 𝐹))) |
100 | 99 | ssrdv 3609 |
. 2
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) |
101 | | fveq2 6191 |
. . . . 5
⊢ (𝑀 = 𝑁 → ((ℝ D 𝐹)‘𝑀) = ((ℝ D 𝐹)‘𝑁)) |
102 | 101 | oveq1d 6665 |
. . . 4
⊢ (𝑀 = 𝑁 → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) = (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑁))) |
103 | 52 | rexrd 10089 |
. . . . 5
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑁) ∈
ℝ*) |
104 | | iccid 12220 |
. . . . 5
⊢
(((ℝ D 𝐹)‘𝑁) ∈ ℝ* →
(((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑁)) = {((ℝ D 𝐹)‘𝑁)}) |
105 | 103, 104 | syl 17 |
. . . 4
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑁)) = {((ℝ D 𝐹)‘𝑁)}) |
106 | 102, 105 | sylan9eqr 2678 |
. . 3
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) = {((ℝ D 𝐹)‘𝑁)}) |
107 | | ffn 6045 |
. . . . . . 7
⊢ ((ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℝ → (ℝ
D 𝐹) Fn dom (ℝ D
𝐹)) |
108 | 33, 107 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ℝ D 𝐹) Fn dom (ℝ D 𝐹)) |
109 | | fnfvelrn 6356 |
. . . . . 6
⊢
(((ℝ D 𝐹) Fn
dom (ℝ D 𝐹) ∧
𝑁 ∈ dom (ℝ D
𝐹)) → ((ℝ D
𝐹)‘𝑁) ∈ ran (ℝ D 𝐹)) |
110 | 108, 51, 109 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑁) ∈ ran (ℝ D 𝐹)) |
111 | 110 | snssd 4340 |
. . . 4
⊢ (𝜑 → {((ℝ D 𝐹)‘𝑁)} ⊆ ran (ℝ D 𝐹)) |
112 | 111 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → {((ℝ D 𝐹)‘𝑁)} ⊆ ran (ℝ D 𝐹)) |
113 | 106, 112 | eqsstrd 3639 |
. 2
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) |
114 | 3 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑁 ∈ (𝐴(,)𝐵)) |
115 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑀 ∈ (𝐴(,)𝐵)) |
116 | 5 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
117 | 34 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
118 | | simprl 794 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑁 < 𝑀) |
119 | | simprr 796 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁))) |
120 | | eqid 2622 |
. . . . 5
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝑥 · 𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝑥 · 𝑦))) |
121 | 114, 115,
116, 117, 118, 119, 120 | dvivthlem2 23772 |
. . . 4
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ ran (ℝ D 𝐹)) |
122 | 121 | expr 643 |
. . 3
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) → 𝑥 ∈ ran (ℝ D 𝐹))) |
123 | 122 | ssrdv 3609 |
. 2
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) |
124 | 31, 1 | sseldi 3601 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℝ) |
125 | 31, 3 | sseldi 3601 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℝ) |
126 | 124, 125 | lttri4d 10178 |
. 2
⊢ (𝜑 → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |
127 | 100, 113,
123, 126 | mpjao3dan 1395 |
1
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) |