| 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 24919 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
| 7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
| 8 | 7 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑤) ∈ ℝ) |
| 9 | 8 | renegcld 11690 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → -(𝐹‘𝑤) ∈ ℝ) |
| 10 | 9 | fmpttd 7135 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)):(𝐴(,)𝐵)⟶ℝ) |
| 11 | | ax-resscn 11212 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
| 12 | | ssid 4006 |
. . . . . . . . . . . . . . 15
⊢ ℂ
⊆ ℂ |
| 13 | | cncfss 24925 |
. . . . . . . . . . . . . . 15
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℝ) ⊆ ((𝐴(,)𝐵)–cn→ℂ)) |
| 14 | 11, 12, 13 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝐵)–cn→ℝ) ⊆ ((𝐴(,)𝐵)–cn→ℂ) |
| 15 | 14, 5 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 16 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) |
| 17 | 16 | negfcncf 24950 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 18 | 15, 17 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 19 | | cncfcdm 24924 |
. . . . . . . . . . . 12
⊢ ((ℝ
⊆ ℂ ∧ (𝑤
∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)):(𝐴(,)𝐵)⟶ℝ)) |
| 20 | 11, 18, 19 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)):(𝐴(,)𝐵)⟶ℝ)) |
| 21 | 10, 20 | mpbird 257 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
| 22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)) ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
| 23 | | reelprrecn 11247 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} |
| 24 | 23 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ℝ ∈ {ℝ,
ℂ}) |
| 25 | 7 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
| 26 | 25 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑤) ∈ ℝ) |
| 27 | 26 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑤) ∈ ℂ) |
| 28 | | fvexd 6921 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑤) ∈ V) |
| 29 | 25 | feqmptd 6977 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝐹 = (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑤))) |
| 30 | 29 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D 𝐹) = (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑤)))) |
| 31 | | ioossre 13448 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴(,)𝐵) ⊆ ℝ |
| 32 | | dvfre 25989 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
| 33 | 7, 31, 32 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
| 34 | | dvivth.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
| 35 | 34 | feq2d 6722 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℝ)) |
| 36 | 33, 35 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ) |
| 37 | 36 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ) |
| 38 | 37 | feqmptd 6977 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D 𝐹) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑤))) |
| 39 | 30, 38 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑤))) |
| 40 | 24, 27, 28, 39 | dvmptneg 26004 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))) |
| 41 | 40 | dmeqd 5916 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → dom (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))) = dom (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))) |
| 42 | | dmmptg 6262 |
. . . . . . . . . . 11
⊢
(∀𝑤 ∈
(𝐴(,)𝐵)-((ℝ D 𝐹)‘𝑤) ∈ V → dom (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) = (𝐴(,)𝐵)) |
| 43 | | negex 11506 |
. . . . . . . . . . . 12
⊢
-((ℝ D 𝐹)‘𝑤) ∈ V |
| 44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ (𝐴(,)𝐵) → -((ℝ D 𝐹)‘𝑤) ∈ V) |
| 45 | 42, 44 | mprg 3067 |
. . . . . . . . . 10
⊢ dom
(𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) = (𝐴(,)𝐵) |
| 46 | 41, 45 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → dom (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))) = (𝐴(,)𝐵)) |
| 47 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑀 < 𝑁) |
| 48 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁))) |
| 49 | 36, 1 | ffvelcdmd 7105 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑀) ∈ ℝ) |
| 50 | 49 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D 𝐹)‘𝑀) ∈ ℝ) |
| 51 | 3, 34 | eleqtrrd 2844 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ dom (ℝ D 𝐹)) |
| 52 | 33, 51 | ffvelcdmd 7105 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑁) ∈ ℝ) |
| 53 | 52 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D 𝐹)‘𝑁) ∈ ℝ) |
| 54 | | iccssre 13469 |
. . . . . . . . . . . . . . 15
⊢
((((ℝ D 𝐹)‘𝑀) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ∈ ℝ) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ℝ) |
| 55 | 49, 52, 54 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ℝ) |
| 56 | 55 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ℝ) |
| 57 | 56, 48 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ ℝ) |
| 58 | | iccneg 13512 |
. . . . . . . . . . . 12
⊢
((((ℝ D 𝐹)‘𝑀) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑁) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ↔ -𝑥 ∈ (-((ℝ D 𝐹)‘𝑁)[,]-((ℝ D 𝐹)‘𝑀)))) |
| 59 | 50, 53, 57, 58 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ↔ -𝑥 ∈ (-((ℝ D 𝐹)‘𝑁)[,]-((ℝ D 𝐹)‘𝑀)))) |
| 60 | 48, 59 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → -𝑥 ∈ (-((ℝ D 𝐹)‘𝑁)[,]-((ℝ D 𝐹)‘𝑀))) |
| 61 | 40 | fveq1d 6908 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑁) = ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑁)) |
| 62 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑁 → ((ℝ D 𝐹)‘𝑤) = ((ℝ D 𝐹)‘𝑁)) |
| 63 | 62 | negeqd 11502 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑁 → -((ℝ D 𝐹)‘𝑤) = -((ℝ D 𝐹)‘𝑁)) |
| 64 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) |
| 65 | | negex 11506 |
. . . . . . . . . . . . . 14
⊢
-((ℝ D 𝐹)‘𝑁) ∈ V |
| 66 | 63, 64, 65 | fvmpt 7016 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (𝐴(,)𝐵) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑁) = -((ℝ D 𝐹)‘𝑁)) |
| 67 | 4, 66 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑁) = -((ℝ D 𝐹)‘𝑁)) |
| 68 | 61, 67 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑁) = -((ℝ D 𝐹)‘𝑁)) |
| 69 | 40 | fveq1d 6908 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑀) = ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑀)) |
| 70 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑀 → ((ℝ D 𝐹)‘𝑤) = ((ℝ D 𝐹)‘𝑀)) |
| 71 | 70 | negeqd 11502 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑀 → -((ℝ D 𝐹)‘𝑤) = -((ℝ D 𝐹)‘𝑀)) |
| 72 | | negex 11506 |
. . . . . . . . . . . . . 14
⊢
-((ℝ D 𝐹)‘𝑀) ∈ V |
| 73 | 71, 64, 72 | fvmpt 7016 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ (𝐴(,)𝐵) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑀) = -((ℝ D 𝐹)‘𝑀)) |
| 74 | 2, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))‘𝑀) = -((ℝ D 𝐹)‘𝑀)) |
| 75 | 69, 74 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑀) = -((ℝ D 𝐹)‘𝑀)) |
| 76 | 68, 75 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑁)[,]((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑀)) = (-((ℝ D 𝐹)‘𝑁)[,]-((ℝ D 𝐹)‘𝑀))) |
| 77 | 60, 76 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → -𝑥 ∈ (((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑁)[,]((ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))‘𝑀))) |
| 78 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ (((𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))‘𝑦) − (-𝑥 · 𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (((𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))‘𝑦) − (-𝑥 · 𝑦))) |
| 79 | 2, 4, 22, 46, 47, 77, 78 | dvivthlem2 26048 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → -𝑥 ∈ ran (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤)))) |
| 80 | 40 | rneqd 5949 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ran (ℝ D (𝑤 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑤))) = ran (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))) |
| 81 | 79, 80 | eleqtrd 2843 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → -𝑥 ∈ ran (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤))) |
| 82 | | negex 11506 |
. . . . . . . 8
⊢ -𝑥 ∈ V |
| 83 | 64 | elrnmpt 5969 |
. . . . . . . 8
⊢ (-𝑥 ∈ V → (-𝑥 ∈ ran (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)-𝑥 = -((ℝ D 𝐹)‘𝑤))) |
| 84 | 82, 83 | ax-mp 5 |
. . . . . . 7
⊢ (-𝑥 ∈ ran (𝑤 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑤)) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)-𝑥 = -((ℝ D 𝐹)‘𝑤)) |
| 85 | 81, 84 | sylib 218 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ∃𝑤 ∈ (𝐴(,)𝐵)-𝑥 = -((ℝ D 𝐹)‘𝑤)) |
| 86 | 57 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ ℂ) |
| 87 | 86 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℂ) |
| 88 | 24, 27, 28, 39 | dvmptcl 25997 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑤) ∈ ℂ) |
| 89 | 87, 88 | neg11ad 11616 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (-𝑥 = -((ℝ D 𝐹)‘𝑤) ↔ 𝑥 = ((ℝ D 𝐹)‘𝑤))) |
| 90 | | eqcom 2744 |
. . . . . . . 8
⊢ (𝑥 = ((ℝ D 𝐹)‘𝑤) ↔ ((ℝ D 𝐹)‘𝑤) = 𝑥) |
| 91 | 89, 90 | bitrdi 287 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (-𝑥 = -((ℝ D 𝐹)‘𝑤) ↔ ((ℝ D 𝐹)‘𝑤) = 𝑥)) |
| 92 | 91 | rexbidva 3177 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (∃𝑤 ∈ (𝐴(,)𝐵)-𝑥 = -((ℝ D 𝐹)‘𝑤) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑤) = 𝑥)) |
| 93 | 85, 92 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → ∃𝑤 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑤) = 𝑥) |
| 94 | 37 | ffnd 6737 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (ℝ D 𝐹) Fn (𝐴(,)𝐵)) |
| 95 | | fvelrnb 6969 |
. . . . . 6
⊢ ((ℝ
D 𝐹) Fn (𝐴(,)𝐵) → (𝑥 ∈ ran (ℝ D 𝐹) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑤) = 𝑥)) |
| 96 | 94, 95 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → (𝑥 ∈ ran (ℝ D 𝐹) ↔ ∃𝑤 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑤) = 𝑥)) |
| 97 | 93, 96 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ (𝑀 < 𝑁 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ ran (ℝ D 𝐹)) |
| 98 | 97 | expr 456 |
. . 3
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → (𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) → 𝑥 ∈ ran (ℝ D 𝐹))) |
| 99 | 98 | ssrdv 3989 |
. 2
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) |
| 100 | | fveq2 6906 |
. . . . 5
⊢ (𝑀 = 𝑁 → ((ℝ D 𝐹)‘𝑀) = ((ℝ D 𝐹)‘𝑁)) |
| 101 | 100 | oveq1d 7446 |
. . . 4
⊢ (𝑀 = 𝑁 → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) = (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑁))) |
| 102 | 52 | rexrd 11311 |
. . . . 5
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑁) ∈
ℝ*) |
| 103 | | iccid 13432 |
. . . . 5
⊢
(((ℝ D 𝐹)‘𝑁) ∈ ℝ* →
(((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑁)) = {((ℝ D 𝐹)‘𝑁)}) |
| 104 | 102, 103 | syl 17 |
. . . 4
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑁)[,]((ℝ D 𝐹)‘𝑁)) = {((ℝ D 𝐹)‘𝑁)}) |
| 105 | 101, 104 | sylan9eqr 2799 |
. . 3
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) = {((ℝ D 𝐹)‘𝑁)}) |
| 106 | 33 | ffnd 6737 |
. . . . . 6
⊢ (𝜑 → (ℝ D 𝐹) Fn dom (ℝ D 𝐹)) |
| 107 | | fnfvelrn 7100 |
. . . . . 6
⊢
(((ℝ D 𝐹) Fn
dom (ℝ D 𝐹) ∧
𝑁 ∈ dom (ℝ D
𝐹)) → ((ℝ D
𝐹)‘𝑁) ∈ ran (ℝ D 𝐹)) |
| 108 | 106, 51, 107 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((ℝ D 𝐹)‘𝑁) ∈ ran (ℝ D 𝐹)) |
| 109 | 108 | snssd 4809 |
. . . 4
⊢ (𝜑 → {((ℝ D 𝐹)‘𝑁)} ⊆ ran (ℝ D 𝐹)) |
| 110 | 109 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → {((ℝ D 𝐹)‘𝑁)} ⊆ ran (ℝ D 𝐹)) |
| 111 | 105, 110 | eqsstrd 4018 |
. 2
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) |
| 112 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑁 ∈ (𝐴(,)𝐵)) |
| 113 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑀 ∈ (𝐴(,)𝐵)) |
| 114 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
| 115 | 34 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
| 116 | | simprl 771 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑁 < 𝑀) |
| 117 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁))) |
| 118 | | eqid 2737 |
. . . . 5
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝑥 · 𝑦))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑦) − (𝑥 · 𝑦))) |
| 119 | 112, 113,
114, 115, 116, 117, 118 | dvivthlem2 26048 |
. . . 4
⊢ ((𝜑 ∧ (𝑁 < 𝑀 ∧ 𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)))) → 𝑥 ∈ ran (ℝ D 𝐹)) |
| 120 | 119 | expr 456 |
. . 3
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝑥 ∈ (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) → 𝑥 ∈ ran (ℝ D 𝐹))) |
| 121 | 120 | ssrdv 3989 |
. 2
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) |
| 122 | 31, 1 | sselid 3981 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 123 | 31, 3 | sselid 3981 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 124 | 122, 123 | lttri4d 11402 |
. 2
⊢ (𝜑 → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |
| 125 | 99, 111, 121, 124 | mpjao3dan 1434 |
1
⊢ (𝜑 → (((ℝ D 𝐹)‘𝑀)[,]((ℝ D 𝐹)‘𝑁)) ⊆ ran (ℝ D 𝐹)) |