Step | Hyp | Ref
| Expression |
1 | | climsubmpt.z |
. 2
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | climsubmpt.m |
. 2
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | climsubmpt.c |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐶) |
4 | | fvex 6113 |
. . . . 5
⊢
(ℤ≥‘𝑀) ∈ V |
5 | 1, 4 | eqeltri 2684 |
. . . 4
⊢ 𝑍 ∈ V |
6 | 5 | mptex 6390 |
. . 3
⊢ (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ∈ V |
7 | 6 | a1i 11 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ∈ V) |
8 | | climsubmpt.d |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐷) |
9 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑍) |
10 | | climsubmpt.k |
. . . . . . 7
⊢
Ⅎ𝑘𝜑 |
11 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑘 𝑗 ∈ 𝑍 |
12 | 10, 11 | nfan 1816 |
. . . . . 6
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝑍) |
13 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑘𝑗 |
14 | 13 | nfcsb1 3514 |
. . . . . . 7
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐴 |
15 | 14 | nfel1 2765 |
. . . . . 6
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ |
16 | 12, 15 | nfim 1813 |
. . . . 5
⊢
Ⅎ𝑘((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ) |
17 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍)) |
18 | 17 | anbi2d 736 |
. . . . . 6
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ 𝑍) ↔ (𝜑 ∧ 𝑗 ∈ 𝑍))) |
19 | | csbeq1a 3508 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → 𝐴 = ⦋𝑗 / 𝑘⦌𝐴) |
20 | 19 | eleq1d 2672 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (𝐴 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ)) |
21 | 18, 20 | imbi12d 333 |
. . . . 5
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) ↔ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ))) |
22 | | climsubmpt.a |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) |
23 | 16, 21, 22 | chvar 2250 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ) |
24 | | eqid 2610 |
. . . . 5
⊢ (𝑘 ∈ 𝑍 ↦ 𝐴) = (𝑘 ∈ 𝑍 ↦ 𝐴) |
25 | 13, 14, 19, 24 | fvmptf 6209 |
. . . 4
⊢ ((𝑗 ∈ 𝑍 ∧ ⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ) → ((𝑘 ∈ 𝑍 ↦ 𝐴)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐴) |
26 | 9, 23, 25 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ 𝐴)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐴) |
27 | 26, 23 | eqeltrd 2688 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ 𝐴)‘𝑗) ∈ ℂ) |
28 | 13 | nfcsb1 3514 |
. . . . . . 7
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 |
29 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑘ℂ |
30 | 28, 29 | nfel 2763 |
. . . . . 6
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ |
31 | 12, 30 | nfim 1813 |
. . . . 5
⊢
Ⅎ𝑘((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ) |
32 | | csbeq1a 3508 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵) |
33 | 32 | eleq1d 2672 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ)) |
34 | 18, 33 | imbi12d 333 |
. . . . 5
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))) |
35 | | climsubmpt.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) |
36 | 31, 34, 35 | chvar 2250 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ) |
37 | | eqid 2610 |
. . . . 5
⊢ (𝑘 ∈ 𝑍 ↦ 𝐵) = (𝑘 ∈ 𝑍 ↦ 𝐵) |
38 | 13, 28, 32, 37 | fvmptf 6209 |
. . . 4
⊢ ((𝑗 ∈ 𝑍 ∧ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ) → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐵) |
39 | 9, 36, 38 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐵) |
40 | 39, 36 | eqeltrd 2688 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑗) ∈ ℂ) |
41 | | ovex 6577 |
. . . . 5
⊢
(⦋𝑗 /
𝑘⦌𝐴 − ⦋𝑗 / 𝑘⦌𝐵) ∈ V |
42 | 41 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (⦋𝑗 / 𝑘⦌𝐴 − ⦋𝑗 / 𝑘⦌𝐵) ∈ V) |
43 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑘
− |
44 | 14, 43, 28 | nfov 6575 |
. . . . 5
⊢
Ⅎ𝑘(⦋𝑗 / 𝑘⦌𝐴 − ⦋𝑗 / 𝑘⦌𝐵) |
45 | 19, 32 | oveq12d 6567 |
. . . . 5
⊢ (𝑘 = 𝑗 → (𝐴 − 𝐵) = (⦋𝑗 / 𝑘⦌𝐴 − ⦋𝑗 / 𝑘⦌𝐵)) |
46 | | eqid 2610 |
. . . . 5
⊢ (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) = (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) |
47 | 13, 44, 45, 46 | fvmptf 6209 |
. . . 4
⊢ ((𝑗 ∈ 𝑍 ∧ (⦋𝑗 / 𝑘⦌𝐴 − ⦋𝑗 / 𝑘⦌𝐵) ∈ V) → ((𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵))‘𝑗) = (⦋𝑗 / 𝑘⦌𝐴 − ⦋𝑗 / 𝑘⦌𝐵)) |
48 | 9, 42, 47 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵))‘𝑗) = (⦋𝑗 / 𝑘⦌𝐴 − ⦋𝑗 / 𝑘⦌𝐵)) |
49 | 26, 39 | oveq12d 6567 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ 𝐴)‘𝑗) − ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑗)) = (⦋𝑗 / 𝑘⦌𝐴 − ⦋𝑗 / 𝑘⦌𝐵)) |
50 | 48, 49 | eqtr4d 2647 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵))‘𝑗) = (((𝑘 ∈ 𝑍 ↦ 𝐴)‘𝑗) − ((𝑘 ∈ 𝑍 ↦ 𝐵)‘𝑗))) |
51 | 1, 2, 3, 7, 8, 27,
40, 50 | climsub 14212 |
1
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐶 − 𝐷)) |