Step | Hyp | Ref
| Expression |
1 | | fdvposlt.d |
. . . 4
⊢ 𝐸 = (𝐶(,)𝐷) |
2 | | fdvposlt.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐸) |
3 | | fdvposlt.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝐸) |
4 | | fdvposlt.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐸⟶ℝ) |
5 | 4 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐸) → (𝐹‘𝑦) ∈ ℝ) |
6 | 5 | renegcld 10457 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐸) → -(𝐹‘𝑦) ∈ ℝ) |
7 | | eqid 2622 |
. . . . 5
⊢ (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦)) = (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦)) |
8 | 6, 7 | fmptd 6385 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦)):𝐸⟶ℝ) |
9 | | reelprrecn 10028 |
. . . . . . 7
⊢ ℝ
∈ {ℝ, ℂ} |
10 | 9 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
11 | | ax-resscn 9993 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
12 | 11, 5 | sseldi 3601 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐸) → (𝐹‘𝑦) ∈ ℂ) |
13 | | fvexd 6203 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐸) → ((ℝ D 𝐹)‘𝑦) ∈ V) |
14 | 4 | feqmptd 6249 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑦 ∈ 𝐸 ↦ (𝐹‘𝑦))) |
15 | 14 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ 𝐸 ↦ (𝐹‘𝑦)))) |
16 | | fdvposlt.c |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℝ)) |
17 | | cncff 22696 |
. . . . . . . . 9
⊢ ((ℝ
D 𝐹) ∈ (𝐸–cn→ℝ) → (ℝ D 𝐹):𝐸⟶ℝ) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐹):𝐸⟶ℝ) |
19 | 18 | feqmptd 6249 |
. . . . . . 7
⊢ (𝜑 → (ℝ D 𝐹) = (𝑦 ∈ 𝐸 ↦ ((ℝ D 𝐹)‘𝑦))) |
20 | 15, 19 | eqtr3d 2658 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐸 ↦ (𝐹‘𝑦))) = (𝑦 ∈ 𝐸 ↦ ((ℝ D 𝐹)‘𝑦))) |
21 | 10, 12, 13, 20 | dvmptneg 23729 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))) = (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦))) |
22 | 18 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐸) → ((ℝ D 𝐹)‘𝑦) ∈ ℝ) |
23 | 22 | renegcld 10457 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐸) → -((ℝ D 𝐹)‘𝑦) ∈ ℝ) |
24 | | eqid 2622 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) = (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) |
25 | 23, 24 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)):𝐸⟶ℝ) |
26 | | ssid 3624 |
. . . . . . . . . 10
⊢ ℂ
⊆ ℂ |
27 | | cncfss 22702 |
. . . . . . . . . 10
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐸–cn→ℝ) ⊆ (𝐸–cn→ℂ)) |
28 | 11, 26, 27 | mp2an 708 |
. . . . . . . . 9
⊢ (𝐸–cn→ℝ) ⊆ (𝐸–cn→ℂ) |
29 | 28, 16 | sseldi 3601 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℂ)) |
30 | 24 | negfcncf 22722 |
. . . . . . . 8
⊢ ((ℝ
D 𝐹) ∈ (𝐸–cn→ℂ) → (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) ∈ (𝐸–cn→ℂ)) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) ∈ (𝐸–cn→ℂ)) |
32 | | cncffvrn 22701 |
. . . . . . 7
⊢ ((ℝ
⊆ ℂ ∧ (𝑦
∈ 𝐸 ↦ -((ℝ
D 𝐹)‘𝑦)) ∈ (𝐸–cn→ℂ)) → ((𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) ∈ (𝐸–cn→ℝ) ↔ (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)):𝐸⟶ℝ)) |
33 | 11, 31, 32 | sylancr 695 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) ∈ (𝐸–cn→ℝ) ↔ (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)):𝐸⟶ℝ)) |
34 | 25, 33 | mpbird 247 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) ∈ (𝐸–cn→ℝ)) |
35 | 21, 34 | eqeltrd 2701 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))) ∈ (𝐸–cn→ℝ)) |
36 | | fdvnegge.le |
. . . 4
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
37 | | fdvnegge.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ≤ 0) |
38 | 18 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (ℝ D 𝐹):𝐸⟶ℝ) |
39 | | ioossicc 12259 |
. . . . . . . . . . 11
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
40 | 39 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
41 | 1, 2, 3 | fct2relem 30675 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐸) |
42 | 40, 41 | sstrd 3613 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐸) |
43 | 42 | sselda 3603 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ 𝐸) |
44 | 38, 43 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ) |
45 | 44 | le0neg1d 10599 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) ≤ 0 ↔ 0 ≤ -((ℝ D 𝐹)‘𝑥))) |
46 | 37, 45 | mpbid 222 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ -((ℝ D 𝐹)‘𝑥)) |
47 | 21 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (ℝ D (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))) = (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦))) |
48 | 47 | fveq1d 6193 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦)))‘𝑥) = ((𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦))‘𝑥)) |
49 | 24 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) = (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦))) |
50 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
51 | 50 | fveq2d 6195 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑥) → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘𝑥)) |
52 | 51 | negeqd 10275 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑥) → -((ℝ D 𝐹)‘𝑦) = -((ℝ D 𝐹)‘𝑥)) |
53 | 44 | renegcld 10457 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → -((ℝ D 𝐹)‘𝑥) ∈ ℝ) |
54 | 49, 52, 43, 53 | fvmptd 6288 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦))‘𝑥) = -((ℝ D 𝐹)‘𝑥)) |
55 | 48, 54 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦)))‘𝑥) = -((ℝ D 𝐹)‘𝑥)) |
56 | 46, 55 | breqtrrd 4681 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ ((ℝ D (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦)))‘𝑥)) |
57 | 1, 2, 3, 8, 35, 36, 56 | fdvposle 30679 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))‘𝐴) ≤ ((𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))‘𝐵)) |
58 | | eqidd 2623 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦)) = (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))) |
59 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → 𝑦 = 𝐴) |
60 | 59 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → (𝐹‘𝑦) = (𝐹‘𝐴)) |
61 | 60 | negeqd 10275 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → -(𝐹‘𝑦) = -(𝐹‘𝐴)) |
62 | 4, 2 | ffvelrnd 6360 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ) |
63 | 62 | renegcld 10457 |
. . . 4
⊢ (𝜑 → -(𝐹‘𝐴) ∈ ℝ) |
64 | 58, 61, 2, 63 | fvmptd 6288 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))‘𝐴) = -(𝐹‘𝐴)) |
65 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵) |
66 | 65 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (𝐹‘𝑦) = (𝐹‘𝐵)) |
67 | 66 | negeqd 10275 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → -(𝐹‘𝑦) = -(𝐹‘𝐵)) |
68 | 4, 3 | ffvelrnd 6360 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ) |
69 | 68 | renegcld 10457 |
. . . 4
⊢ (𝜑 → -(𝐹‘𝐵) ∈ ℝ) |
70 | 58, 67, 3, 69 | fvmptd 6288 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))‘𝐵) = -(𝐹‘𝐵)) |
71 | 57, 64, 70 | 3brtr3d 4684 |
. 2
⊢ (𝜑 → -(𝐹‘𝐴) ≤ -(𝐹‘𝐵)) |
72 | 68, 62 | lenegd 10606 |
. 2
⊢ (𝜑 → ((𝐹‘𝐵) ≤ (𝐹‘𝐴) ↔ -(𝐹‘𝐴) ≤ -(𝐹‘𝐵))) |
73 | 71, 72 | mpbird 247 |
1
⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐹‘𝐴)) |