| Step | Hyp | Ref
| Expression |
| 1 | | fdvposlt.d |
. . . 4
⊢ 𝐸 = (𝐶(,)𝐷) |
| 2 | | fdvposlt.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐸) |
| 3 | | fdvposlt.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝐸) |
| 4 | | fdvposlt.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐸⟶ℝ) |
| 5 | 4 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐸) → (𝐹‘𝑦) ∈ ℝ) |
| 6 | 5 | renegcld 11690 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐸) → -(𝐹‘𝑦) ∈ ℝ) |
| 7 | 6 | fmpttd 7135 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦)):𝐸⟶ℝ) |
| 8 | | reelprrecn 11247 |
. . . . . . 7
⊢ ℝ
∈ {ℝ, ℂ} |
| 9 | 8 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
| 10 | | ax-resscn 11212 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
| 11 | 10, 5 | sselid 3981 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐸) → (𝐹‘𝑦) ∈ ℂ) |
| 12 | | fvexd 6921 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐸) → ((ℝ D 𝐹)‘𝑦) ∈ V) |
| 13 | 4 | feqmptd 6977 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑦 ∈ 𝐸 ↦ (𝐹‘𝑦))) |
| 14 | 13 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ 𝐸 ↦ (𝐹‘𝑦)))) |
| 15 | | fdvposlt.c |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℝ)) |
| 16 | | cncff 24919 |
. . . . . . . . 9
⊢ ((ℝ
D 𝐹) ∈ (𝐸–cn→ℝ) → (ℝ D 𝐹):𝐸⟶ℝ) |
| 17 | 15, 16 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐹):𝐸⟶ℝ) |
| 18 | 17 | feqmptd 6977 |
. . . . . . 7
⊢ (𝜑 → (ℝ D 𝐹) = (𝑦 ∈ 𝐸 ↦ ((ℝ D 𝐹)‘𝑦))) |
| 19 | 14, 18 | eqtr3d 2779 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐸 ↦ (𝐹‘𝑦))) = (𝑦 ∈ 𝐸 ↦ ((ℝ D 𝐹)‘𝑦))) |
| 20 | 9, 11, 12, 19 | dvmptneg 26004 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))) = (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦))) |
| 21 | 17 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐸) → ((ℝ D 𝐹)‘𝑦) ∈ ℝ) |
| 22 | 21 | renegcld 11690 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐸) → -((ℝ D 𝐹)‘𝑦) ∈ ℝ) |
| 23 | 22 | fmpttd 7135 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)):𝐸⟶ℝ) |
| 24 | | ssid 4006 |
. . . . . . . . . 10
⊢ ℂ
⊆ ℂ |
| 25 | | cncfss 24925 |
. . . . . . . . . 10
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐸–cn→ℝ) ⊆ (𝐸–cn→ℂ)) |
| 26 | 10, 24, 25 | mp2an 692 |
. . . . . . . . 9
⊢ (𝐸–cn→ℝ) ⊆ (𝐸–cn→ℂ) |
| 27 | 26, 15 | sselid 3981 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℂ)) |
| 28 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) = (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) |
| 29 | 28 | negfcncf 24950 |
. . . . . . . 8
⊢ ((ℝ
D 𝐹) ∈ (𝐸–cn→ℂ) → (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) ∈ (𝐸–cn→ℂ)) |
| 30 | 27, 29 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) ∈ (𝐸–cn→ℂ)) |
| 31 | | cncfcdm 24924 |
. . . . . . 7
⊢ ((ℝ
⊆ ℂ ∧ (𝑦
∈ 𝐸 ↦ -((ℝ
D 𝐹)‘𝑦)) ∈ (𝐸–cn→ℂ)) → ((𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) ∈ (𝐸–cn→ℝ) ↔ (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)):𝐸⟶ℝ)) |
| 32 | 10, 30, 31 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) ∈ (𝐸–cn→ℝ) ↔ (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)):𝐸⟶ℝ)) |
| 33 | 23, 32 | mpbird 257 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) ∈ (𝐸–cn→ℝ)) |
| 34 | 20, 33 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))) ∈ (𝐸–cn→ℝ)) |
| 35 | | fdvnegge.le |
. . . 4
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
| 36 | | fdvnegge.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ≤ 0) |
| 37 | 17 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (ℝ D 𝐹):𝐸⟶ℝ) |
| 38 | | ioossicc 13473 |
. . . . . . . . . . 11
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
| 39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
| 40 | 1, 2, 3 | fct2relem 34612 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐸) |
| 41 | 39, 40 | sstrd 3994 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐸) |
| 42 | 41 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ 𝐸) |
| 43 | 37, 42 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ) |
| 44 | 43 | le0neg1d 11834 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) ≤ 0 ↔ 0 ≤ -((ℝ D 𝐹)‘𝑥))) |
| 45 | 36, 44 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ -((ℝ D 𝐹)‘𝑥)) |
| 46 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (ℝ D (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))) = (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦))) |
| 47 | 46 | fveq1d 6908 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦)))‘𝑥) = ((𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦))‘𝑥)) |
| 48 | 28 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦)) = (𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦))) |
| 49 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
| 50 | 49 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑥) → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘𝑥)) |
| 51 | 50 | negeqd 11502 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑥) → -((ℝ D 𝐹)‘𝑦) = -((ℝ D 𝐹)‘𝑥)) |
| 52 | 43 | renegcld 11690 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → -((ℝ D 𝐹)‘𝑥) ∈ ℝ) |
| 53 | 48, 51, 42, 52 | fvmptd 7023 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝑦 ∈ 𝐸 ↦ -((ℝ D 𝐹)‘𝑦))‘𝑥) = -((ℝ D 𝐹)‘𝑥)) |
| 54 | 47, 53 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦)))‘𝑥) = -((ℝ D 𝐹)‘𝑥)) |
| 55 | 45, 54 | breqtrrd 5171 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ ((ℝ D (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦)))‘𝑥)) |
| 56 | 1, 2, 3, 7, 34, 35, 55 | fdvposle 34616 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))‘𝐴) ≤ ((𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))‘𝐵)) |
| 57 | | eqidd 2738 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦)) = (𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))) |
| 58 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → 𝑦 = 𝐴) |
| 59 | 58 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → (𝐹‘𝑦) = (𝐹‘𝐴)) |
| 60 | 59 | negeqd 11502 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → -(𝐹‘𝑦) = -(𝐹‘𝐴)) |
| 61 | 4, 2 | ffvelcdmd 7105 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ) |
| 62 | 61 | renegcld 11690 |
. . . 4
⊢ (𝜑 → -(𝐹‘𝐴) ∈ ℝ) |
| 63 | 57, 60, 2, 62 | fvmptd 7023 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))‘𝐴) = -(𝐹‘𝐴)) |
| 64 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵) |
| 65 | 64 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (𝐹‘𝑦) = (𝐹‘𝐵)) |
| 66 | 65 | negeqd 11502 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → -(𝐹‘𝑦) = -(𝐹‘𝐵)) |
| 67 | 4, 3 | ffvelcdmd 7105 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ) |
| 68 | 67 | renegcld 11690 |
. . . 4
⊢ (𝜑 → -(𝐹‘𝐵) ∈ ℝ) |
| 69 | 57, 66, 3, 68 | fvmptd 7023 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ 𝐸 ↦ -(𝐹‘𝑦))‘𝐵) = -(𝐹‘𝐵)) |
| 70 | 56, 63, 69 | 3brtr3d 5174 |
. 2
⊢ (𝜑 → -(𝐹‘𝐴) ≤ -(𝐹‘𝐵)) |
| 71 | 67, 61 | lenegd 11842 |
. 2
⊢ (𝜑 → ((𝐹‘𝐵) ≤ (𝐹‘𝐴) ↔ -(𝐹‘𝐴) ≤ -(𝐹‘𝐵))) |
| 72 | 70, 71 | mpbird 257 |
1
⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐹‘𝐴)) |