Step | Hyp | Ref
| Expression |
1 | | df-fwddif 31436 |
. . . . 5
⊢ △
= (𝑓 ∈ (ℂ
↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥)))) |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → △ = (𝑓 ∈ (ℂ
↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥))))) |
3 | | dmeq 5246 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹) |
4 | 3 | eleq2d 2673 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ((𝑦 + 1) ∈ dom 𝑓 ↔ (𝑦 + 1) ∈ dom 𝐹)) |
5 | 3, 4 | rabeqbidv 3168 |
. . . . . 6
⊢ (𝑓 = 𝐹 → {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} = {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹}) |
6 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘(𝑥 + 1)) = (𝐹‘(𝑥 + 1))) |
7 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥)) |
8 | 6, 7 | oveq12d 6567 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥)) = ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥))) |
9 | 5, 8 | mpteq12dv 4663 |
. . . . 5
⊢ (𝑓 = 𝐹 → (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥))) = (𝑥 ∈ {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥)))) |
10 | 9 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 = 𝐹) → (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥))) = (𝑥 ∈ {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥)))) |
11 | | fwddifval.2 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
12 | | fwddifval.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
13 | | cnex 9896 |
. . . . . 6
⊢ ℂ
∈ V |
14 | | elpm2r 7761 |
. . . . . 6
⊢
(((ℂ ∈ V ∧ ℂ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ)) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
15 | 13, 13, 14 | mpanl12 714 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
16 | 11, 12, 15 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
17 | | fdm 5964 |
. . . . . . 7
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
18 | 11, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = 𝐴) |
19 | 13 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ∈
V) |
20 | 19, 12 | ssexd 4733 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ V) |
21 | 18, 20 | eqeltrd 2688 |
. . . . 5
⊢ (𝜑 → dom 𝐹 ∈ V) |
22 | | rabexg 4739 |
. . . . 5
⊢ (dom
𝐹 ∈ V → {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ∈ V) |
23 | | mptexg 6389 |
. . . . 5
⊢ ({𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ∈ V → (𝑥 ∈ {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥))) ∈ V) |
24 | 21, 22, 23 | 3syl 18 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥))) ∈ V) |
25 | 2, 10, 16, 24 | fvmptd 6197 |
. . 3
⊢ (𝜑 → ( △ ‘𝐹) = (𝑥 ∈ {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥)))) |
26 | 18 | eleq2d 2673 |
. . . . 5
⊢ (𝜑 → ((𝑦 + 1) ∈ dom 𝐹 ↔ (𝑦 + 1) ∈ 𝐴)) |
27 | 18, 26 | rabeqbidv 3168 |
. . . 4
⊢ (𝜑 → {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} = {𝑦 ∈ 𝐴 ∣ (𝑦 + 1) ∈ 𝐴}) |
28 | 27 | mpteq1d 4666 |
. . 3
⊢ (𝜑 → (𝑥 ∈ {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥))) = (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ (𝑦 + 1) ∈ 𝐴} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥)))) |
29 | 25, 28 | eqtrd 2644 |
. 2
⊢ (𝜑 → ( △ ‘𝐹) = (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ (𝑦 + 1) ∈ 𝐴} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥)))) |
30 | | oveq1 6556 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 + 1) = (𝑋 + 1)) |
31 | 30 | fveq2d 6107 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝐹‘(𝑥 + 1)) = (𝐹‘(𝑋 + 1))) |
32 | | fveq2 6103 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) |
33 | 31, 32 | oveq12d 6567 |
. . 3
⊢ (𝑥 = 𝑋 → ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥)) = ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋))) |
34 | 33 | adantl 481 |
. 2
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥)) = ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋))) |
35 | | fwddifval.3 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
36 | | fwddifval.4 |
. . 3
⊢ (𝜑 → (𝑋 + 1) ∈ 𝐴) |
37 | | oveq1 6556 |
. . . . 5
⊢ (𝑦 = 𝑋 → (𝑦 + 1) = (𝑋 + 1)) |
38 | 37 | eleq1d 2672 |
. . . 4
⊢ (𝑦 = 𝑋 → ((𝑦 + 1) ∈ 𝐴 ↔ (𝑋 + 1) ∈ 𝐴)) |
39 | 38 | elrab 3331 |
. . 3
⊢ (𝑋 ∈ {𝑦 ∈ 𝐴 ∣ (𝑦 + 1) ∈ 𝐴} ↔ (𝑋 ∈ 𝐴 ∧ (𝑋 + 1) ∈ 𝐴)) |
40 | 35, 36, 39 | sylanbrc 695 |
. 2
⊢ (𝜑 → 𝑋 ∈ {𝑦 ∈ 𝐴 ∣ (𝑦 + 1) ∈ 𝐴}) |
41 | | ovex 6577 |
. . 3
⊢ ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋)) ∈ V |
42 | 41 | a1i 11 |
. 2
⊢ (𝜑 → ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋)) ∈ V) |
43 | 29, 34, 40, 42 | fvmptd 6197 |
1
⊢ (𝜑 → (( △ ‘𝐹)‘𝑋) = ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋))) |